Library ZFwf

Require Import ZF ZFnats ZFord.
Import IZF.

Section WellFoundedSets.

Definition isWf x :=
  forall P : set -> Prop,
  (forall x x', x == x' -> P x -> P x') ->
  (forall a,(forall b, b \in a -> P b)-> P a) -> P x.

Lemma isWf_intro : forall x,
  (forall a, a \in x -> isWf a) -> isWf x.

Lemma isWf_ext : forall x x', x == x' -> isWf x -> isWf x'.

Lemma isWf_inv : forall a b,
  isWf a -> b \in a -> isWf b.

Lemma isWf_ind :
  forall P : set -> Prop,
  (forall x x', x == x' -> P x -> P x') ->
  (forall a, isWf a -> (forall b, b \in a -> P b)-> P a) ->
  forall x, isWf x -> P x.

Lemma isWf_zero: isWf zero.

Lemma isWf_pair : forall x y,
  isWf x -> isWf y -> isWf (pair x y).

Lemma isWf_power : forall x, isWf x -> isWf (power x).

Lemma isWf_union : forall x, isWf x -> isWf (union x).

Lemma isWf_subset : forall x P, isWf x -> isWf (subset x P).

Lemma isWf_succ : forall n, isWf n -> isWf (succ n).

Lemma isWf_N : isWf N.

Lemma isWf_antirefl : forall x, isWf x -> ~ x \in x.

Require Import ZFrepl.

Lemma isWf_repl : forall x R,
  repl_rel x R ->
  (forall a b, a \in x -> R a b -> isWf b) ->
  isWf (repl x R).

End WellFoundedSets.