proposition: Lemma universe_inaccessible_mo2 : let U := (fun z => inc z (universe a)) in [/\ ZF_axioms1 U inc, comprehensionA U inc, infiniteA U inc, choiceA U inc & foundationA U inc] /\ Ufacts U a.
proof: Proof. move: ia => [[[/infinite_card_limit2 la _] _] _]. move:(universe_mo3 la) => [ [p1 p2 p3 p4 p5] [ap ap'] p6 p7 p8]. move: universe_inaccessible_mo1 => p9. have p10: ZF_axioms1 (inc^~ (universe a)) inc by []. have loa: omega0 <o a. rewrite -aleph0E (inaccessible_pr1 (proj1 ia)). by apply /aleph_lt_lto; apply: limit_pos. move /p6: (loa) => p6'. move:(proj32_1 loa) => oa. move: (universe_mo' oa) => [pa pb]. move: (universe_mo1 pa pb) =>[r1 [r2 [r3 [r4 [r5 [r6 [r7 [r8 [r9 [r10 [r10b r11]]]]]]]]]]]. pose U x := inc x (universe a). have sa: forall x y, U x -> U y -> (subU U x y <-> sub x y). move => x y ux uy; split. move => h t tx; apply:h => //; apply: (pa _ _ ux tx). by move => h t ut tx; apply: h. have sb: forall X, U X -> (transitive_setU U X <-> transitive_set X). move => X UX; split => h. move => t tX; move:(pa _ _ UX tX) => ut. by apply /(sa _ _ ut UX); apply: h. by move => x ux xx; apply /(sa _ _ ux UX); apply: h. have sc: forall X, U X -> (ordinalU U X <-> ordinalp X). move => X UX; split => h. move=> t tT tt tnx; move: (pb _ _ UX tT) => tU; apply: h => //; [by apply/ (sa _ _ tU UX) | by apply /(sb _ tU)]. move => y uy yx ty xy; apply: h => //; first by apply/ (sa _ _ uy UX). by apply /(sb _ uy). have sd: forall x, (U x /\ ordinalU U x) <-> (ordinalp x /\ x <o a). move => x; split; move => [xa xb]. move /(sc _ xa): xb => ox; split => //. move: (urank_pr1 oa xa)(urank_ordinal ox) => [q1 q2] q3. by rewrite -{1} (urank_uniq q2 q3). have ux: U x. apply:(universe_inc1 xb); apply /setP_P; exact:(proj32 (urank_ordinal xa)). by split => //; apply /(sc _ ux). have se0: forall x, U x -> U (union x). move => x ux; move: (p3 x ux) => [u [ua ub]]. suff : u = union x by move => <-. set_extens t => tu. move /(ub _ (pa _ _ ua tu)): tu => [z [za zx tz]]; union_tac. move/setU_P: tu => [z tz zx]; move:(pa _ _ ux zx) => zu. by apply /(ub _ (pa _ _ zu tz)); exists z. have se00: forall r x, U x -> (forall t, inc t x -> U (r t)) -> U (fun_image x r). move => r x /universe_inaccessible_inc [pa1 pb1] xru. apply /universe_inaccessible_inc; split. by move => t/funI_P [z ra ->]; apply: xru => //; apply: pa. exact: (cle_ltT (fun_image_smaller x r) pb1). have se1: forall x y, U x -> U y -> U (J x y). by move => x y ux uy; rewrite kpairE; apply: (ap'); apply: ap'. have se2: forall x y, U x -> U y -> U (x \times y). move => x y ux uy; apply: se0; apply: (se00) => //. move => t tx; apply: se00 => // s sy; apply: se1. apply: (pa _ _ ux tx). apply: (pa _ _ uy sy). have se3: forall x y, U x -> U y -> (x \Eq y <-> equipotentU U x y). move => x y ux uy; split => ha. move: ha => [f [[fa fb] sf tf]]. move: (proj1 fa) => [[qa qa'] qb qc]. rewrite sf in qa'; rewrite tf in qa'; move: (se2 _ _ ux uy) => xyu. move: (pb _ _ xyu qa') => grfu. have qd: subU U (graph f) (x \times y) by apply /sa. have qe:forall b, inc b x -> exists2 c, U c & inc (J b c) (graph f). move => b; rewrite - sf => bsf. move: (Vf_target (proj1 fa) bsf); rewrite tf => h1. rewrite qc in bsf; move :(fdomain_pr1 qb bsf) => h. exists (Vg (graph f) b) => //; apply (pa _ _ uy h1). have qf:forall c, inc c y -> exists2 b, U b & inc (J b c) (graph f). rewrite - tf; move => c cy; move: (surjective_pr fb cy); rewrite sf. move => [b bx ok]; exists b => //; apply (pa _ _ ux bx). have qg:forall b c c', U b -> U c -> U c' -> inc (J b c) (graph f) -> inc (J b c') (graph f) -> c = c'. move => b b' c _ _ _ s1 s2; move: (proj2 qb _ _ s1 s2); aw => h. by move: (pr2_def (h (erefl b))). have qh:forall b b' c, U b -> U b' -> U c -> inc (J b c) (graph f) -> inc (J b' c) (graph f) -> b = b'. move => b b' c _ _ _ s1 s2; exact: (injective_pr3 fa s1 s2). exists (graph f) => //; split => //. move: ha => [g gu [q1 q2 q3 q4 q5]]. have q7: sub g (x \times y) by apply/sa => //; apply /se2. have q8: forall b c, inc (J b c) g -> U b /\ U c. move => b c /q7 /setXp_P [s1 s2]; split. apply: (pa _ _ ux s1). apply: (pa _ _ uy s2). set f := (triple x y g); exists f; rewrite /f; saw. have fgg: fgraph g. apply /functionalP; split; first by apply: (sub_setX_graph q7). move => b c c' bc1 bc2. exact (q5 _ _ _ (proj1 (q8 _ _ bc1)) (proj2 (q8 _ _ bc1)) (proj2 (q8 _ _ bc2)) bc1 bc2). have ff: function f. apply: function_pr => //. by move => s /funI_P [z /q7 /setX_P [_ _ h] -> ]. set_extens s. by move => /q2 [c _ cu]; apply /funI_P; ex_tac; aw. by move => /funI_P [z /q7 /setX_P [_ h _] -> ]. split. apply: injective_pr_bis => // c; aw; move => b b' /= bu b'u. exact: (q4 _ _ _ (proj1 (q8 _ _ bu)) (proj1 (q8 _ _ b'u)) (proj2 (q8 _ _ bu)) bu b'u). apply: surjective_pr5 => //; aw => b /q3 [c uc pg]; exists c => //. by move: (q7 _ pg) => /setXp_P []. have ca: cardinalp a by move: ia => [[[[]]]]. have se6: forall x, cardinalU U x <-> (cardinalp x /\ x <c a). move => x; split. move => [ux oux etc]. move /sd: (conj ux oux) => [ox xa]; suff: cardinalp x. by split => //; apply:oclt3 => //. split => // z oz xeqz. case: (oleT_el (proj1 ca) oz) => za. move: (ocle1 za); rewrite (card_card ca). move /(universe_inaccessible_inc x): ux => [_ ]. by move /card_eqP: xeqz => -> e1 /(cltNge e1). move /sd:(conj oz za) => [uz ouz]. move /(se3 _ _ ux uz): xeqz => eq1. apply /(sa _ _ ux uz); exact (etc _ uz ouz eq1). move => [cx xa]. move: cx => [c1 c2]. have xa1: x <o a by apply: oclt. move /sd:(conj c1 xa1) => [ux oux]; split => // z uz ouz euz. move /sd: (conj uz ouz) => [oz za]; move /(se3 _ _ ux uz):euz => euz'. by move: (c2 _ oz euz') => /(sa _ _ ux uz). have se4: forall X Y Z Z', funsetU U X Y Z -> funsetU U X Y Z' -> Z = Z'. move => X Y Z Z' [ra rb] [rc rd]. set_extens t; [ by move /rb /rd | by move /rd /rb]. have se5: forall X Y, U X -> U Y -> funsetU U X Y (gfunctions Y X). move => X Y ux uy. have ra: sub (gfunctions Y X) (\Po (Y \times X)) by apply: Zo_S. move: (ap _ (se2 _ _ uy ux)) => rb. split; first by exact (pb _ _ rb ra). split. move => /Zo_P [rc [rd re]];move: (pa _ _ rb rc)=> rf. move/setP_P: rc => rc; split => //. rewrite re => x /(fdomain_pr1 rd) => h; exists (Vg f x) => //. by move: (rc _ h) => /setXp_P [_] => vx; apply: (pa _ _ ux vx). move => x y z rg rh; move: (proj2 rd _ _ rg rh); aw => h. exact: (pr2_def(h (erefl x))). move => [rc rd re rf]. have sgf: sgraph f by move => t /rd /setX_P []. apply: Zo_i; [by apply /setP_P => p /rd | split ]. split=> //. move => u v rg rh sp; move: (sgf _ rg)(sgf _ rh) => pr1 pr2. by move: rg rh; rewrite - pr1 -pr2 sp => rg rh; rewrite (rf _ _ _ rg rh). set_extens t; first by move /re => [y uuy yv]; apply /funI_P; ex_tac; aw. by move /funI_P => [z /rd /setX_P [_ aa bb] ->]. have se7: forall x y, cardinalU U x -> cardinalU U y -> powerU_pr U x y (x^c y). move => x y cux cuy. move /se6: (cux) => [cx cxs]; move: (proj31 cux) => ux. move /se6: (cuy) => [cy cys]; move: (proj31 cuy) => uy. move: (se5 _ _ ux uy) => fsv; move: (fsv) => [fsu _]. have aux: cardinalU U (x^c y). by apply /se6; split; fprops;apply: (proj2 (inaccessible_dominant ia)). split => //; exists (gfunctions y x) => //. apply/se3 => //; first exact (proj31 aux). by apply/card_eqP; rewrite cpow_pr0 ;aw. have se8: (forall x y, cardinalU U x -> cardinalU U y -> powerU U x y = (x ^c y)). move => x y cux cuy; move: (se7 _ _ cux cuy) => h. move: (se5 _ _ (proj31 cux) (proj31 cuy)) => ha. pose p z := powerU_pr U x y z. have: exists z, p z by exists (x ^c y). move /choose_pr; rewrite -/(powerU _ _ _); set z := (powerU U x y). rewrite /p; move => [ra [Z za zb]]; move: (se4 _ _ _ _ ha za) => hb. move / (se3 _ _ (proj31 ra) (proj1 za)): zb; rewrite - hb. move/se6:ra => [cz _]. move /card_eqP; rewrite (card_card cz) => ->. by move:(Eq_fun_set y x) => /card_eqP <-. have se9: (forall x, inaccessibleU U x <-> (inaccessible x /\ x <c a)). have aux: forall a b, (a <c b) <-> [/\ cardinalp a, cardinalp b& ssub a b]. by move => b c; split; [move => [[s1 s2 s3] s4] | move => [s1 s2 [s3 s4]]]. move => x;split. move=> [ra rb rc rd]; move /se6: (ra) => [re rf]; split => //. move /aux: (And3 CS_omega re rb) => ox. have a2: forall b, b <c x -> cardinalU U b /\ ssub b x. move => b bx. move: (clt_leT bx (proj1 rf)) => ba. by move/aux: bx => [cb _ h]; split => //;apply /se6. apply /(inaccessible_dominant3 ox); split. move => b c l1 l2; move: (a2 _ l1)(a2 _ l2) => [c1 c2][c3 c4]. apply/ aux; split; [ by apply: CS_pow | exact | ]. move: (rc _ _ c1 c3 c2 c4);rewrite se8 //. move => z za zb; move: (a2 _ zb) => [c1 c2]. have ze: z <> emptyset by move => h; move: (proj2 za); rewrite h. by move: (rd _ c1 ze c2); rewrite se8. move=> [ra rb]. have xo: omega0 <c x. move: (ra) => [[[/infinite_card_limit2 la1 _] _] _]. rewrite -aleph0E (inaccessible_pr1 (proj1 ra)). by apply /aleph_lt_ltc; apply: limit_pos. move /(inaccessible_dominant3 xo): ra=> [rc rd]. have cux: cardinalU U x by apply /se6; split => //; exact: (proj31_1 rb). move/ (aux): xo => [_ cx xo1]. split => //. move => b c qa qb qc qd; move/se6: (qa) => [qe qf]. move /se6: (qb) => [qg qh]. move /aux: (And3 qe cx qc) => bx. move /aux: (And3 qg cx qd) => lcx. move /aux: (rc _ _ bx lcx) => [qi qj qk]; rewrite se8 //. move => b qa qb qc; move/se6: (qa) => [qd qe]. move /aux: (And3 qd cx qc) => bx. have qf: ssub emptyset b by split; fprops. move /aux: (And3 CS0 qd qf) => bx0. by move: (rd _ bx0 bx); rewrite se8. done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)