proposition: Lemma universe_mo4 (U :=fun z => inc z (universe omega0)) : [/\ ZF_axioms1 U inc, ~(infiniteA U inc), choiceA U inc & foundationA U inc].
proof: Proof. move:(universe_mo3 omega_limit). move: (universe_mo' OS_omega) => [pr1 pr2]. move => [[pa pb pc pd] pe ap pf pg ph]; split => //;last by move => /pf []. split => //. move => x p f ux au; exists (fun_image (Zo x p) f); split. move: (universe_omega_props ux) => [ra rb rc]. apply: universe_omega_hi. apply: finite_fun_image;apply: (sub_finite_set _ ra); apply: Zo_S. move => t /funI_P [z /Zo_P [sa sb] ->]; apply: au => //. apply: (pr1 _ _ ux sa). move => z uz; split. move /funI_P => [a /Zo_P [bb cc] ->]; exists a => //; apply: (pr1 _ _ ux bb). by move => [t tu [sa sb ->]]; apply /funI_P;exists t => //; apply /Zo_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)