# Library ZFfix

Require Import ZF.
Require Import ZFrelations.
Import IZF.

Require Import ZFord.
Require Import ZFnats.

Section IterMonotone.

Variable F : set -> set.
Variable Fmono : Proper (incl_set ==> incl_set) F.

Instance Fmono_morph: Proper (eq_set ==> eq_set) F.

Qed.
Hint Resolve Fmono_morph.

Lemma TI_mono : increasing (TI F).

Lemma TI_incl : forall o, isOrd o ->
forall o', lt o' o ->
TI F o' \incl TI F o.

Lemma TI_mono_succ : forall o,
isOrd o ->
TI F (osucc o) == F (TI F o).

Lemma TI_pre_fix : forall fx o,
isOrd o ->
F fx \incl fx ->
TI F o \incl fx.

End IterMonotone.

Definition VN := TI power.

Lemma VN_trans : forall o x y,
isOrd o ->
x \in VN o ->
y \in x ->
y \in VN o.

Lemma VN_incl : forall o x y,
isOrd o ->
y \incl x ->
x \in VN o ->
y \in VN o.

Lemma VNsucc_power : forall o x,
isOrd o ->
x \in VN o ->
power x \in VN (osucc o).

Lemma VNlim_clos_power : forall o x, limitOrd o -> x \in VN o -> power x \in VN o.

Lemma VN_clos_union : forall o x, isOrd o -> x \in VN o -> union x \in VN o.

Require Import ZFcard.
Require Import ZFrepl.
Require Import ZFordcl ZFord_equiv.
Import ZFord.

Lemma repl_rel_incl : forall x y R,
x \incl y ->
repl_rel y R ->
repl_rel x R.

Section Inaccessible.

Variable mu : set.
Variable mu_ord : isOrd mu.
Variable mu_lim : forall x, lt x mu -> lt (osucc x) mu.
Variable mu_regular : regular mu.

Lemma VNcard : forall x,
x \in VN mu -> lt_card x mu.

Lemma VNlim_clos_union_repl : forall I R,
repl_rel I R ->
I \in VN mu ->
(forall x y, x \in I -> R x y -> y \in VN mu) ->
union (repl I R) \in VN mu.

End Inaccessible.

Section InaccessibleCard.

Variable mu : set.
Variable mu_card : isCard mu.
Variable mu_lim : forall x, lt x mu -> lt (osucc x) mu.
Variable mu_regular : regular_card mu.

Let mu_ord : isOrd mu.
Qed.
Let mu_lt : forall x, lt x mu -> lt_card x mu.
Qed.

Lemma lt_card_lt : forall x, isOrd x -> lt_card x mu -> lt x mu.

Lemma VNcard' : forall x,
x \in VN mu -> lt_card x mu.

Lemma VNreg_clos_sup : forall I F,
ext_fun I F ->
I \in VN mu ->
(forall x, x \in I -> F x \in VN mu) ->
sup I F \in VN mu.

End InaccessibleCard.