Library ZFrank
Require Import ZF ZFnats ZFord ZFstable ZFfix.
Definition VN := TI power.
Instance VN_morph : morph1 VN.
Qed.
Lemma VN_def : ∀ x z,
isOrd x ->
(z ∈ VN x <-> exists2 y, y ∈ x & z ⊆ VN y).
Lemma VN_trans : ∀ o x y,
isOrd o ->
x ∈ VN o ->
y ∈ x ->
y ∈ VN o.
Lemma VN_incl : ∀ o x y,
isOrd o ->
y ⊆ x ->
x ∈ VN o ->
y ∈ VN o.
Lemma VN_mono : ∀ o x,
isOrd o ->
lt x o -> VN x ∈ VN o.
Lemma VN_mono_le : ∀ o o',
isOrd o ->
isOrd o' ->
o ⊆ o' ->
VN o ⊆ VN o'.
Lemma VN_stable : stable_ord VN.
Lemma VN_compl : ∀ x z, isOrd x -> isOrd z -> z ∈ VN x -> VN z ∈ VN x.
Lemma VN_intro :
∀ x, isOrd x -> x ⊆ VN x.
Lemma VN_succ : ∀ x, isOrd x -> power (VN x) == VN (osucc x).
Lemma VN_ord_inv : ∀ o x, isOrd o -> isOrd x -> x ∈ VN o -> lt x o.
Lemma VN_subset : ∀ o x P, isOrd o -> x ∈ VN o -> subset x P ∈ VN o.
Lemma VN_union : ∀ o x, isOrd o -> x ∈ VN o -> union x ∈ VN o.
Lemma VNsucc_power : ∀ o x,
isOrd o ->
x ∈ VN o ->
power x ∈ VN (osucc o).
Lemma VNsucc_pair : ∀ o x y, isOrd o ->
x ∈ VN o -> y ∈ VN o -> pair x y ∈ VN (osucc o).
Lemma VNlim_def : ∀ o x, limitOrd o ->
(x ∈ VN o <-> exists2 o', lt o' o & x ∈ VN o').
Lemma VNlim_power : ∀ o x, limitOrd o -> x ∈ VN o -> power x ∈ VN o.
Lemma VNlim_pair : ∀ o x y, limitOrd o ->
x ∈ VN o -> y ∈ VN o -> pair x y ∈ VN o.
Require Import ZFrelations.
Lemma VN_func : ∀ o A B,
isOrd o ->
A ∈ VN o ->
B ∈ VN o ->
func A B ∈ VN (osucc (osucc (osucc (osucc o)))).
Require Import ZFwf.
Lemma VN_wf o x : isOrd o -> x ∈ VN o -> isWf x.
Lemma VN_osup2 o :
isOrd o ->
∀ x y,
x ∈ VN o ->
y ∈ VN o ->
x ⊔ y ∈ VN o.
Lemma VN_N : N ⊆ VN omega.
Definition VN_regular o :=
∀ x F,
ext_fun x F ->
x ∈ VN o ->
(∀ y, y ∈ x -> F y ∈ VN o) ->
sup x F ∈ VN o.
Definition bound_ord A o :=
∀ F, ext_fun A F ->
(∀ n, n ∈ A -> lt (F n) o) ->
lt (osup A F) o.
Lemma VN_ord_sup F o :
isOrd o ->
VN_regular o ->
omega ∈ o ->
(∀ n, F n ∈ VN o) ->
ord_sup F ∈ VN o.
Lemma VN_reg_ord : ∀ o,
isOrd o ->
VN_regular o ->
omega ∈ o ->
∀ x F,
ext_fun x F ->
x ∈ VN o ->
(∀ y, y ∈ x -> lt (F y) o) ->
lt (osup x F) o.
Definition VN_inaccessible o :=
limitOrd o /\ VN_regular o.
Require Import ZFrepl.
Definition VN_regular_rel o :=
∀ x R,
repl_rel x R ->
x ∈ VN o ->
(∀ y z, y ∈ x -> R y z -> z ∈ VN o) ->
union (repl x R) ∈ VN o.
Definition VN_inaccessible_rel o :=
limitOrd o /\ VN_regular_rel o.
Section UnionClosure.
Variable mu : set.
Hypothesis mu_ord : isOrd mu.
Hypothesis mu_lim : ∀ x, lt x mu -> lt (osucc x) mu.
Hypothesis mu_reg : VN_regular_rel mu.
Hypothesis mu_inf : omega ∈ mu.
Lemma VN_regular_weaker : VN_regular mu.
Let mul : limitOrd mu := conj mu_ord mu_lim.
Lemma VN_clos_pair : ∀ x y,
x ∈ VN mu -> y ∈ VN mu -> pair x y ∈ VN mu.
Definition lt_cardf a b :=
∀ F, ext_fun a F ->
exists2 y, y ∈ b & ∀ x, x ∈ a -> ~ y == F x.
Lemma VN_cardf : ∀ a,
a ∈ VN mu -> lt_cardf a mu.
Require Import ZFcard.
Lemma VNcard : ∀ x,
x ∈ VN mu -> lt_card x mu.
Lemma reg_card : isCard mu.
End UnionClosure.
Definition VN := TI power.
Instance VN_morph : morph1 VN.
Qed.
Lemma VN_def : ∀ x z,
isOrd x ->
(z ∈ VN x <-> exists2 y, y ∈ x & z ⊆ VN y).
Lemma VN_trans : ∀ o x y,
isOrd o ->
x ∈ VN o ->
y ∈ x ->
y ∈ VN o.
Lemma VN_incl : ∀ o x y,
isOrd o ->
y ⊆ x ->
x ∈ VN o ->
y ∈ VN o.
Lemma VN_mono : ∀ o x,
isOrd o ->
lt x o -> VN x ∈ VN o.
Lemma VN_mono_le : ∀ o o',
isOrd o ->
isOrd o' ->
o ⊆ o' ->
VN o ⊆ VN o'.
Lemma VN_stable : stable_ord VN.
Lemma VN_compl : ∀ x z, isOrd x -> isOrd z -> z ∈ VN x -> VN z ∈ VN x.
Lemma VN_intro :
∀ x, isOrd x -> x ⊆ VN x.
Lemma VN_succ : ∀ x, isOrd x -> power (VN x) == VN (osucc x).
Lemma VN_ord_inv : ∀ o x, isOrd o -> isOrd x -> x ∈ VN o -> lt x o.
Lemma VN_subset : ∀ o x P, isOrd o -> x ∈ VN o -> subset x P ∈ VN o.
Lemma VN_union : ∀ o x, isOrd o -> x ∈ VN o -> union x ∈ VN o.
Lemma VNsucc_power : ∀ o x,
isOrd o ->
x ∈ VN o ->
power x ∈ VN (osucc o).
Lemma VNsucc_pair : ∀ o x y, isOrd o ->
x ∈ VN o -> y ∈ VN o -> pair x y ∈ VN (osucc o).
Lemma VNlim_def : ∀ o x, limitOrd o ->
(x ∈ VN o <-> exists2 o', lt o' o & x ∈ VN o').
Lemma VNlim_power : ∀ o x, limitOrd o -> x ∈ VN o -> power x ∈ VN o.
Lemma VNlim_pair : ∀ o x y, limitOrd o ->
x ∈ VN o -> y ∈ VN o -> pair x y ∈ VN o.
Require Import ZFrelations.
Lemma VN_func : ∀ o A B,
isOrd o ->
A ∈ VN o ->
B ∈ VN o ->
func A B ∈ VN (osucc (osucc (osucc (osucc o)))).
Require Import ZFwf.
Lemma VN_wf o x : isOrd o -> x ∈ VN o -> isWf x.
Lemma VN_osup2 o :
isOrd o ->
∀ x y,
x ∈ VN o ->
y ∈ VN o ->
x ⊔ y ∈ VN o.
Lemma VN_N : N ⊆ VN omega.
Definition VN_regular o :=
∀ x F,
ext_fun x F ->
x ∈ VN o ->
(∀ y, y ∈ x -> F y ∈ VN o) ->
sup x F ∈ VN o.
Definition bound_ord A o :=
∀ F, ext_fun A F ->
(∀ n, n ∈ A -> lt (F n) o) ->
lt (osup A F) o.
Lemma VN_ord_sup F o :
isOrd o ->
VN_regular o ->
omega ∈ o ->
(∀ n, F n ∈ VN o) ->
ord_sup F ∈ VN o.
Lemma VN_reg_ord : ∀ o,
isOrd o ->
VN_regular o ->
omega ∈ o ->
∀ x F,
ext_fun x F ->
x ∈ VN o ->
(∀ y, y ∈ x -> lt (F y) o) ->
lt (osup x F) o.
Definition VN_inaccessible o :=
limitOrd o /\ VN_regular o.
Require Import ZFrepl.
Definition VN_regular_rel o :=
∀ x R,
repl_rel x R ->
x ∈ VN o ->
(∀ y z, y ∈ x -> R y z -> z ∈ VN o) ->
union (repl x R) ∈ VN o.
Definition VN_inaccessible_rel o :=
limitOrd o /\ VN_regular_rel o.
Section UnionClosure.
Variable mu : set.
Hypothesis mu_ord : isOrd mu.
Hypothesis mu_lim : ∀ x, lt x mu -> lt (osucc x) mu.
Hypothesis mu_reg : VN_regular_rel mu.
Hypothesis mu_inf : omega ∈ mu.
Lemma VN_regular_weaker : VN_regular mu.
Let mul : limitOrd mu := conj mu_ord mu_lim.
Lemma VN_clos_pair : ∀ x y,
x ∈ VN mu -> y ∈ VN mu -> pair x y ∈ VN mu.
Definition lt_cardf a b :=
∀ F, ext_fun a F ->
exists2 y, y ∈ b & ∀ x, x ∈ a -> ~ y == F x.
Lemma VN_cardf : ∀ a,
a ∈ VN mu -> lt_cardf a mu.
Require Import ZFcard.
Lemma VNcard : ∀ x,
x ∈ VN mu -> lt_card x mu.
Lemma reg_card : isCard mu.
End UnionClosure.