proposition: Lemma universe_stable_inc x: universe_i x <-> (forall y, inc y x -> universe_i y).
proof: Proof. split. by move => [a pa pb] y ye; move: (urank_inc pa pb ye) => [ya _]; exists a. move => h. pose p x y := ordinalp y /\ inc x (universe y). have cp: forall y, inc y x -> p y (choose (p y)). by move => y yx; apply choose_pr; move: (h _ yx) => [t ta tb]; exists t. set E := fun_image x (fun z => choose (p z)). have ose: ordinal_set E by move => t /funI_P [z /cp [pa _] ->]. move: (OS_sup ose)(ord_sup_ub ose); set a := \osup E => pa pb. exists (osucc a); first by fprops. rewrite (universe_succ pa); apply /setP_P => y yx. have: inc (choose (p y)) E by apply /funI_P; ex_tac. by move /pb /universe_inc2; apply; move: (cp _ yx) => [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)