proposition: Lemma universe_mo2 : let U := universe_i in [/\ ZF_axioms1 U inc, comprehensionA U inc, infiniteA U inc, choiceA U inc & foundationA U inc].
proof: Proof. set U := universe_i => /=. have pa: forall x y, U x -> inc y x -> U y. move => x y /universe_stable_inc; apply. have pa': forall x y, U x -> sub y x -> U y. move => x y ux yx; apply /universe_stable_inc => t ty. apply:(pa _ _ ux (yx _ ty)). move: (universe_mo1 pa pa')=> [p1 [p2 [p3 [p4 [p5 [p6 [p7 [p8 [p9 [p10 [p10b p11]]]]]]]]]]]. have q1: (forall x, U x -> U (union x)). move => x ux; apply /universe_stable_inc => y /setU_P [z za zb]. exact (pa _ _ (pa _ _ ux zb) za). have q2: unionA U inc. by move =>x ux; move: (p4 _ ux (q1 _ ux)) => [h _]; exists (union x). have q3: (forall x : Set, U x -> U (\Po x)). by move => x ux; apply /universe_stable_inc => y /setP_P; apply: pa'. have q4: powersetA U inc. by move =>x ux; move: (p5 _ ux (q3 _ ux)) => [h _]; exists (\Po x). have q5: replacementA U inc. move => x p f ux fp; exists (fun_image (Zo x p) f); split. apply/universe_stable_inc => s /funI_P [z /Zo_P [za zb] ->]. by apply:fp => //; apply: (pa _ _ ux za). move => z uz; split. move /funI_P => [s /Zo_P [r1 r2] ->]; exists s => //. apply: (pa _ _ ux r1). by move => [t ut [tx pt ->]]; apply /funI_P; exists t => //;apply /Zo_P. have q6: U omega0 by apply (universe_ordinal OS_omega). have q7: exists x, U x by exists omega0. have q8: (ZF_axioms1 U inc) by []. move: (model_existence2 q8) => p12. have pru: forall a b, U a -> U b -> U (doubleton a b). by move => a b ua ub; apply /universe_stable_inc=> y /set2_P; case => ->. have q9: infiniteA U inc. have qq:forall a, inc a omega0 -> U (singleton a). move => a ao; apply: pru; apply: (pa _ _ q6 ao). apply: p10 => //. by move => a ao; apply: pru => //; [ apply: (pa _ _ q6 ao) | apply: qq]. have q10: foundationA U inc. apply p11 => x xu; case:(universe_AF xu);[ by left| move => [y yx dx]; right]. exists y => //; apply (pa _ _ xu yx). split => //. 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. by apply /universe_stable_inc => s /funI_P [z zx ->]; apply: pd. 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)). move: (p12 _ _ (pd _ zx) (pd _ zx)) => [s1 s2]. apply: extensionality. move => t ts; apply /set1_P. by move: (s2 _ (pa _ _ s1 ts)) => h; move /h: ts; case. by move => t /set1_P ->; apply /(s2 _ (pd _ zx)); 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). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)