proposition: Theorem infinite_partition E: infinite_set E -> exists f, [/\ partition_w_fam f E, (domain f) \Eq E & (forall i, inc i (domain f) -> (countable_infinite (Vg f i)))].
proof: Proof. move=> iE; move: (infinite_greater_countable1 iE) => h1. have iE': infinite_c (cardinal E) by apply /infinite_setP. move: (cprod_inf h1 iE' aleph0_nz). rewrite cprod2_pr1; move /card_eqP=> [f [bf sf tf]]. move: (bf) => [injf sjf]. pose G a := (indexedr a aleph0). set (g:= Lg (cardinal E) (fun a => Vfs f (G a))). have ff: function f by fct_tac. have ppa: forall i, inc i (cardinal E) -> sub (G i) (source f). by move => i ie;rewrite sf; apply: setX_Sl; apply/sub1setP. exists g; rewrite /g; aw; split => //; [ | by apply/card_eqP; aw | ]. split => //; fprops. apply: mutually_disjoint_prop;aw; move=> i j y inE jnE;rewrite !LgV//. move: (ppa _ inE)(ppa _ jnE) => pa pb. move /(Vf_image_P ff pa) => [u u1 u2] /(Vf_image_P ff pb) [v v1 v2]. rewrite u2 in v2; move: (proj2 injf _ _ (pa _ u1) (pb _ v1) v2). by move: u1 v1 => /setX_P [_ /set1_P <-] _ /setX_P [_ /set1_P <-] _ ->. set_extens t. move=> /setUb_P1 [y ycE]; move/(Vf_image_P ff (ppa _ ycE)). by move => [u u1 ->]; rewrite -tf; Wtac; apply: (ppa _ ycE). move => tE. have tt: inc t (target f) by rewrite tf. move: (proj2 sjf _ tt);move=> [x xsf jG]. move: xsf; rewrite sf; move /setX_P => [pax px qx]. apply /setUb_P1;ex_tac; apply /(Vf_image_P ff (ppa _ px)). exists x => //; apply /setX_P; split;fprops. move => i inE; rewrite LgV//. have sd: (sub (G i) (source f)) by apply: ppa. apply /infinite_countableP. by rewrite (cardinal_image sd injf) cardinal_indexedr (card_card (CS_aleph0)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)