proposition: Lemma infinite_finite_sequence E: infinite_set E -> (Zo (sub_functions Nat E) (fun z=> finite_set (source z))) =c E.
proof: Proof. move=> iE. have iE': infinite_c (cardinal E) by apply /infinite_setP. set q:= Zo _ _. apply: cleA. move: (infinite_finite_subsets infinite_Nat). set Fn:=Zo _ _ => fse. have qu:q = unionb (Lg Fn (fun z=> (functions z E))). set_extens t. move => /Zo_P [] /sfunctionsP [ft sst tt] fst. apply /setUb_P1;exists (source t) => //. apply: Zo_i =>//; by apply /setP_P. apply /functionsP;split => //. move => /setUb_P1 [y] /Zo_P [] /setP_P pa pb /functionsP [ft st tt]. apply: Zo_i; [ apply /sfunctionsP;split => //; ue | rewrite st; fprops ]. have ze: (forall z, inc z Fn -> (cardinal (functions z E)) <=c (cardinal E)). move=> z zFn ; rewrite -/(E ^c z) - cpowcl - cpowcr. apply: cpow_inf1 =>//; move: zFn => /Zo_P [_ pa]; fprops. move: (csum_pr1 (Lg Fn (functions^~ E))). rewrite -qu; rewrite Lgd /csumb. set (g:= (Lg Fn (fun _:Set => cardinal E))). set f0:= (Lg Fn _ ). have fg1: (fgraph f0) by rewrite /f0; fprops. have fg2: (fgraph g) by rewrite /g; fprops. have df0g: domain f0 = domain g by rewrite /f0 /g !Lgd. have ale: (forall x, inc x (domain f0) -> (Vg f0 x) <=c (Vg g x)). by rewrite /f0/g Lgd; move=> x xdf; rewrite !LgV//; apply: ze. move: (csum_increasing df0g ale); rewrite [csum g]csum_of_same => le1 le2. move: (infinite_greater_countable1 iE) => le3. move: (cprod_inf1 le3 iE'). rewrite aleph0_pr1 - fse cprod2cr. exact: cleT (cleT le2 le1). apply /eq_subset_cardP1. have aux: forall v, inc v E -> lf_axiom (fun _ => v) (singleton \0c) E by move=> vE t //=. exists (Lf (fun z => (Lf ((fun _:Set => z))(singleton \0c) E)) E q). saw; apply: lf_injective. move=> z zE; apply: Zo_i. apply /sfunctionsP;saw. apply: lf_function =>//. apply: set1_sub; apply: NS0. aw; apply: set1_finite. have zs:= set1_1 \0c. by move=> u v uE vE /(f_equal (Vf ^~ \0c)); rewrite !LfV //; apply: aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)