proposition: Lemma cardinal_pformulas_in X : cardinal (pformulas_in X) = cardinal X +c aleph0.
proof: Proof. set Y := (pformulas_in X). move: (aleph0_pr X) => /=; set c1 := cardinal X +c aleph0. move => [h1 h2 h3 h4 [h5 h6 h7 h8]]. have hd: aleph0 <=c cardinal Y. pose phi i:= J (J val_eq (J i i)) emptyset. have ax: forall i, inc i variables -> inc (phi i) Y. move=> i iv; apply/pformulas_inP;rewrite /phi; split; first split;aww. + exact (proj1(fkind_eq_p2 iv iv)). + exact fgraph_set0. set f := Lf phi variables Y. have injf: injection f. apply:lf_injective => // u v _ _ h. exact: (pr1_def (pr2_def (pr1_def h))). move: (inj_source_smaller injf); rewrite /f; aw; ue. have he: cardinal X <=c cardinal Y. pose phi i:= J (J val_eq (J \0c \0c)) (singleton (J \0c i)). have ax: forall i, inc i X -> inc (phi i) Y. move => i iv. move: (simple_fct NS0 iv ) => [pa pb pc pd [pe pf]]. apply/pformulas_inP; rewrite /phi;split; first saw. + fprops. + exact (proj1(fkind_eq_p2 NS0 NS0)). + by rewrite (free_vars_eq NS0 NS0) pb. + by aw. set f := Lf phi X Y. have injf: injection f. apply:lf_injective => // u v _ _ h. exact: (pr2_def(set1_inj(pr2_def h))). by move: (inj_source_smaller injf); rewrite /f; aw. have hf: c1 <=c cardinal Y by exact: (h8 _ hd he). set fa := (fun z => singleton z \times Zo (sub_fgraphs variables X) (fun t => pformula_in X (J z t))). have eq1 : Y = unionf all_formulas fa. set_extens t. move/pformulas_inP => h; move: (h) => [[pa pb pc pd] pe ]. apply /setUf_P; exists (P t) => //; apply /setX_P; split => //. fprops. apply/ Zo_P; rewrite pa; split => //;apply/sub_fgraphsP. exists (domain (Q t)); last by apply/gfunctions_P2. exact:(sub_trans pd (proj1 (free_vars_variables pb))). move => /setUf_P [z za /setX_P [zb /set1_P zc /Zo_P [zd ze]]]. by apply /pformulas_inP; rewrite - zb zc. suff h: forall z, formulap z -> cardinal (fa z) <=c c1. move: (csum_pr1_bis all_formulas fa); rewrite - eq1 /csumb. set g := (Lg all_formulas (fun a : Set => cardinal (fa a))) => k1. move:countable_formulas => /countableP => uc. have ud: cardinal (domain g) <=c c1 by rewrite /g; aw;exact : (cleT uc h6). have ue:(forall i, inc i (domain g) -> Vg g i <=c c1). by rewrite /g; aw => i idf; rewrite LgV//; apply: h. move: (notbig_family_sum h5 ud ue) => uf. exact: (cleA (cleT k1 uf) hf). move => z fz; rewrite /fa cardinal_indexedr. move: (free_vars_variables fz) => [sa /NatP sb]. set E := Zo _ _. set A := (\Po (free_vars z)); set B := (fun u => gfunctions u X). have : sub E (unionf A B). move => t /Zo_P [qa [[qb qc qd qe] qf]]. rewrite pr1_pair in qe; rewrite pr2_pair in qd qe qf. apply/setUf_P; exists (domain t); first by apply /setP_P. by apply/gfunctions_P2; split => //. move/sub_smaller => le2. move: (cleT le2 (csum_pr1_bis A B)); rewrite /csumb. set f := (Lg A (fun a : Set => cardinal (B a))) => le1; apply: (cleT le1). have k6: forall t, inc t Nat -> t <=c c1. move => t k2; move /olt_omegaP: (k2) => k3. exact: (cleT (proj1 (oclt3 (CS_nat k2) CS_omega k3)) h6). have sc: cardinal (domain f) <=c c1. rewrite /f/A; aw; rewrite card_setP - cpowcr; exact: (k6 _ (NS_pow NS2 sb)). have sd: (forall i, inc i (domain f) -> Vg f i <=c c1). rewrite /f/A/B; aw; move => i ia; rewrite LgV//; move /setP_P: ia => ia. move: (Eq_fun_set i X) => /card_eqP <-;rewrite cpow_pr1. have hi := (NS_le_nat (sub_smaller ia) sb). case: (finite_or_infinite (proj31 he)) => fx. move/NatP: fx => fx; exact: (k6 _ (NS_pow fx hi)). exact: (cleT (cpow_inf1 fx hi) h7). exact:(notbig_family_sum h5 sc sd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)