proposition: Lemma cofinality_pr6 a f (b:= omega_fct a): ordinalp a -> inc f (functions b b) -> exists g, inc g (injections b b) /\ (forall x, inc x b -> Vf f x <=o Vf g x).
proof: Proof. move => oa /functionsP [ff sf tf]. move: (aleph_limit oa); rewrite -/b => lb. move: (lb) => [ob zb plb]. move: (ordinal_o_wor ob); set r := ordinal_o _ => wor. have sr: substrate r = b by rewrite /r ordinal_o_sr. pose unsrc f:= Yo (inc (domain f) b) (domain f) \0o. have cp3: forall x, inc (unsrc x) b by move=> x; rewrite /unsrc; Ytac h => //. pose coer1 v y := intersection (b -s (v \cup y)). pose coex v := (Yo (inc v b) v \0o). pose p g := let s := unsrc g in coex (coer1 (Vf f s) (direct_image g s)). move: (transfinite_pr1 p wor); rewrite /transfiniteg_def sr. set g:= transfiniteg_defined r p; move=> [fgg sg tgp]. pose Tf := direct_image g. have cp0 u v: inc (coer1 u v) b. rewrite/coer1;set c := _ -s _;case: (emptyset_dichot c) => ce. by rewrite ce setI_0. have os: ordinal_set c by move => t /setC_P [/(Os_ordinal ob) tb _]. by move: (ordinal_setI ce os) => /setC_P []. have cp4 x: inc x b -> Vg g x = (coer1 (Vf f x) (Tf x)). move=> xb. rewrite (tgp _ xb) /p /unsrc restr_d (ordinal_segment ob xb); Ytac0. rewrite/coex (Y_true (cp0 _ _)) (dirim_restr2 fgg) //. by rewrite sg; move/(oltP ob): xb => /proj1/proj33. have ta: lf_axiom (Vg g) b b by move => t tb; rewrite (cp4 _ tb); apply:cp0. have taa: forall x, inc x b -> lf_axiom (Vg g) x b. move=> x xb t ita; move: (ordinal_transitive ob xb ita); apply ta. set h:= Lf (fun z => Vg g z) b b. have hp x: inc x b -> Vf h x = Vg g x by move => xsf; rewrite /h LfV. have off1 x: inc x b -> inc (Vf f x) b by move => xb; Wtac. have off2: forall x, inc x b -> ordinalp (Vf f x). by move => x /off1 /(Os_ordinal ob). have cp5: forall x, inc x b -> nonempty (b -s ((Vf f x) \cup (Tf x))). move => x xb. apply:(infinite_union2 (CIS_aleph oa)). have: Vf f x <o b by move /(oltP ob): (off1 _ xb). by move/ (ocle2P (CS_aleph oa) (off2 _ xb)). move /(oltP ob): xb => lxb. move/(ocle2P (CS_aleph oa) (proj31_1 lxb)): (lxb) => lec2. have xsg: sub x (domain g) by rewrite sg; exact: (proj33 (proj1 lxb)). move:(range_smaller (restr_fgraph g x)). rewrite (dirim_restr fgg xsg) restr_d => cc; apply:(cle_ltT cc lec2). have cp6 x: inc x b -> inc (Vg g x) (b -s ((Vf f x) \cup (Tf x))). move => xb; move: (cp5 _ xb)=> ne. rewrite (cp4 _ xb) /coer1; apply:(ordinal_setI ne). by move => t /setC_P [/(Os_ordinal ob) tb _]. have ra: function_prop h b b. by rewrite /h; red; saw; apply: lf_function. have rb: (forall x, inc x b -> Vf f x <=o Vf h x). move => x xb; rewrite (hp _ xb). move: (cp6 _ xb) => /setC_P [p1] /setU2_P p2. case: (oleT_el (off2 _ xb) (Os_ordinal ob p1)) => // /oltP0/ proj33 ok. by case: p2; left. exists h; split => //; apply:Zo_i;first by apply/functionsP. apply: lf_injective => // u v ub vb sv. have Ha x: inc x b -> ~ inc (Vg g x) (Tf x). by move => /cp6 /setC_P [p1] /setU2_P ww res; case: ww; right. have Hb x y: inc x y -> inc y b -> inc (Vg g x) (Tf y). move => ixy yb; apply/dirim_P; ex_tac; apply:(fdomain_pr1 fgg). by rewrite sg; move: (ordinal_transitive ob yb ixy). case: (ordinal_inA (Os_ordinal ob ub)(Os_ordinal ob vb)) => // cuv. by case:(Ha _ vb); move: (Hb _ _ cuv vb); rewrite sv. by case:(Ha _ ub); move: (Hb _ _ cuv ub); rewrite sv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)