Library ZFrank
Require Import ZF ZFnats ZFord ZFstable ZFfix.
Definition VN := TI power.
Instance VN_morph : morph1 VN.
do 2 red; intros.
apply TI_morph; trivial.
Qed.
Lemma VN_def : ∀ x z,
isOrd x ->
(z ∈ VN x <-> exists2 y, y ∈ x & z ⊆ VN y).
split; intros.
apply TI_elim in H0; auto with *.
destruct H0.
exists x0; trivial.
red; intros.
eauto using power_elim.
destruct H0.
apply TI_intro with x0; auto with *.
apply power_intro; auto.
Qed.
Lemma VN_trans : ∀ o x y,
isOrd o ->
x ∈ VN o ->
y ∈ x ->
y ∈ VN o.
intros.
rewrite VN_def in H0; trivial.
destruct H0.
apply H2 in H1.
revert H1; apply TI_incl; auto with *.
apply power_mono.
Qed.
Lemma VN_incl : ∀ o x y,
isOrd o ->
y ⊆ x ->
x ∈ VN o ->
y ∈ VN o.
intros.
rewrite VN_def in H1|-*; auto with *.
destruct H1.
exists x0; trivial.
transitivity x; trivial.
Qed.
Lemma VN_mono : ∀ o x,
isOrd o ->
lt x o -> VN x ∈ VN o.
intros.
rewrite (VN_def o); trivial.
exists x; auto with *.
Qed.
Lemma VN_mono_le : ∀ o o',
isOrd o ->
isOrd o' ->
o ⊆ o' ->
VN o ⊆ VN o'.
red; intros.
rewrite VN_def in H2|-*; trivial.
destruct H2.
exists x; auto.
Qed.
Lemma VN_stable : stable_ord VN.
unfold VN.
apply TI_stable.
apply power_mono.
apply power_stable.
Qed.
Lemma VN_compl : ∀ x z, isOrd x -> isOrd z -> z ∈ VN x -> VN z ∈ VN x.
intros x z xo; revert z.
induction xo using isOrd_ind; intros.
rewrite VN_def in H2|-*; auto with *.
destruct H2.
exists x0; trivial.
red; intros.
rewrite VN_def in H4; auto with *.
destruct H4.
apply VN_incl with (VN x1); eauto using isOrd_inv.
Qed.
Lemma VN_intro :
∀ x, isOrd x -> x ⊆ VN x.
induction 1 using isOrd_ind; red; intros.
rewrite VN_def; trivial.
eauto.
Qed.
Lemma VN_succ : ∀ x, isOrd x -> power (VN x) == VN (osucc x).
intros.
unfold VN.
symmetry; apply TI_mono_succ; trivial.
apply power_mono.
Qed.
Lemma VN_ord_inv : ∀ o x, isOrd o -> isOrd x -> x ∈ VN o -> lt x o.
intros o x xo; revert x.
induction xo using isOrd_ind; intros.
rewrite VN_def in H2; trivial; destruct H2.
apply isOrd_plump with x0; trivial.
red; intros.
apply H0; auto.
apply isOrd_inv with x; trivial.
Qed.
Lemma VN_subset : ∀ o x P, isOrd o -> x ∈ VN o -> subset x P ∈ VN o.
intros.
apply VN_incl with x; trivial.
red; intros.
apply subset_elim1 in H1; trivial.
Qed.
Lemma VN_union : ∀ o x, isOrd o -> x ∈ VN o -> union x ∈ VN o.
intros.
rewrite VN_def in H0|-*; trivial.
destruct H0.
exists x0; trivial.
red; intros.
apply union_elim in H2; destruct H2.
apply VN_trans with x1; eauto using isOrd_inv.
Qed.
Lemma VNsucc_power : ∀ o x,
isOrd o ->
x ∈ VN o ->
power x ∈ VN (osucc o).
intros.
rewrite <- VN_succ; trivial.
apply power_intro; intros.
apply VN_incl with x; trivial.
red; eauto using power_elim.
Qed.
Lemma VNsucc_pair : ∀ o x y, isOrd o ->
x ∈ VN o -> y ∈ VN o -> pair x y ∈ VN (osucc o).
intros.
rewrite <- VN_succ; trivial.
rewrite power_ax; intros.
apply pair_elim in H2; destruct H2; rewrite H2; trivial.
Qed.
Lemma VNlim_def : ∀ o x, limitOrd o ->
(x ∈ VN o <-> exists2 o', lt o' o & x ∈ VN o').
destruct 1; rewrite VN_def; trivial.
split; intros.
destruct H1.
exists (osucc x0); auto.
rewrite <- VN_succ; auto.
rewrite power_ax; auto.
apply isOrd_inv with o; trivial.
destruct H1.
exists x0; trivial.
red; intros.
apply VN_trans with x; trivial.
apply isOrd_inv with o; trivial.
Qed.
Lemma VNlim_power : ∀ o x, limitOrd o -> x ∈ VN o -> power x ∈ VN o.
intros.
rewrite VNlim_def in H0|-*; trivial.
destruct H0.
exists (osucc x0).
apply H; trivial.
apply VNsucc_power; trivial.
apply isOrd_inv with o; trivial.
apply H.
Qed.
Lemma VNlim_pair : ∀ o x y, limitOrd o ->
x ∈ VN o -> y ∈ VN o -> pair x y ∈ VN o.
intros o x y lim; intros.
rewrite VNlim_def in H,H0|-*; auto.
destruct H; destruct H0.
assert (o0 : isOrd x0) by eauto using isOrd_inv.
assert (o1 : isOrd x1) by eauto using isOrd_inv.
exists (osucc (x0 ⊔ x1)).
apply lim.
apply osup2_lt; auto.
apply VNsucc_pair.
apply isOrd_osup2; trivial.
revert H1; apply VN_mono_le; trivial; [apply isOrd_osup2|apply osup2_incl1]; auto.
revert H2; apply VN_mono_le; trivial; [apply isOrd_osup2|apply osup2_incl2]; auto.
Qed.
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)))).
unfold func; intros.
apply VN_subset; auto.
unfold rel.
apply VNsucc_power; auto.
unfold ZFpairs.prodcart.
apply VN_subset; auto.
apply VNsucc_power; auto.
apply VNsucc_power; auto.
unfold union2.
apply VN_union; auto.
apply VNsucc_pair; trivial.
Qed.
Require Import ZFwf.
Lemma VN_wf o x : isOrd o -> x ∈ VN o -> isWf x.
intros oo; revert x; induction oo using isOrd_ind.
intros.
apply isWf_intro; intros.
rewrite VN_def in H1; trivial; destruct H1.
apply H3 in H2; eauto.
Qed.
Lemma VN_osup2 o :
isOrd o ->
∀ x y,
x ∈ VN o ->
y ∈ VN o ->
x ⊔ y ∈ VN o.
induction 1 using isOrd_ind; intros.
rewrite VN_def in H2,H3|-*; trivial.
destruct H2.
destruct H3.
exists (x0 ⊔ x1).
apply osup2_lt; trivial.
red; intros.
rewrite osup2_ax in H6.
2:apply isWf_intro; intros; eauto using VN_wf, isOrd_inv.
assert (x ⊆ VN (x0 ⊔ x1)).
red; intros.
apply H4 in H7; revert H7; apply VN_mono_le.
apply isOrd_inv with y; trivial.
apply isOrd_osup2; eauto using isOrd_inv.
apply osup2_incl1; eauto using isOrd_inv.
assert (y0 ⊆ VN (x0 ⊔ x1)).
red; intros.
apply H5 in H8; revert H8; apply VN_mono_le.
apply isOrd_inv with y; trivial.
apply isOrd_osup2; eauto using isOrd_inv.
apply osup2_incl2; eauto using isOrd_inv.
destruct H6 as [?|[?|(x',?,(y',?,?))]]; auto.
rewrite H10; apply H1; auto.
apply osup2_lt; trivial.
Qed.
Lemma VN_N : N ⊆ VN omega.
red; intros.
elim H using N_ind; simpl; intros.
rewrite <- H1; trivial.
apply VN_intro; trivial.
apply zero_omega.
unfold succ.
apply VN_union; trivial.
apply VNlim_pair; trivial.
apply VNlim_pair; trivial.
Qed.
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.
intros.
apply ord_sup_typ; trivial; intros.
apply H0; trivial.
do 2 red; intros; apply H3; trivial.
apply VN_incl with (VN omega); trivial.
apply VN_N.
apply VN_mono; trivial.
Qed.
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.
intros.
apply VN_ord_inv; trivial.
apply isOrd_osup; eauto using isOrd_inv.
apply osup_univ; intros; trivial.
apply isOrd_inv with o; auto.
apply H0; trivial.
rewrite VN_def in H5; trivial; destruct H5.
apply H9 in H7; apply H9 in H8.
rewrite VN_def; trivial.
exists x1; trivial.
red; intros.
apply singl_elim in H10; rewrite H10; apply VN_osup2; eauto using isOrd_inv.
apply VN_incl with (VN omega); trivial. apply VN_N.
apply VN_mono; trivial.
apply VN_intro; auto.
apply H4; trivial.
Qed.
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.
red; intros.
apply mu_reg; trivial; intros.
apply repl_rel_fun; trivial.
rewrite H3; auto.
Qed.
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.
intros.
apply VNlim_pair; trivial.
Qed.
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.
red; intros.
pose (mu' := osup (subset a (fun x => F x ∈ mu)) F).
assert (ext : ext_fun (subset a (fun x : set => F x ∈ mu)) F).
red; red; intros.
apply H0; trivial.
apply subset_elim1 in H1; trivial.
assert (mu' ∈ mu).
unfold mu'; apply VN_reg_ord; auto.
exact VN_regular_weaker.
apply VN_incl with a; trivial.
red; intros.
apply subset_elim1 in H1; trivial.
intros.
rewrite subset_ax in H1; destruct H1.
destruct H2.
setoid_replace (F y) with (F x); trivial.
apply H0; auto.
assert (isOrd mu').
eauto using isOrd_inv.
exists (osucc mu').
apply mu_lim; trivial.
red; intros.
apply (lt_antirefl mu'); trivial.
unfold mu' at 2.
apply osup_intro with x; trivial.
apply subset_intro; trivial.
rewrite <- H4.
apply mu_lim; trivial.
rewrite <- H4; apply lt_osucc; auto.
Qed.
Require Import ZFcard.
Lemma VNcard : ∀ x,
x ∈ VN mu -> lt_card x mu.
red; red; intros.
destruct H0 as (R,?,(?,?)).
rewrite VN_def in H; auto; destruct H.
pose (mu' := osup (subset x (fun x' => exists2 w, w ∈ mu & R w x'))
(fun x' => uchoice (fun o => o ∈ mu /\ R o x'))).
assert (ext : ext_fun (subset x (fun x' => exists2 w, w ∈ mu & R w x'))
(fun x' => uchoice (fun o => o ∈ mu /\ R o x'))).
red; red; intros.
apply uchoice_morph_raw.
red; intros.
rewrite H5; rewrite H6; reflexivity.
assert (mu' ∈ mu).
unfold mu'; apply VN_reg_ord; auto.
exact VN_regular_weaker.
apply VN_subset; trivial.
rewrite VN_def; trivial.
exists x0; trivial.
intros.
rewrite subset_ax in H4; destruct H4.
destruct H5.
destruct H6.
rewrite <- H5 in H7; clear x1 H5.
assert (uchoice_pred (fun o => o ∈ mu /\ R o y)).
split; [|split]; intros; eauto.
rewrite <- H5; trivial.
destruct H5; destruct H8.
eauto with *.
destruct (uchoice_def _ H5); trivial.
assert (mu == mu').
apply eq_intro; intros.
destruct (H1 _ (mu_lim _ H5)).
unfold mu'.
apply osup_intro with (x:=x1).
do 2 red; intros; apply uchoice_morph_raw.
red; intros.
rewrite H9; rewrite H10; reflexivity.
apply subset_intro; trivial.
exists (osucc z); trivial.
apply mu_lim; trivial.
rewrite <- (uchoice_ext _ (osucc z)).
apply lt_osucc; eauto using isOrd_inv.
split; [|split]; intros; eauto.
rewrite <- H8; trivial.
exists (osucc z); auto.
split; auto.
apply mu_lim; trivial.
destruct H8; destruct H9.
eauto with *.
split; trivial.
apply mu_lim; trivial.
apply isOrd_trans with mu'; trivial.
rewrite <- H5 in H4.
revert H4; apply lt_antirefl; trivial.
Qed.
Lemma reg_card : isCard mu.
split; trivial.
intros.
apply VNcard.
apply VN_intro; trivial.
Qed.
End UnionClosure.
Definition VN := TI power.
Instance VN_morph : morph1 VN.
do 2 red; intros.
apply TI_morph; trivial.
Qed.
Lemma VN_def : ∀ x z,
isOrd x ->
(z ∈ VN x <-> exists2 y, y ∈ x & z ⊆ VN y).
split; intros.
apply TI_elim in H0; auto with *.
destruct H0.
exists x0; trivial.
red; intros.
eauto using power_elim.
destruct H0.
apply TI_intro with x0; auto with *.
apply power_intro; auto.
Qed.
Lemma VN_trans : ∀ o x y,
isOrd o ->
x ∈ VN o ->
y ∈ x ->
y ∈ VN o.
intros.
rewrite VN_def in H0; trivial.
destruct H0.
apply H2 in H1.
revert H1; apply TI_incl; auto with *.
apply power_mono.
Qed.
Lemma VN_incl : ∀ o x y,
isOrd o ->
y ⊆ x ->
x ∈ VN o ->
y ∈ VN o.
intros.
rewrite VN_def in H1|-*; auto with *.
destruct H1.
exists x0; trivial.
transitivity x; trivial.
Qed.
Lemma VN_mono : ∀ o x,
isOrd o ->
lt x o -> VN x ∈ VN o.
intros.
rewrite (VN_def o); trivial.
exists x; auto with *.
Qed.
Lemma VN_mono_le : ∀ o o',
isOrd o ->
isOrd o' ->
o ⊆ o' ->
VN o ⊆ VN o'.
red; intros.
rewrite VN_def in H2|-*; trivial.
destruct H2.
exists x; auto.
Qed.
Lemma VN_stable : stable_ord VN.
unfold VN.
apply TI_stable.
apply power_mono.
apply power_stable.
Qed.
Lemma VN_compl : ∀ x z, isOrd x -> isOrd z -> z ∈ VN x -> VN z ∈ VN x.
intros x z xo; revert z.
induction xo using isOrd_ind; intros.
rewrite VN_def in H2|-*; auto with *.
destruct H2.
exists x0; trivial.
red; intros.
rewrite VN_def in H4; auto with *.
destruct H4.
apply VN_incl with (VN x1); eauto using isOrd_inv.
Qed.
Lemma VN_intro :
∀ x, isOrd x -> x ⊆ VN x.
induction 1 using isOrd_ind; red; intros.
rewrite VN_def; trivial.
eauto.
Qed.
Lemma VN_succ : ∀ x, isOrd x -> power (VN x) == VN (osucc x).
intros.
unfold VN.
symmetry; apply TI_mono_succ; trivial.
apply power_mono.
Qed.
Lemma VN_ord_inv : ∀ o x, isOrd o -> isOrd x -> x ∈ VN o -> lt x o.
intros o x xo; revert x.
induction xo using isOrd_ind; intros.
rewrite VN_def in H2; trivial; destruct H2.
apply isOrd_plump with x0; trivial.
red; intros.
apply H0; auto.
apply isOrd_inv with x; trivial.
Qed.
Lemma VN_subset : ∀ o x P, isOrd o -> x ∈ VN o -> subset x P ∈ VN o.
intros.
apply VN_incl with x; trivial.
red; intros.
apply subset_elim1 in H1; trivial.
Qed.
Lemma VN_union : ∀ o x, isOrd o -> x ∈ VN o -> union x ∈ VN o.
intros.
rewrite VN_def in H0|-*; trivial.
destruct H0.
exists x0; trivial.
red; intros.
apply union_elim in H2; destruct H2.
apply VN_trans with x1; eauto using isOrd_inv.
Qed.
Lemma VNsucc_power : ∀ o x,
isOrd o ->
x ∈ VN o ->
power x ∈ VN (osucc o).
intros.
rewrite <- VN_succ; trivial.
apply power_intro; intros.
apply VN_incl with x; trivial.
red; eauto using power_elim.
Qed.
Lemma VNsucc_pair : ∀ o x y, isOrd o ->
x ∈ VN o -> y ∈ VN o -> pair x y ∈ VN (osucc o).
intros.
rewrite <- VN_succ; trivial.
rewrite power_ax; intros.
apply pair_elim in H2; destruct H2; rewrite H2; trivial.
Qed.
Lemma VNlim_def : ∀ o x, limitOrd o ->
(x ∈ VN o <-> exists2 o', lt o' o & x ∈ VN o').
destruct 1; rewrite VN_def; trivial.
split; intros.
destruct H1.
exists (osucc x0); auto.
rewrite <- VN_succ; auto.
rewrite power_ax; auto.
apply isOrd_inv with o; trivial.
destruct H1.
exists x0; trivial.
red; intros.
apply VN_trans with x; trivial.
apply isOrd_inv with o; trivial.
Qed.
Lemma VNlim_power : ∀ o x, limitOrd o -> x ∈ VN o -> power x ∈ VN o.
intros.
rewrite VNlim_def in H0|-*; trivial.
destruct H0.
exists (osucc x0).
apply H; trivial.
apply VNsucc_power; trivial.
apply isOrd_inv with o; trivial.
apply H.
Qed.
Lemma VNlim_pair : ∀ o x y, limitOrd o ->
x ∈ VN o -> y ∈ VN o -> pair x y ∈ VN o.
intros o x y lim; intros.
rewrite VNlim_def in H,H0|-*; auto.
destruct H; destruct H0.
assert (o0 : isOrd x0) by eauto using isOrd_inv.
assert (o1 : isOrd x1) by eauto using isOrd_inv.
exists (osucc (x0 ⊔ x1)).
apply lim.
apply osup2_lt; auto.
apply VNsucc_pair.
apply isOrd_osup2; trivial.
revert H1; apply VN_mono_le; trivial; [apply isOrd_osup2|apply osup2_incl1]; auto.
revert H2; apply VN_mono_le; trivial; [apply isOrd_osup2|apply osup2_incl2]; auto.
Qed.
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)))).
unfold func; intros.
apply VN_subset; auto.
unfold rel.
apply VNsucc_power; auto.
unfold ZFpairs.prodcart.
apply VN_subset; auto.
apply VNsucc_power; auto.
apply VNsucc_power; auto.
unfold union2.
apply VN_union; auto.
apply VNsucc_pair; trivial.
Qed.
Require Import ZFwf.
Lemma VN_wf o x : isOrd o -> x ∈ VN o -> isWf x.
intros oo; revert x; induction oo using isOrd_ind.
intros.
apply isWf_intro; intros.
rewrite VN_def in H1; trivial; destruct H1.
apply H3 in H2; eauto.
Qed.
Lemma VN_osup2 o :
isOrd o ->
∀ x y,
x ∈ VN o ->
y ∈ VN o ->
x ⊔ y ∈ VN o.
induction 1 using isOrd_ind; intros.
rewrite VN_def in H2,H3|-*; trivial.
destruct H2.
destruct H3.
exists (x0 ⊔ x1).
apply osup2_lt; trivial.
red; intros.
rewrite osup2_ax in H6.
2:apply isWf_intro; intros; eauto using VN_wf, isOrd_inv.
assert (x ⊆ VN (x0 ⊔ x1)).
red; intros.
apply H4 in H7; revert H7; apply VN_mono_le.
apply isOrd_inv with y; trivial.
apply isOrd_osup2; eauto using isOrd_inv.
apply osup2_incl1; eauto using isOrd_inv.
assert (y0 ⊆ VN (x0 ⊔ x1)).
red; intros.
apply H5 in H8; revert H8; apply VN_mono_le.
apply isOrd_inv with y; trivial.
apply isOrd_osup2; eauto using isOrd_inv.
apply osup2_incl2; eauto using isOrd_inv.
destruct H6 as [?|[?|(x',?,(y',?,?))]]; auto.
rewrite H10; apply H1; auto.
apply osup2_lt; trivial.
Qed.
Lemma VN_N : N ⊆ VN omega.
red; intros.
elim H using N_ind; simpl; intros.
rewrite <- H1; trivial.
apply VN_intro; trivial.
apply zero_omega.
unfold succ.
apply VN_union; trivial.
apply VNlim_pair; trivial.
apply VNlim_pair; trivial.
Qed.
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.
intros.
apply ord_sup_typ; trivial; intros.
apply H0; trivial.
do 2 red; intros; apply H3; trivial.
apply VN_incl with (VN omega); trivial.
apply VN_N.
apply VN_mono; trivial.
Qed.
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.
intros.
apply VN_ord_inv; trivial.
apply isOrd_osup; eauto using isOrd_inv.
apply osup_univ; intros; trivial.
apply isOrd_inv with o; auto.
apply H0; trivial.
rewrite VN_def in H5; trivial; destruct H5.
apply H9 in H7; apply H9 in H8.
rewrite VN_def; trivial.
exists x1; trivial.
red; intros.
apply singl_elim in H10; rewrite H10; apply VN_osup2; eauto using isOrd_inv.
apply VN_incl with (VN omega); trivial. apply VN_N.
apply VN_mono; trivial.
apply VN_intro; auto.
apply H4; trivial.
Qed.
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.
red; intros.
apply mu_reg; trivial; intros.
apply repl_rel_fun; trivial.
rewrite H3; auto.
Qed.
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.
intros.
apply VNlim_pair; trivial.
Qed.
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.
red; intros.
pose (mu' := osup (subset a (fun x => F x ∈ mu)) F).
assert (ext : ext_fun (subset a (fun x : set => F x ∈ mu)) F).
red; red; intros.
apply H0; trivial.
apply subset_elim1 in H1; trivial.
assert (mu' ∈ mu).
unfold mu'; apply VN_reg_ord; auto.
exact VN_regular_weaker.
apply VN_incl with a; trivial.
red; intros.
apply subset_elim1 in H1; trivial.
intros.
rewrite subset_ax in H1; destruct H1.
destruct H2.
setoid_replace (F y) with (F x); trivial.
apply H0; auto.
assert (isOrd mu').
eauto using isOrd_inv.
exists (osucc mu').
apply mu_lim; trivial.
red; intros.
apply (lt_antirefl mu'); trivial.
unfold mu' at 2.
apply osup_intro with x; trivial.
apply subset_intro; trivial.
rewrite <- H4.
apply mu_lim; trivial.
rewrite <- H4; apply lt_osucc; auto.
Qed.
Require Import ZFcard.
Lemma VNcard : ∀ x,
x ∈ VN mu -> lt_card x mu.
red; red; intros.
destruct H0 as (R,?,(?,?)).
rewrite VN_def in H; auto; destruct H.
pose (mu' := osup (subset x (fun x' => exists2 w, w ∈ mu & R w x'))
(fun x' => uchoice (fun o => o ∈ mu /\ R o x'))).
assert (ext : ext_fun (subset x (fun x' => exists2 w, w ∈ mu & R w x'))
(fun x' => uchoice (fun o => o ∈ mu /\ R o x'))).
red; red; intros.
apply uchoice_morph_raw.
red; intros.
rewrite H5; rewrite H6; reflexivity.
assert (mu' ∈ mu).
unfold mu'; apply VN_reg_ord; auto.
exact VN_regular_weaker.
apply VN_subset; trivial.
rewrite VN_def; trivial.
exists x0; trivial.
intros.
rewrite subset_ax in H4; destruct H4.
destruct H5.
destruct H6.
rewrite <- H5 in H7; clear x1 H5.
assert (uchoice_pred (fun o => o ∈ mu /\ R o y)).
split; [|split]; intros; eauto.
rewrite <- H5; trivial.
destruct H5; destruct H8.
eauto with *.
destruct (uchoice_def _ H5); trivial.
assert (mu == mu').
apply eq_intro; intros.
destruct (H1 _ (mu_lim _ H5)).
unfold mu'.
apply osup_intro with (x:=x1).
do 2 red; intros; apply uchoice_morph_raw.
red; intros.
rewrite H9; rewrite H10; reflexivity.
apply subset_intro; trivial.
exists (osucc z); trivial.
apply mu_lim; trivial.
rewrite <- (uchoice_ext _ (osucc z)).
apply lt_osucc; eauto using isOrd_inv.
split; [|split]; intros; eauto.
rewrite <- H8; trivial.
exists (osucc z); auto.
split; auto.
apply mu_lim; trivial.
destruct H8; destruct H9.
eauto with *.
split; trivial.
apply mu_lim; trivial.
apply isOrd_trans with mu'; trivial.
rewrite <- H5 in H4.
revert H4; apply lt_antirefl; trivial.
Qed.
Lemma reg_card : isCard mu.
split; trivial.
intros.
apply VNcard.
apply VN_intro; trivial.
Qed.
End UnionClosure.