proposition: Theorem infinite_finite_subsets E: infinite_set E -> (Zo (\Po E) finite_set) =c E.
proof: Proof. move=> inE. have icE: infinite_c (cardinal E) by split; [apply: CS_cardinal | exact]. set bF:=Zo _ _ . pose T n := Zo (\Po E) (fun z => cardinal z = n). have le1: (forall n, natp n -> (cardinal (T n)) <=c (cardinal E)). move=> n nN; rewrite /T. have cn:= card_nat nN. set (K:= injections n E). have ta: lf_axiom (fun z => Imf z) K (T n). move=> z /Zo_P [] /functionsP [fz sz tz] inz; apply: Zo_i. apply /setP_P;rewrite -tz => //; apply: Imf_Starget => //. by rewrite (cardinal_range inz) sz cn. set (f:= Lf (fun z => Imf z) K (T n)). have ff: function f by apply: lf_function. set (q:= permutations n). set (c := cardinal q). have fc: (finite_c c). apply/NatP; rewrite /c /q (card_permutations) /finite_set cn; fprops. by apply: NS_factorial. have cii: (forall x, inc x (target f) -> cardinal (Vfi1 f x) = c). move=> x ;rewrite/f; aw; move => /Zo_P [] /setP_P xE cx. have /card_eqP [x0 [bx0 sx0 tx0]]: n =c x by rewrite - cx; aw. set x1 := triple n E (graph x0). have sx1: (source x1 = n) by rewrite /x1; aw. have tx1: (target x1 = E) by rewrite /x1; aw. have fx1: function x1. have fx0 := (proj1 (proj1 bx0)). have ha := (function_fgraph fx0). have hb:sub (range (graph x0)) E. apply: (sub_trans (f_range_graph fx0)); ue. by apply: (function_pr ha hb); rewrite domain_fg. have ix1: injection x1. apply:injective_pr_bis => //. rewrite /x1;aw;move=> u v w p1 p2. apply: (injective_pr (proj1 bx0) p1 p2). set iif := Vfi1 _ _. set (g:= Lf (fun z=> (x1 \co z)) q iif). have ta2: (lf_axiom (fun z=> (x1 \co z)) q iif). rewrite/q/iif => z zq; apply /iim_fun_set1_P => //. move: zq => /Zo_P [] /functionsP [fz sz tz] bz. have cxz: (x1 \coP z) by split => //; ue. set (t:= x1 \co z). have fr: (function t) by rewrite /t; fct_tac. have tk: (inc t K). apply: Zo_i; first by apply /functionsP;split => //; rewrite /t; aw. apply: inj_compose1 =>//; [ move: bz => [iz _] => // | ue]. split; first by aw. have gz: sgraph (graph z) by fprops. suff: (x = Vf f t) by move => ->; rewrite /f; aw. rewrite /f LfV // (ImfE fr) /t /compose; aw. rewrite (compg_range _ gz) - (ImfE fz) (surjective_pr0 (proj2 bz)). by rewrite - tx0 - (surjective_pr0 (proj2 bx0)) tz - sx0 /x1; aw. have fg: function g by rewrite /g; apply: lf_function =>//. symmetry;apply /card_eqP; exists g; split => //; rewrite /g; aw; trivial. apply: lf_bijective => //. move=> u v /Zo_P [] /functionsP [fu su tu] bu /Zo_P [] /functionsP [fv sv tv] bv sc. apply: function_exten; try fct_tac; try ue. move=> w wsu. have : (Vf (x1 \co u) w = Vf (x1 \co v) w) by ue. have c1: x1 \coP v by split => //; try fct_tac; try ue. have c2: x1 \coP u by split => //; try fct_tac; try ue. have wsv :inc w (source v) by rewrite sv - su. rewrite !compfV //; apply: (proj2 ix1). rewrite sx1 -tu; Wtac;fct_tac. rewrite sx1 -tv; Wtac;fct_tac. move => y /(iim_fun_set1_P _ ff) []. rewrite /f lf_source => pa; rewrite LfV// => rgy. move: pa; rewrite /f; aw; move => /Zo_P [y1 iy]. have w2: Imf y = Imf x0 by rewrite (surjective_pr0 (proj2 bx0)) tx0. have w3: Imf x0 = Imf x1. by rewrite (ImfE fx1) (ImfE (proj1 (proj1 bx0))) /x1;aw. have ww: sub (Imf y) (Imf x1) by rewrite w2 w3. move: y1 => /functionsP [fy sy ty]. rewrite -tx1 in ty; move: ww;rewrite -(exists_right_composable fy ix1 ty). move => [h [cph ch]]; exists h => //. have sh: (source h = n) by rewrite - sy - ch; aw. have th: (target h = n) by move: cph => [_ _ hq]; rewrite -hq. have ih: injection h. split;first by fct_tac. move => v w vsh wsh sw. have: Vf y v = Vf y w by rewrite - ch !compfV // sw. apply: (proj2 iy); [rewrite sy - sh // |rewrite sy - sh //]. have bh: bijection h. apply: bijective_if_same_finite_c_inj; rewrite ? th ? sh //. by rewrite /finite_set cn; fprops. apply: Zo_i => //; apply /functionsP;split => //; fct_tac. move: (shepherd_principle ff cii). rewrite /f; aw; move => cK. case: (equal_or_not n \0c) => nz. have te: (T \0c = singleton emptyset). apply: set1_pr. apply: Zo_i; [apply:setP_0i | apply:cardinal_set0]. move => z /Zo_P [_ aux]; rewrite (card_nonempty aux) //. rewrite nz -/(T _) te cardinal_set1. apply: cle_fin_inf; [ fprops | exact]. case: (finite_or_infinite (CS_cardinal (T n))) => finT. apply: cle_fin_inf =>//. set (K1:= cardinal (functions n E)). have k1E: (K1 = cardinal E). by rewrite /K1 -/(E ^c n) - cpowcl; apply: cpow_inf. have: (cardinal K <=c cardinal E). rewrite -k1E; apply: sub_smaller;apply: Zo_S. apply: cleT; rewrite cK. have i2: (c <=c (cardinal (T n))) by apply: cle_fin_inf. have i3: (c <> \0c). rewrite /c/q. have fsn: finite_set n by rewrite /finite_set cn; fprops. rewrite (card_permutations fsn) cn; apply: (factorial_nz nN). rewrite (cprod_inf i2 finT i3); fprops. set Fn := Lg Nat T. apply: cleA; last first. apply /eq_subset_cardP1. exists (Lf (fun x => singleton x) E bF); saw. apply: lf_injective. move=> x xe /=; rewrite/bF; apply: Zo_i; last by apply: set1_finite. by apply /setP_P; apply /sub1setP. move=> u v _ _;apply: set1_inj. have <-: csumb (domain Fn) (fun i => (cardinal E)) = cardinal E. rewrite /Fn csum_of_same Lgd. exact: cprod_inf (infinite_greater_countable1 inE) icE aleph0_nz. have ->: (bF = unionb Fn). set_extens t. move /Zo_P => [pa pb]; apply /setUb_P1; exists (cardinal t). rewrite -/(natp _); fprops. apply /Zo_i => //. move /setUb_P1 => [y yb] /Zo_P [pa pb]; apply /Zo_P;split => //. by apply /NatP; rewrite pb. have ->: (unionb Fn) =c (unionb (disjointU_fam Fn)). apply: Eqc_disjointU; rewrite/Fn/disjointU_fam. + split => //; aww=> i iN; rewrite !LgV//; aw; trivial; apply: Eqc_indexed2. + apply: mutually_disjoint_prop; rewrite /Fn Lgd. by move=> i j y iN jN; rewrite !LgV//;aw; move => /Zo_hi <- /Zo_hi <-. + apply: mutually_disjoint_prop3. rewrite -/(csum Fn) (csum_pr Fn). apply: csum_increasing; fprops;rewrite /Fn !Lgd //; move=> x xd. rewrite !LgV //; apply: le1 =>//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)