proposition: Lemma Exercise6_24a: exists P, [/\ sub P E,cardinal (P) = a & forall x, inc x F -> ~ (sub x P)].
proof: Proof. move: (proj1 iF) => ca. move: (sym_eq cF); rewrite - (card_card ca); move /card_eqP => [g [bg sg tg]]. have fg: function g by fct_tac. have oa: ordinalp a by apply: OS_cardinal. have g1: forall b, b <o a -> inc (Vf g b) F. move => b /(oltP oa); rewrite - sg - tg => h; Wtac. have g2: forall x, inc x F -> exists2 b, b <o a & (Vf g b) = x. rewrite -tg => x xt; move: (bij_surj bg xt) => [b b1 b2]; exists b => //. apply /(oltP oa); ue. pose PP x b p := [/\ pairp p, (inc (P p) ((Vf g b) -s x)), (inc (Q p) ((Vf g b) -s x)) & P p <> Q p]. have g3: forall x b, cardinal x <c a -> b <o a -> exists p, PP x b p. move => x b cx ba; rewrite /PP;move: (g1 _ ba); set s:= (Vf g b) => sF. have cs: cardinal s = a by apply: ceF. have ifs: infinite_set s by apply /infinite_setP; rewrite cs. rewrite - cs in cx. move: (infinite_compl ifs cx); rewrite cs => h. have: (\2c <=c cardinal (s -s x)) by apply: cle_fin_inf; fprops; ue. move/cle2P => [u [v [u1 u2 u3]]]. exists (J u v);split => //; aww. pose g4 x b := choose (PP x b). have g5: forall x b, cardinal x <c a -> b <o a -> PP x b (g4 x b). move => x b p1 p2; move: (g3 _ _ p1 p2); apply: choose_pr. pose mu X := (domain X \cup range X). have mu1: forall X, cardinal X <c a -> cardinal (mu X) <c a. move => X xs; apply: csum2_pr6_inf2 => //; apply: cle_ltT xs; apply: fun_image_smaller. pose g6 fct := g4 (mu (target fct)) (source fct). move: (ordinal_o_wor oa) => wor. move: (transfinite_defined_pr g6 wor). set f := transfinite_defined _ _. rewrite /transfinite_def (ordinal_o_sr a); move=> [pa pb pc]. have g7: forall x, inc x a -> Vf f x = g4 (mu (Vfs f x)) x. by move => x xa; rewrite (pc _ xa) (ordinal_segment oa xa) /g6 /restriction1; aw. have g8: forall x, inc x a -> cardinal x <c a. move => x /(oltP oa) h. apply /(ocle2P ca) => //; exact: (proj31_1 h). have g9: forall x, inc x a -> PP (mu (Vfs f x)) x (Vf f x). move => x xa. have: x <o a by apply /oltP. rewrite (g7 _ xa); apply: g5; apply: mu1; apply: (cle_ltT _ (g8 _ xa)). exact: (image_smaller1 x (proj1 pa)). pose f1 z:= P (Vf f z). have g10: forall z, inc z a -> inc (f1 z) E. move => z za; move: (g9 _ za) => [_ /setC_P [h _] _ _]; apply: FE h. by apply: g1; apply /(oltP oa). have aT: forall s, inc s a -> sub s (source f). by move => s sa; rewrite pb; apply: ordinal_transitive. set r := fun_image a f1. have r1: sub r E by move => t /funI_P [z za ->]; apply g10. have r2: cardinal r = cardinal a. symmetry; apply/card_eqP; exists (Lf f1 a r); aw. saw;apply: lf_bijective. move => t ta; apply /funI_P; ex_tac. suff: forall u v, u <o v -> inc v a -> f1 u <> f1 v. move => H u v ua va sf. have ou:= Os_ordinal oa ua. have ov:= Os_ordinal oa va. case: (oleT_ell ou ov) => // l1. by case: (H _ _ l1 va). by case: (H _ _ l1 ua). move => u v uv va sv; move: (g9 _ va) => [_ /setC_P [sa sb] _ _ ]. case: sb; rewrite -/(f1 v) - sv; apply /setU2_P; left; apply /funI_P. have iuv:= olt_i uv. exists (Vf f u) => //; apply /(Vf_image_P (proj1 pa));fprops;last by ex_tac. by move => y /funI_P. exists r ;split => //. move => x; rewrite - tg => xtg; move: (bij_surj bg xtg); rewrite sg. move => [z za ->] bad. move: (g9 _ za) => [_ _ /setC_P [f2g f2r]] f1f2. move: (bad _ f2g) => /funI_P [s sa sb]. have oz:= Os_ordinal oa za. have os:= Os_ordinal oa sa. case: (oleT_ell oz os); move => zs; first by case: f1f2; rewrite sb zs. move: (g9 _ sa) => [_]; rewrite -/(f1 s). move => /setC_P [_ f1r'] _. case: f1r'; rewrite - sb; apply /setU2_P; right; apply /funI_P. have iuv:= olt_i zs. exists (Vf f z) => //; apply /(Vf_image_P (proj1 pa)); fprops; by ex_tac. case: f2r; rewrite sb; apply /setU2_P; left; apply /funI_P. have iuv:= olt_i zs. exists (Vf f s) => //; apply /(Vf_image_P (proj1 pa));fprops;last by ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)