proposition: Lemma aleph_pr9 x: ordinalp x -> let y:= (omega_fct x) in let src := (osucc x) in let trg := Zo (cardinals_le y) infinite_c in order_isomorphism (Lf (fun z => (omega_fct z)) src trg) (ole_on src)(ole_on trg).
proof: Proof. move=> ox y src trg. have osrc: ordinalp src by apply: OS_succ. move:(wordering_ole_pr (Os_ordinal osrc)) => [p2 p1]. move: p2 => [p2 _]. have cy: cardinalp y by apply: CS_aleph. have cse:ordinal_set trg by move => t /Zo_P [_] [] []. have [[p3 _] p4]:=(wordering_ole_pr cse). have ta:lf_axiom (fun z => (omega_fct z)) src trg. move=> z;rewrite /src/trg; move /(oleP ox) => pa; apply /Zo_P; split. apply /cardinals_leP => //. apply: (aleph_le_lec pa). have oz:= proj31 pa. apply: (CIS_aleph oz). saw. saw => //; apply: lf_bijective => //. move => u v usr vsr. move: (Os_ordinal osrc usr) (Os_ordinal osrc vsr) => oa ob. by apply: aleph_inj. move=> z /Zo_P [] /(cardinals_leP cy) zy iz. move: (ord_index_pr1 iz)=> [ot tp]. exists (ord_index z) => //. rewrite /src; apply/oleP => //. by apply: aleph_lec_le => //; rewrite tp. red;aw;move=> a b ais bis; rewrite !LfV//. split; move /Zo_P => [] /setXp_P [pa pb]; aw => h; apply: Zo_i; try apply:setXp_i => //; try apply: ta => //; aw. by apply: aleph_le_leo. move:(Os_ordinal osrc ais) (Os_ordinal osrc bis) => oa ob. apply: aleph_leo_le => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)