proposition: Lemma Exercise6_33f: cardinal M = c.
proof: Proof. have bnz := nesym (proj2(clt_leT clt_01 hb)). have le: cardinal M <=c c. set f := (Lg E6_33_c (fun z => Vf X z)). apply: (cleT (csum_pr1 f)). set f1 := (Lg (domain f) (fun z => cardinal (Vg f z))). set g := cst_graph c b. have f1x: fgraph f1 by rewrite /f1/cst_graph; fprops. have gx: fgraph g by rewrite /g/cst_graph; fprops. have sd: domain f1 = domain g by rewrite /f1 /g /f /cst_graph; aw. have le1: (forall x, inc x (domain f1) -> Vg f1 x <=c Vg g x). rewrite /f1/f/g/cst_graph; aw => x xd; rewrite !LgV//. by apply: HF2; apply:Exercise6_33d1. move: (csum_increasing sd le1);rewrite [csum g] csum_of_same. by rewrite cprodC (cprod_inf (proj1 Exercise6_33a4) Exercise6_33c bnz). case: (Exercise6_33a5 le) => //le1. set T1:= fun_image (functions b M) Imf; set T := T1 +s1 emptyset. move: (Exercise6_33d) => [[fx ix] sx tx]. have pa: forall i, inc i c -> inc (Vf X i) T. move => i ic. move: (ic); rewrite - sx => ic'. move: ((Vf_target fx) _ ic'); rewrite tx =>/setC1_P [wf _]. move: (HF2 wf) => cl. case: (emptyset_dichot (Vf X i))=> wne; first by rewrite wne /T; fprops. apply /setU1_P; left; aw. move: cl; rewrite - {1} (card_card (proj32 hb)) => le2. have /set_leP [c2 cb ecb]: (Vf X i) <=s b. apply /(eq_subset_cardP); exact: (cardinal_le_aux1 le2). have [f [bf sf tf]]: c2 \Eq Vf X i by apply: EqS. pose g z := Yo (inc z c2) (Vf f z) (rep (Vf X i)). have pa: forall z, inc (g z) (Vf X i). move => z; rewrite /g; Ytac zc; last by apply: rep_i. rewrite -tf; Wtac; fct_tac. have pb: forall z, inc z (Vf X i) -> exists2 i, inc i b & g i = z. rewrite -tf; move=> z ztf; move: ((proj2 (proj2 bf)) _ ztf)=> [y ysf ->]. rewrite sf in ysf; exists y; [by apply: cb | by rewrite /g; Ytac0]. have pc: lf_axiom g b M. by move => z zb; move: (pa z) => i1; apply /setUb_P; aw; ex_tac; bw. set G := Lf g b M. have fg: function G by apply: lf_function. have pd: inc G (functions b M). by rewrite /G;apply /functionsP;saw. apply /funI_P;ex_tac; symmetry;set_extens t. move /(Imf_P fg) => [u usg ->]. by rewrite /G;aw; rewrite LfV//; move: usg; rewrite /G; aw. move => tw; move: (pb _ tw) => [z zi <-]; apply /(Imf_P fg). by exists z; rewrite /G; aw;bw. have : c <=s T. exists (Lf (fun z => (Vf X z)) c T); saw. apply: lf_injective; first by apply: pa. by rewrite - sx; apply: ix. move /eq_subset_cardP1; rewrite (card_card (proj32 le)) => eq1. set aa:= (functions b M). have sj: (surjection (Lf Imf aa (fun_image aa Imf))). apply: lf_surjective. by move=> t ta; apply /funI_P;exists t. by move=> y /funI_P. move: (image_smaller (proj1 sj)). move: (surjective_pr0 sj); aw; move => ->; rewrite /aa -/T1. rewrite cpow_pr1 (card_card (proj32 hb)). have -> : cardinal T1 = cardinal T. case: (inc_or_not emptyset T1) => eT. by rewrite /T (setU1_eq eT). move: Exercise6_33c => i1. move: (cle_inf_inf Exercise6_33c eq1) => /infinite_setP it. by rewrite (card_setC1_inf emptyset it) /T (setU1_K eT). move => l2; move: (cleT eq1 l2) => l3. case: (equal_or_not (cardinal M) \0c) => mz. by move:l3; rewrite mz (cpow0x bnz) => h; symmetry; apply: cle0. move: (cpow_Mleeq b le1 mz); rewrite Exercise6_33a2 => l1. case: (cltNge Exercise6_33b (cleT l3 l1)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)