proposition: Lemma cofinality_pr4 x (y:= \cf x): ordinalp x -> exists2 f, (cofinal_function f x y /\ normal_function f y x) & (inc \1o y -> Vf f \0o = \0o).
proof: Proof. move => ox. move: (cofinality_rw ox); rewrite -/y;move => [oy [g cg gmin]]. case: (ordinal_limA ox) => lx. move: cg; rewrite /y lx cofinality0 => cg; move: (cg) => [pa _]. exists g; first (split => //;split => // a; first move => b); case; case. move: lx cg => [t ot ts]; rewrite /y ts cofinality_succ. exists g; last by move => h; case: (ordinal_irreflexive OS1 h). split => //; move: cg => [pa pb]; split => //. - by move => a b /set1_P -> /set1_P -> [_]. - by move => a /set1_P -> /limit_nz. by apply: OS_succr; ue. move: (cofinality_limit3 lx) => ly. move: cg => [[fg sg tg] cfg]. move: (lx) => [_ xnz lx1]. move: (ordinal_o_wor oy); set r := ordinal_o _ => wor. have sr: substrate r = y by rewrite /r ordinal_o_sr. pose unsrc f:= Yo (inc (domain f) y) (domain f) \0o. have cp3: forall a, inc (unsrc a) y. move=> a; rewrite /unsrc; Ytac h => //; exact (proj32 ly). pose coex v := (Yo (inc v x) v \0o). pose coer1 v u := (Yo (v <=o u) u v). pose coer a ga fa su := coex (Yo (osuccp a) (coer1 ga (osucc fa)) su). pose p f := let a := unsrc f in coer a (Vf g (opred a)) (Vg f (opred a)) (\osup (direct_image f a)). move: (transfinite_pr1 p wor); rewrite /transfiniteg_def sr. set f:= transfiniteg_defined r p; move=> [ff sf tfp]. have oty := (ordinal_transitive oy). have sfa a: inc a y -> sub a (domain f) by move=> /oty ay; rewrite sf. set T := direct_image f. have cp4: forall a, inc a y -> Vg f a = coer a (Vf g (opred a)) (Vg f (opred a)) (\osup (T a)). move=> a ay. rewrite (tfp _ ay) /p /unsrc restr_d (ordinal_segment oy ay); Ytac0. rewrite /coer; case: (p_or_not_p (osuccp a)) => aux2; Ytac0; Ytac0. by move: (succ_i (opred a)); rewrite (predo_K aux2) => /(restr_ev f) ->. by rewrite (dirim_restr2 ff (sfa _ ay)). have ta: lf_axiom (Vg f) y x. by move => t /cp4 ->; rewrite /coer /coex; Ytac xx. have srg: sub (range f) x by move => t /(range_gP ff) [z zs ->]; apply: ta; ue. have taa: forall a, inc a y -> lf_axiom (Vg f) a x. move=> a ay t /(oty _ ay); apply: ta. set h:= Lf (Vg f) y x. have hp a: inc a y -> Vf h a = Vg f a by move => asf; rewrite /h LfV. have fsv: forall b, inc b y -> inc (osucc b) y -> Vg f (osucc b) = coer1 (Vf g b) (osucc (Vg f b)). move=> b iby siby; rewrite (cp4 _ siby) /coer. move: (Os_ordinal oy iby) => ob. have isb: (osuccp (osucc b)) by exists b. Ytac0; rewrite (succo_K ob). rewrite /coex Y_true// /coer1; Ytac aux; first by apply: lx1; apply: ta. rewrite -tg; apply: Vf_target => //; ue. have noovf: forall a, inc a y -> inc (\osup (T a)) x. move => a ay. have ax := (taa _ ay). have pa:= (sub_trans (@dirim_Sr f a) srg). have ost:(ordinal_set (T a)) by move => t tT;apply:(Os_ordinal ox (pa _ tT)). case:(oleT_el ox (OS_sup ost)); [move => xb | by move/(oltP ox)]. suff: cofinal_function_ex x a. have le2: (a <o y) by apply /oltP. by move /(gmin _ (Os_ordinal oy ay)) => /(oltNge le2). exists (Lf (Vg f) a x); split. hnf;saw; by apply: lf_function. move => t itx. move /(oltP ox):(itx) => ltx; move:(olt_leT ltx xb) => ltb. move:(olt_sup ost ltb) => [z zT /proj1 ltz]. move: (zT) => /(dirim_P) [v va /(in_graph_V ff) /pr2_def zv]; ex_tac. by move: zv;aw; rewrite LfV// => <-. have nf1: (forall a, inc a y -> ~(osuccp a) -> Vg f a = \osup (T a)). move=> a ay ni; rewrite (cp4 _ ay) /coer /coex; Ytac0. by rewrite (Y_true (noovf _ ay)). have si1: forall a, inc a y -> Vg f a <o Vg f (osucc a). move=> a ay. have o1: ordinalp (Vf g a). apply: (Os_ordinal ox); rewrite - tg; apply: Vf_target=> //; ue. have o2: ordinalp (osucc (Vg f a)). by apply: OS_succ;apply: (Os_ordinal ox); apply: (ta _ ay). rewrite (fsv _ ay (proj33 ly _ ay)) /coer1;apply /oleSltP. case: (oleT_el o1 o2) => le1; first by Ytac0; exact: (oleR (proj32 le1)). rewrite (Y_false (oltNge le1)); exact (proj1 le1). have fh: function h by apply:lf_function. have fyx:function_prop h y x by rewrite /h; saw. have nf: normal_function h y x. apply: ord_sincr_cont_propv => //. by move => a ay; rewrite (hp _ ay) (hp _ (proj33 ly _ ay)); apply: si1. move => a ay la; rewrite (hp _ ay) (nf1 _ ay (limit_nonsucc' la)). by rewrite /T /Vfs /h /Lf corresp_g - sf (Lg_recovers ff). exists h; last first. have n0z: ~ (osuccp \0o) by move => [u _ uu];case: (@osucc_nz u). move:(proj32 ly) => y0; rewrite (hp _ y0) (nf1 _ y0 n0z) => _. suff: T \0o = emptyset by move ->; rewrite setU_0. by apply/set0_P => t /dirim_P [z /in_set0]. split => //; split => //. move => t tx; move: (cfg _ tx) => [a ay tw]. move:(proj33 ly _ ay) => cy; ex_tac. rewrite (hp _ cy) (fsv _ ay cy). rewrite /coer1. Ytac hh => //; apply: (oleT tw hh). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)