proposition: Lemma Exercise6_24b: (forall G, sub G F -> cardinal G <c a -> a <=c cardinal (E -s union G)) -> exists P, [/\ sub P E, cardinal (P) = a & forall x, inc x F -> (cardinal (P \cap x)) <c a].
proof: Proof. move: (proj1 iF) => ca. move: (sym_eq cF); rewrite - {1 4} (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. move => bighyp. pose PP x b p := [/\ inc p E, ~ inc p x & ~ inc p (unionf b (Vf g))]. have g3: forall x b, cardinal x <c a -> b <o a -> exists p, PP x b p. move => X z cx za; rewrite /PP. set G := (fun_image z (Vf g)). have sza:= proj33 (proj1 za). have sG: sub G F. move => t /funI_P [s sa ->]; apply: g1. apply /(oltP oa); exact(sza s sa). have oz:= proj31_1 za. move /(ocle2P ca oz): za => lt1. have cG: cardinal G <c a. apply: cle_ltT lt1; apply: (fun_image_smaller). move: (bighyp _ sG cG) => le1. move: (clt_leT cx le1) => le2. have ifs: infinite_set (E -s union G). by apply /infinite_setP;apply: (cle_inf_inf iF le1). move: (infinite_compl ifs le2) => le3. case: (emptyset_dichot ((E -s union G) -s X)) => ee. move: ifs => /infinite_setP; rewrite -le3 ee cardinal_set0 => le4. case: (finite_not_infinite finite_0 le4). move: ee => [x /setC_P [/setC_P [xe xg]] xX]; ex_tac => // xu; case: xg. move /setUf_P: xu => [y ya yb]; apply /setU_P; exists (Vf g y)=> //. apply /funI_P; ex_tac. 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 g6 fct := g4 (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 (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. by apply /(ocle2P ca (proj31_1 h)). have g9: forall x, inc x a -> PP (Vfs f x) x (Vf f x). move => x xa. have: x <o a by apply /oltP. rewrite (g7 _ xa); apply: g5; apply: (cle_ltT _ (g8 _ xa)). exact: (image_smaller1 x (proj1 pa)). have aT: forall s, inc s a -> sub s (source f). by move => s sa; rewrite pb; apply: ordinal_transitive. exists (target f);split => //. by move => t /(proj2 pa); rewrite pb; move => [x /g9 [xe _ _]] ->. symmetry; apply /card_eqP; exists f; saw; split => //. split; first by fct_tac. suff: forall u v, u <o v -> inc v a -> (Vf f u) <> Vf f v. rewrite pb => H x y xsf ysf sv. have ox:= Os_ordinal oa xsf. have oy:= Os_ordinal oa ysf. case:(oleT_ell ox oy) => // h. by case: (H _ _ h ysf). by case: (H _ _ h xsf). move => u v uv va sv; move: (g9 _ va) => [_ h1 _]. have ov:= proj32_1 uv. move /(oltP ov): uv => uv1. case: h1; rewrite - sv; apply /(Vf_image_P (proj1 pa)); fprops; ex_tac. move => x; rewrite -tg => xtg; move: (bij_surj bg xtg); rewrite sg. move => [b ba ->]; set G := _ \cap _. have: sub G (fun_image (osucc b) (fun z => Vf f z)). move => t /setI2_P [/(proj2 pa)]; rewrite pb; move => [z za ->] zb. move:(g9 _ za) => [_ h1 h2]. have oz:= Os_ordinal oa za. have ob:= Os_ordinal oa ba. apply /funI_P; exists z => //. case:(oleT_ell oz ob) => // h. rewrite h; fprops. by apply /setU1_P; left; apply /oltP. by case: h2; apply /setUf_P; exists b => //; apply /oltP. move /sub_smaller => h1; apply: (cle_ltT h1). apply: (@cle_ltT (cardinal (osucc b))). by apply:fun_image_smaller. move: (infinite_card_limit2 iF) => [_ _ h]. move: (h _ ba) => /(oltP oa) lt1. apply /(ocle2P ca) => //; exact (proj31_1 lt1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)