proposition: Lemma Exercise6_7b E F (A:= functions E F) (B := injections E F) (C:= Zo (\Po F)(fun x => x =c E)): infinite_set F -> (cardinal E) <=c (cardinal F) -> (cardinal A = cardinal B /\ cardinal A = cardinal C).
proof: Proof. move => infF leEF. case: (emptyset_dichot E) => ne. have -> : C= singleton emptyset. apply:set1_pr. by apply/ Zo_P;split;[apply /setP_P | rewrite ne]; fprops. move => z /Zo_P [_]; rewrite ne cardinal_set0; apply: card_nonempty. rewrite cardinal_set1. move: (@fun_set_small_source F); rewrite -ne -/A => sA. set f:= empty_function_tg F. have injf: injection f. move: (empty_function_tg_function F) => [xa xb xc]. by split => // x y; rewrite xb => /in_set0. have fA: inc f A. rewrite /A /f/empty_function_tg. by apply /functionsP; red;aw;split => //; fct_tac. have As: A = singleton f. by set_extens t; [ move=> tA; apply /set1_P;apply: sA | move /set1_P=> -> ]. have Bs: B = singleton f. set_extens t; aw; first by move => /Zo_P; rewrite -/A As; case. by move /set1_P => ->; apply: Zo_i. rewrite As Bs ! cardinal_set1; split => //. have prop1:cardinal A = cardinal B. symmetry;apply: cleA. have pa: sub B A by apply: Zo_S. apply: (sub_smaller pa). move/card_eqP: (cprod_inf3 ne leEF infF) => [g [bg sg tg]]. pose Cf f := Lf (fun x => Vf g (J (Vf f x) x)) E F. suff pa: injection (Lf Cf A B) by move: (inj_source_smaller pa); aw. have pa: forall u x, inc u A -> inc x E -> inc (J (Vf u x) x) (source g). move=> u x; rewrite /A sg;move=> /functionsP [fu su tu] xE. apply: setXp_i => //; rewrite -tu; Wtac. have pb: forall u, inc u A -> lf_axiom (fun x=> Vf g (J (Vf u x) x)) E F. move=> u uA x xE; rewrite -tg; apply:Vf_target;[fct_tac | by apply: pa]. move: bg => [[fg ig] sjg]. have pc:lf_axiom Cf A B. move=> t tA. have aux: injection (Cf t). apply: lf_injective; first by apply: pb. move=> u v uE vE h;exact(pr2_def (ig _ _ (pa _ _ tA uE)(pa _ _ tA vE) h)). apply: Zo_i => //; rewrite /Cf;apply /functionsP;saw; fct_tac. apply: lf_injective => //. move=> u v uA vA; move: (pb _ uA) (pb _ vA) => ta1 ta2. move: (uA) (vA); move=> /functionsP [fu su tu] /functionsP [fv sv tv] sf. apply: function_exten => //; try ue; rewrite su => x xs. move: (f_equal (Vf^~ x) sf); rewrite /Cf !LfV// => sw. exact: (pr1_def (ig _ _ (pa _ _ uA xs) (pa _ _ vA xs) sw)). split => //. move: (cprod_inf3 ne leEF infF) =>/card_eqP aux. move: (EqT (Eq_setX2_S E F) aux) => [g [bg sg tg]]. pose k f := Vfs g (graph f). have pa: forall f, inc f A -> sub (graph f) (source g). move=> f /functionsP [ff sf tf]. by rewrite sg - sf -tf; move: ff => [[_ qa] _]. have ig: injection g by move: bg => [ok _]. have ta: lf_axiom k A C. move=> f fA; move: (pa _ fA)=> ha; apply: Zo_i. apply /setP_P;rewrite /k -tg; apply: fun_image_Starget1; fct_tac. rewrite/k (cardinal_image ha ig). by move: fA => /functionsP [/Eq_src_graph /card_eqP <- -> _]. have i1: injection (Lf k A C). apply: lf_injective => //. move=> u v uA vA; move: (pa _ uA) (pa _ vA) => g1 g2; move: uA vA. move=> /functionsP [fu su tu] /functionsP [fv sv tv] => aux2. apply: function_exten1 => //; last by ue. apply: (image_by_fun_injective ig) => //. apply: cleA; first by move: (inj_source_smaller i1); aw. rewrite prop1. apply: Exercise6_7a. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)