proposition: Lemma universe_omega_hi x: finite_set x -> sub x (universe omega0) -> inc x (universe omega0).
proof: Proof. move => fxs ux. set s := fun_image x (fun t => (urank omega0 t)). case: (emptyset_dichot x) => nex. rewrite nex (universe_limit omega_limit);apply /setUf_P. exists \1o; first by apply: NS1. rewrite - osucc_zero (universe_succ OS0) universe_0. apply: setP_Ti. have nes: nonempty s. exists (urank omega0 (rep x)); apply /funI_P;exists (rep x) => //. by apply: rep_i. have fss: finite_set s by apply: finite_fun_image. have sr: sub s Nat. move => t /funI_P [z zx ->]. by move: (universe_omega_props (ux _ zx)) => []. move: (finite_subset_Nat sr fss nes) => [n]. move /funI_P => [z /ux /universe_omega_props [_ _ za] zb] pb. set k := osucc (osucc n). have on: ordinalp n by rewrite zb; apply: OS_nat. rewrite (universe_limit omega_limit); apply /setUf_P; exists k. by move: (proj33 omega_limit)=> rec; apply: (rec); apply: rec; rewrite zb. rewrite universe_succ; last by apply: OS_succ. apply /setP_P => t tx. have: inc (urank omega0 t) s by apply /funI_P; ex_tac. move /pb => /ocle /universe_inc2 pd. move :(urank_pr1 OS_omega (ux _ tx)) => [_ [_ pe _]]. rewrite (universe_succ on);apply/setP_P; apply: sub_trans pe pd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)