# 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.