proposition: Lemma cofinality_pr7 X b f (E := omega_fct b): ofg_Mle_leo X -> domain X = omega_fct b -> ordinalp b -> limit_ordinal (\osup (range X)) -> inc f (functions E (omega_fct (union (range X)))) -> exists2 g, inc g (injections E E) & (forall x, inc x (source f) -> Vf f x <=o omega_fct (Vg X (Vf g x))).
proof: Proof. move=> [p1 p2 p2'] p4 p3. have lb: limit_ordinal (domain X) by rewrite p4; apply: aleph_limit. set a := (union (range X)) => la. set E1 := functions E (omega_fct a). set F2 := functions E E. move => /functionsP [ff sf tf]. move: (p1)(lb) => fgX [p5 p5' p6]. move: (ofg_Mle_leo_os p1 p2) => p8. have p9: forall t, inc t (omega_fct a) -> exists u, inc u E /\ t <=o omega_fct (Vg X u). move => t ta. move: (la) => [oa _]. move: (OS_aleph oa) => pa0. move: aleph_normal => [_ ap1]; move: (ap1 _ la) => ap2. have ap3: (ordinal_set (fun_image a omega_fct)). move => u /funI_P [v ve ->]; apply (OS_aleph (Os_ordinal oa ve)). have ap4: t <o \osup (fun_image a omega_fct). by rewrite - ap2; apply /oltP. move: (olt_sup ap3 ap4) => [z ] /funI_P [w wa ->]. move => le1. have le2: w <o union (range X) by apply /oltP. move: (olt_sup p8 le2) => [u q1 q2]. move:q1 => /(range_gP fgX) [v vd vv]. rewrite /E - p4; exists v; split => //; apply: (oleT (proj1 le1)). rewrite - vv; apply: (aleph_le_leo (proj1 q2)). pose bv t := choose (fun u => inc u E /\ t <=o omega_fct (Vg X u)). have p10: forall t, inc t (omega_fct a) -> (inc (bv t) (omega_fct b) /\ t <=o omega_fct (Vg X (bv t))). move => t to;apply: (choose_pr (p9 _ to)). pose bff := Lf (fun z => bv (Vf f z)) E E. have p11: lf_axiom (fun z : Set => bv (Vf f z)) E E. move => z ze. have wt: inc (Vf f z)(omega_fct a) by rewrite -tf; Wtac. by move: (p10 _ wt) => []. have p12: inc bff F2. apply /functionsP;rewrite /bff;red;saw. apply: lf_function; apply: p11. have p13: forall x, inc x (source f) -> Vf f x <=o omega_fct (Vg X (Vf bff x)). move => x xsf. rewrite sf in xsf; rewrite /bff LfV//. have wt: inc (Vf f x)(omega_fct a) by rewrite -tf; Wtac. by move: (p10 _ wt) => []. move: (cofinality_pr6 p3 p12)=> [g [ge H]]; exists g=> //. move => x xsf; move: (p13 _ xsf) => le1. apply (oleT le1); apply: aleph_le_leo. rewrite sf in xsf. move: (H _ xsf) => h1. have q4: inc (Vf bff x) (domain X). by move: p12 => /functionsP [s1 s2 s3]; rewrite p4 -/E - s3; Wtac. have q5: inc (Vf g x) (domain X). move: ge => /Zo_P [] /functionsP [s1 s2 s3] _. by rewrite p4 /E - s3; Wtac; rewrite s2. exact: (p2' _ _ q4 q5 h1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)