proposition: Lemma universe_mo1 (U: property): (forall x y, U x -> inc y x -> U y) -> (forall x y, U x -> sub y x -> U y) -> (extensionalityA U inc) /\ (forall x r, U x -> (setofU U inc x r) = (Zo x r)) /\ (comprehensionA U inc) /\ (forall x, U x -> U (union x) -> (unionA_pr U inc x (union x)) /\ (unionU U inc x = union x)) /\ (forall x, U x -> U (powerset x) -> (powersetA_pr U inc x (powerset x)) /\ (powersetU U inc x = powerset x)) /\ ( forall a b, U a -> U b -> U (doubleton a b) -> (pairA_pr U inc a b (doubleton a b)) /\ (doubletonU U inc a b = doubleton a b)) /\ (forall a b, U a -> intersectionU2 U inc a b = a \cap b) /\ (forall a b, U a -> U b -> U (doubleton a b) -> U (a\cup b) -> unionU2 U inc a b = a \cup b) /\ ((exists x, U x) -> emptysetU U inc = emptyset) /\ ((forall a, inc a omega0 -> U (singleton a)) -> (forall a, inc a omega0 -> U (doubleton a (singleton a))) -> U omega0 -> infiniteA U inc) /\ ( (forall a b, U a -> U b -> U (doubleton a b)) -> (forall a b, U a -> U b -> U (a \cup b)) -> infiniteA U inc -> U omega0) /\ ( (forall x, U x -> x = emptyset \/ exists2 y, U y & inc y x /\ disjoint y x) -> foundationA U inc).
proof: Proof. move => su su'. have p1: extensionalityA U inc. move => x y ux uy h; apply: extensionality => t ta. by apply /(h _ (su _ _ ux ta)). by apply /(h _ (su _ _ uy ta)). move: (model_uniqueness p1) => [uu up uc ur [ue upa]]. have aux: forall (p:property) x, p x -> uniqueness p -> (choose p) = x. by move => p x px unp; apply: unp => //; apply: choose_pr; exists x. have p2: forall x p, U x -> (comprehensionA_pr U inc x p (Zo x p)). move => x p ux; split; first by apply: (su' x _ ux); apply: Zo_S. by move => z uz; split; move/Zo_P. have p3: (comprehensionA U inc). by move => x p ux; exists (Zo x p); apply: p2. have p4: (forall x r, U x -> (setofU U inc x r) = (Zo x r)). move => x p ux; apply: aux; [ by apply: p2 | apply: uc]. have p5: forall x, U x -> U (union x) -> (unionA_pr U inc x (union x)) /\ (unionU U inc x = union x). move => x ux uux. have pa:unionA_pr U inc x (union x). split=> // y uy; split => //. move /setU_P => [z za zb]; exists z; split => //; apply: (su _ _ ux zb). move => [z [_ zx zy]]; union_tac. split => //; apply: aux; [ by apply: pa | apply: uu]. have p6: (forall x, U x -> U (\Po x) -> (powersetA_pr U inc x (\Po x)) /\ (powersetU U inc x = \Po x)). move => x ux uux. have pa:(powersetA_pr U inc x (\Po x)). split => // y uy; split. move /setP_P => yx t _; apply: yx. move => h; apply /setP_P => t tx; apply: h => //;apply (su _ _ uy tx). split => //; apply: aux; [ by apply: pa | apply: up]. have p7: forall a b, U a -> intersectionU2 U inc a b = a \cap b. move => a b ua ; rewrite /intersectionU2 (p4 _ _ ua);set_extens t. by move /Zo_P /setI2_P. by move /setI2_P => h; apply/Zo_P. have p8: forall a b, U a -> U b -> U (doubleton a b) -> (pairA_pr U inc a b (doubleton a b)) /\ (doubletonU U inc a b = doubleton a b). move => a b ua ub uab. have pa:(pairA_pr U inc a b (doubleton a b)). split=> // y uy; split => //; by move /set2_P. split => //; apply: aux; [ by apply: pa | apply: upa]. have p9: forall a b, U a -> U b -> U (doubleton a b) -> U (a\cup b) -> unionU2 U inc a b = a \cup b. move => a b ua ub ud uab. rewrite /unionU2 (proj2 (p8 _ _ ua ub ud)). by rewrite (proj2 (p5 _ ud uab)). have p0: (exists x, U x) -> emptysetU U inc = emptyset. move => [x Ux]; apply: aux => //. split; last by move => t _ /in_set0. move: (p2 x (fun _:Set => False) Ux) => []. have -> // : (Zo x (fun _ : Set => False))= emptyset. apply /set0_P; apply :Zo_hi. have p10: (forall a, inc a omega0 -> U (singleton a)) -> (forall a, inc a omega0 -> U (doubleton a (singleton a))) -> U omega0 -> infiniteA U inc. move=> q1 q2 q3; exists omega0 => //. move: omega_limit => [o1 o2 o3]. have neu: (exists x, U x) by exists omega0. rewrite (p0 neu); split; [exact | move => t ut to]. move: (p8 _ _ ut ut (q1 _ to))=> [[sa _] ->]. move: (o3 _ to) => so. by rewrite (p9 _ _ ut sa (q2 _ to) (su _ _ q3 so)). have p11:((forall a b, U a -> U b -> U (doubleton a b)) -> (forall a b, U a -> U b -> U (a \cup b)) -> infiniteA U inc -> U omega0). move => pa pb [u ux [uy uz]]. have ee: (exists x : Set, U x) by exists u. rewrite (p0 ee) in uy. have pc: forall t, inc t u -> inc (osucc t) u. move => t tu; move: (su _ _ ux tu) => ut. move: (uz _ ut tu); move: (pa _ _ ut ut) => utt. rewrite (proj2 (p8 _ _ ut ut utt)). move: (pa _ _ ut utt) => ut3. by rewrite (p9 _ _ ut utt ut3 (pb _ _ ut utt)). have: sub omega0 u. by apply:Nat_induction => // n nN /pc; rewrite succ_of_nat. by apply: su'. have p12: (forall x, U x -> x = emptyset \/ exists2 y, U y & inc y x /\ disjoint y x) -> foundationA U inc. move => hyp x ux. have neu: (exists x, U x) by exists x. rewrite (p0 neu); case: (hyp _ ux);[ by left | move => [y yu [yx di]]; right]. by exists y => //; rewrite (p7 _ _ yu). done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)