proposition: Lemma universe_mo3 a (U :=fun z => inc z (universe a)) : limit_ordinal a -> [/\ [/\ (exists x, U x), (extensionalityA U inc), (unionA U inc), (powersetA U inc) & comprehensionA U inc], ((forall x : Set, U x -> U (powerset x)) /\ (forall x y, U x -> U y -> U (doubleton x y))), (omega0 <o a <-> infiniteA U inc), choiceA U inc & foundationA U inc].
proof: Proof. move => /limit_ordinal_P [anz la]. have la': forall t, osucc t <=o a -> sub (universe (osucc (osucc t))) (universe a). by move => t /oleSltP /la /oleSltP/universe_inc2. have oa:= (proj32_1 anz). move: (universe_mo' oa) => [pa pb]. move: (universe_mo1 pa pb) =>[p1 [p2 [p3 [p4 [p5 [p6 [p7 [p8 [p9 [p10 [p10b p11]]]]]]]]]]]. have q1: (forall x, U x -> U (union x)). move =>x ux; exact (proj1(urank_union oa ux)). have q2: unionA U inc. by move =>x ux; move: (proj1 (p4 _ ux (q1 _ ux))); exists (union x). have q3: (forall x : Set, U x -> U (\Po x)). move => x xa. move: (urank_pr1 oa xa) => [sa [sb /setP_P sc sd]]. move: sc; rewrite - (universe_succ sb) => aa. have: (osucc (osucc (urank a x))) <=o a by apply /oleSltP; apply:la. move /universe_inc2; apply. by move: (urank_powerset (OS_succ sb) aa) => [se _]. have q8b: forall x y, U x -> U y -> U (doubleton x y). move => x y xa ya. suff: exists b, [/\ b <o a, inc x (universe b) & inc y (universe b)]. move => [b [b1 b2 b3]]. by apply:(universe_inc1 b1); apply /setP_P => t;case /set2_P => ->. move: (urank_alt2 oa xa) (urank_alt2 oa ya) => sx sy. move: (urank_pr1 oa xa) => [/la sa _]. move: (urank_pr1 oa ya) => [/la sb _]. move: (OS_succ (OS_urank oa (x:=x))) => o1. move: (OS_succ (OS_urank oa (x:=y))) => o2. case: (oleT_ee o1 o2) => H. by exists (osucc (urank a y)); split => //; apply:(universe_inc2 H). by exists (osucc (urank a x)); split => //; apply:(universe_inc2 H). have q8: forall x, U x -> U (singleton x) by move => x ux; apply: q8b. have q4: powersetA U inc. by move =>x ux; move: (p5 _ ux (q3 _ ux)) => [h _]; exists (\Po x). have q6: U emptyset. move: (ord_ne0_pos oa (nesym (proj2 anz))) => /universe_inc1. by rewrite universe_0 setP_0; apply; apply /set1_P. have q7: exists x, U x by exists emptyset. have q9: foundationA U inc. apply p11 => x xa. have xu: universe_i x by exists a. case:(universe_AF xu);[ by left| move => [y yx dx]; right]. exists y => //; apply (pa _ _ xa yx). have q10: choiceA U inc. move => x xu; rewrite (p9 q7); move => xx1 xx2. set y := fun_image x rep. have pc: forall t, inc t x -> inc (rep t) t. move => t tx; apply: rep_i; apply /nonemptyP; apply: xx1 => //. apply: (pa _ _ xu tx). have pd: forall t, inc t x -> U (rep t). move => t tx; exact: (pa _ _ (pa _ _ xu tx) (pc _ tx)). have yU: U y. apply: (pb _ _ (q1 _ xu)) => s /funI_P [z zx ->]; apply /setU_P; ex_tac. exists y => // z _ zx; exists (rep z); first by apply: pd. rewrite (p7 _ _ yU). have ->: doubletonU U inc (rep z) (rep z) = (singleton (rep z)). rewrite /doubletonU. set p := [eta pairA_pr U inc (rep z) (rep z)]. move: (pd _ zx) => urz; move: (q8 _ urz) => sa. have aux: p (singleton (rep z)). split => // t _; split; first by move /set1_P => h; left. by case => ->; apply /set1_P. have: exists y, p y by exists (singleton (rep z)). move /choose_pr; set w := choose p; move => [sb h]; set_extens t => tz. move /(h _ (pa _ _ sb tz)): tz; case => ->; fprops. by move /set1_P: tz ->; apply /(h _ urz); left. apply: set1_pr. apply /setI2_P; split; [apply /funI_P; ex_tac | by apply: pc]. move => t /setI2_P [/funI_P [u ux -> t2]]. case: (xx2 _ _ (pa _ _ xu zx) (pa _ _ xu ux) zx ux); first by move ->. rewrite (p7 _ _ (pa _ _ xu zx)) => di; empty_tac1 (rep u). have q11 : omega0 <o a <-> infiniteA U inc. move: (urank_ordinal OS_omega) => [sa sb sc]. split. move /universe_inc1 => h. have ou: U omega0 by apply h; apply /setP_P. apply: p10 => // b bo; first by apply:(q8 _ (pa _ _ ou bo)). move: (pa _ _ ou bo) => aa; exact: (q8b _ _ aa (q8 _ aa)). move => ia. case: (oleT_el oa OS_omega) => // /universe_inc2 H. have pr1: forall u v, U u -> U v -> U (u \cup v). by move => u v uu vv; apply: q1; apply: q8b. by move: (H _ (p10b q8b pr1 ia)) => /(universe_P OS_omega) [b /sc]. split => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)