proposition: Lemma exists_ordering X: cardinal_fam X -> exists f, [/\ bijection f, ordinalp (source f), target f = domain X & fg_Mle_lec (X \cf (graph f))].
proof: Proof. move => pb. set d := domain X. set w := Zo d (fun z => ~ (inc z z)). case: (p_or_not_p (inc w d)) => wp. case: (p_or_not_p (inc w w)) => h2; first by move: (h2) => /Zo_hi bad. by case: (h2); apply: Zo_i. pose mzY Y z := (forall u, inc u Y -> Vg X z <=c Vg X u). pose lev Y:= rep (Zo Y (mzY Y)). have lep Y: sub Y d -> nonempty Y -> (inc (lev Y) Y /\ mzY Y (lev Y)). move => yd [y yY]; rewrite /lev; set T := Zo _ _. suff: nonempty T by move/rep_i => /Zo_P []. set Z := fun_image Y (Vg X). have neZ: nonempty Z by exists (Vg X y); apply /funI_P; exists y. have cZ: cardinal_set Z. by move => t /funI_P [z zy ->]; apply: pb; apply: yd. move:(cle_wor' cZ neZ) => [/funI_P [t ty ->] qb]. by exists t; apply: (Zo_i ty) => u uy; apply:qb; apply:funI_i. pose lew Y:= Yo (nonempty (d -s Y)) (lev (d -s Y)) w. have lewe Y: nonempty (d -s Y) -> (inc (lew Y) (d -s Y) /\ mzY (d -s Y) (lew Y)). by move => ne; rewrite /lew; Ytac0; apply: lep => //; apply: sub_setC. have lewb Y: inc (lew Y) (d +s1 w). apply/setU1_P;case: (p_or_not_p (nonempty (d -s Y))) => h. by move: (lewe _ h) => [] /setC_P [ok _] _; left. by right;rewrite /lew; Ytac0. move: (cantor (CS_cardinal d)); set a := _ ^c _ => lt1. move: (proj32_1 lt1) => ca; move: (proj1 ca) => oa. move: (ordinal_o_wor oa); set r := ordinal_o _ => wor. have sr: substrate r = a by rewrite /r ordinal_o_sr. pose lef f := lew (Imf f). have ts: (forall f, function f -> segmentp r (source f) -> sub (target f) (d +s1 w) -> inc (lef f) (d +s1 w)). move=> f _ _ _; apply: lewb. move: (transfinite_defined_pr lef wor); rewrite /transfinite_def sr. move: (transfinite_definition_stable wor ts). set f := transfinite_defined _ _; move=> stf [sjf sf fv]. have ff: function f by fct_tac. pose R i := restriction1 f (segment r i). have sRi i: inc i a -> source (R i) = i. by move => ia; rewrite /R /restriction1 /r ordinal_segment; aw. have fi: forall i, inc i a -> Vf f i <> w -> forall j, inc j i -> Vf f i <> Vf f j. move => i ia fw; move: (fv _ ia); rewrite /lef. set E := (Imf (R i)) => eq1. move: eq1; case: (p_or_not_p (nonempty (d -s E))) => nt; last by rewrite /lew; Ytac0. move: (lewe _ nt) => [ /setC_P [_ s1]] _ eq j ji sv. case: s1; rewrite -eq sv /E. have sr1 := sRi _ ia. have sa1: sub (segment r i) (source f) by rewrite sf - sr ;apply: sub_segment. have ji1: inc j (segment r i). apply /segmentP; apply /ordo_ltP => //. by apply: (ordinal_transitive oa ia). apply /(Imf_P (proj1 (restriction1_fs ff sa1))). by rewrite sr1;exists j => //; rewrite (restriction1_V ff sa1 ji1). case: (p_or_not_p (inc w (target f))) => wt; last first. have bf: (bijection f). split; last by exact. split; [exact | move => x y xsf ysf sv]. case: (equal_or_not (Vf f x) w) => le1. case: wt; rewrite -le1; Wtac. rewrite sf in xsf ysf. have ox:= (Os_ordinal oa xsf). have oy:= (Os_ordinal oa ysf). case: (oleT_ell ox oy) => //. move /(oltP oy) => lt2. by rewrite sv in le1; move: (fi _ ysf le1 _ lt2); rewrite sv. by move /(oltP ox) => lt2; move: (fi _ xsf le1 _ lt2). have /sub_smaller: sub (target f) d. move=> t td; move: (stf _ td); case/setU1_P => // tw; case: wt;ue. by rewrite -(card_bijection bf) sf (card_card ca) => /(cltNge lt1). pose pri i := (inc i (source f) /\ w = Vf f i). have [i0 iv0]: exists i, pri i by move: ((proj2 sjf) _ wt) => [i0]; exists i0. have oi0: ordinalp i0 by move: (proj1 iv0); rewrite sf; apply: (Os_ordinal oa). move: (least_ordinal4 oi0 iv0). set qi :=least_ordinal _ _;move=> [oq [qsf qv] ql]. rewrite sf in qsf;move: qv; rewrite (fv _ qsf) /lef /lew. set e := Imf (R qi). case: (p_or_not_p (nonempty (d -s e))) =>h qv. move: (lewe _ h) => [ /setC_P [wd _] _]; case: wp. by move: wd;rewrite /lew - qv. have sr1 := sRi _ qsf. have sa1: sub (segment r qi) (source f) by rewrite sf - sr ;apply: sub_segment. have fr:=(proj1 (restriction1_fs ff sa1)). have pa1: forall i, inc i qi -> (inc (Vf f i) d /\ Vf f i <> w). move => t tq. move: (ordinal_transitive oa qsf tq); rewrite - sf => tf. case/setU1_P: (stf _ (Vf_target ff tf)) => qa. by split => // ww; case: wp; rewrite - ww. have prt : (pri t) by split. have h1:= (ql _ (Os_ordinal oq tq) prt). by move: tq => /(oltP oq) /(oleNgt h1). have fv1 i: inc i qi -> Vf (R qi) i = Vf f i. move => iq. rewrite /R (ordinal_segment oa qsf)(restriction1_V ff) //. rewrite sf; apply:(ordinal_transitive oa qsf). have de: d = e. set_extens t. move => qa; ex_middle tne; case: h; exists t; fprops. move /(Imf_P fr); rewrite sr1; move => [u uq ->]. by rewrite (fv1 _ uq); move: (pa1 _ uq) => []. have ij1: forall i j, inc i qi -> inc j qi -> Vf f i = Vf f j -> i = j. move => i j iq jq sv. move: (pa1 _ iq) (pa1 _ jq)=> [_ xa1] [_ ya1]. have ia:= ordinal_transitive oa qsf iq. have ja:=ordinal_transitive oa qsf jq. have oi:= Os_ordinal oa ia. have oj:= Os_ordinal oa ja. case: (oleT_ell oi oj) => //. by move /(oltP oj) => lt2; move: (fi _ ja ya1 _ lt2); rewrite sv. by move /(oltP oi) => lt2; move: (fi _ ia xa1 _ lt2). have ij2: injection (R qi). split; first by exact. rewrite sr1; move => x y xsf ysf /=. by rewrite (fv1 _ xsf) (fv1 _ ysf); apply: ij1. move: (restriction_to_image_fb ij2). set g := restriction_to_image (R qi) => bg. have tg: target g = d. by rewrite /g de /restriction_to_image/ restriction2; aw. have osd: ordinalp (source g). by rewrite /g /restriction_to_image/ restriction2 sr1; aw. have fg: function g by fct_tac. have r2a: restriction2_axioms (R qi) (source (R qi)) (Imf (R qi)). by split => //; apply: Imf_Starget. have gV : forall i, inc i qi -> Vf g i = Vf f i. move => i iq; rewrite/g /restriction_to_image restriction2_V // ? fv1 ? sr1//. exists g; split => // u v. rewrite composef_domain => us vs uv. rewrite !composef_ev //;rewrite -/(Vf g u) -/ (Vf g v). have aux: domain (graph g) = qi. rewrite (domain_fg fg) /g /restriction_to_image /restriction2 corresp_s. by aw; rewrite sr1. rewrite aux in us vs; rewrite (gV _ us) (gV _ vs). move: (pa1 _ us) => [wfu wfuw]. case: (equal_or_not u v) => euv. by rewrite - euv; apply: cleR; apply: pb. move: (ordinal_transitive oa qsf us) => ua. rewrite (fv _ ua) /lef; set f0:= (R u). case: (p_or_not_p (nonempty (d -s Imf f0))) => cle; last first. by case: wfuw; rewrite (fv _ ua) /lef -/f0 /lew; Ytac0. move: (lewe _ cle); set x := lew _ ; move=> [qa qb]. suff: inc (Vf f v)(d -s (Imf f0)). move => qc; apply: (qb _ qc). have sa2: sub (segment r u) (source f) by rewrite sf - sr ;apply: sub_segment. have sr2 : (source f0) = u by apply: sRi. have fr2:=(proj1 (restriction1_fs ff sa2)). move: (pa1 _ vs) => [wfv _]; apply /setC_P;split => //. move /(Imf_P fr2); rewrite sr2; move => [t tu]. have tu1: inc t (segment r u). by apply/segmentP; apply/ordo_ltP => //; move:(ordinal_transitive oa ua tu). rewrite (restriction1_V ff sa2 tu1) => sv1; symmetry in sv1. have tqi:=(ordinal_transitive oq us tu). move: tu; rewrite (ij1 _ _ tqi vs sv1). by move /(oltP (Os_ordinal oa ua)) => /(oleNgt uv). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)