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