proposition: Lemma ordinals_set_normal1 C (E:= cnext C) B (f:= ordinalsE E B): infinite_c C -> iclosed_set B -> ord_cofinal B E -> [/\ lf_axiom (ordinals (fun x y=> [/\ inc x B, inc y B & x <=o y])) E E , normal_function f E E & Imf f = B].
proof: Proof. move => pa pb pc. move: (ord_cofinal_p5 pa pc); rewrite -/E => eq1. move: (ordinals_set_normal pb) (ordinals_set_iso (proj1 pb)). rewrite eq1; set g := (Lf (ordinals _) E B); move => [p1 p2 p3] [pd pe]. have sbe: sub B E by move: pc => []. have pf: lf_axiom (ordinals (fun x y=> [/\ inc x B, inc y B & x <=o y])) E E by move => t /pd /sbe. have ff: function f by apply: lf_function. have fg: function g by apply: lf_function. have oe: ordinalp E by move:(cnext_pr1 (proj1 pa)) => [[]]. have sf: forall x, inc x E -> Vf f x = Vf g x. by move => x xe; rewrite /f/ordinalsE/g !LfV. have imf: Imf f = B. set_extens t. move /(Imf_P ff); rewrite /f /ordinalsE; aw. by move=> [u ua ->]; rewrite LfV//; apply: pd. move => tb;move: pe => [_ _ [[_ [_ p4]] _ _] _]. have ttg: inc t (target g) by rewrite /g; aw. have sg: source g = E by rewrite /g; aw. move: (p4 _ ttg) => [u ua ->]; rewrite - sf; last by ue. apply /(Imf_P ff); exists u => //;rewrite /f/ordinalsE; aw; ue. split => //; split => //. + by rewrite /f /ordinalsE/function_prop;aw. + by move => x y xe ye xy; rewrite sf // sf //; apply: p2. + move => x xe lx; rewrite sf // (p3 x xe lx). have sxe :=(ordinal_transitive oe xe). have sa: sub x (source g) by rewrite /g; aw. have sb: sub x (source f) by rewrite /f/ordinalsE; aw. congr union; set_extens y. move /(Vf_image_P fg sa) => [u ux ->]; rewrite - sf //; last by apply: sxe. apply /(Vf_image_P ff sb); ex_tac. move /(Vf_image_P ff sb) => [u ux ->]; rewrite sf //; last by apply: sxe. apply /(Vf_image_P fg sa); ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)