proposition: Lemma countable_inv_image f: surjection f -> (forall y, inc y (target f) -> countable_set (Vfi1 f y)) -> infinite_set (target f) -> (source f) =c (target f).
proof: Proof. move => sf alc it. apply: cleA; last by apply: surjective_cle; exists f. have ff: function f by fct_tac. set (pa := Lg (target f) (fun z=> (Vfi1 f z))). have ->: source f = unionb pa. set_extens t;last by move /setUb_P1 => [y ytf] /(iim_fun_set1_P _ ff) []. move => tsf; apply /setUb_P1; exists (Vf f t)=> //; first by Wtac. apply (iim_fun_set1_P _ ff);split => //. have ->: cardinal(unionb pa) = csum pa. apply: Eqc_disjointU => //. - rewrite /pa /disjointU_fam; split => //;fprops. - rewrite/disjointU_fam /pa !Lgd//. - by rewrite /disjointU_fam /pa Lgd; move=> i idf; rewrite !LgV//; aw. - rewrite /pa;apply: mutually_disjoint_prop; aw. move=> i j y itf jtf; rewrite !LgV//. move /(iim_fun_set1_P _ ff) => [_ ->]. by move /(iim_fun_set1_P _ ff) => [_ <-]. - fprops. have ->: cardinal (target f) = aleph0 *c domain pa. rewrite /pa Lgd - cprod2cr cprodC cprod_inf //. + by apply: infinite_greater_countable1. + by apply/infinite_setP. + exact: aleph0_nz. rewrite - csum_of_same (csum_pr pa) /pa; apply: csum_increasing;aw; trivial. move => x xa; rewrite !LgV//; apply /countableP; apply: alc =>//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)