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