proposition: Lemma Exercise6_7a E F (B := injections E F) (C := Zo (\Po F)(fun x => x =c E)): (cardinal C) <=c (cardinal B).
proof: Proof. apply: surjective_cle. exists (Lf (fun f => (Imf f)) B C); saw. have pa: lf_axiom (fun f => (Imf f)) B C. move=> f => /Zo_P [] /functionsP [ff sf tf] injf. apply:Zo_i; last by move: (cardinal_range injf); rewrite sf. by apply /setP_P; rewrite -tf; apply:Imf_Starget. apply: lf_surjective => //. move=> y => /Zo_P [] /setP_P yF/card_eqP /EqS [f [bf sf tf]]. have ta: lf_axiom (Vf f) E F. move=> t; rewrite - sf => zE; apply: yF; rewrite -tf. apply: Vf_target => //; fct_tac. move: bf => [[ff injf] sjf]. have fi: injection (Lf (Vf f) E F). apply: lf_injective =>// u v uE vE; by apply: injf; rewrite sf. have ffi:function (Lf (Vf f) E F) by fct_tac. exists (Lf (Vf f) E F). apply: Zo_i =>//; apply /functionsP;saw. symmetry;set_extens t. move /(Imf_P ffi); aw; move => [x xE];rewrite LfV// => ->; Wtac. rewrite - tf;move => ty; apply /(Imf_P ffi); aw. by move: ((proj2 sjf) _ ty); rewrite sf; move=> [x xE ->]; ex_tac; rewrite !LfV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)