proposition: Lemma Exercise6_6c (p:= \Po E) : (functions E F) \Eq p /\ (sub_functions E F) \Eq p.
proof: Proof. set s1:= (functions E F); set s2 := (sub_functions E F). move: (Exercise6_5a E F); rewrite -/s1 -/s2 => prop1. move: Finf => [a [b [aF bF ab]]]. have pb: (cardinal p) <=c (cardinal s1). pose f A x := Yo (inc x A) a b. have ta: forall A, lf_axiom (f A) E F. by move=> A t tE; rewrite /f; Ytac xE. pose fA A := Lf (f A) E F. have pb:forall u v : Set, inc u p -> inc v p -> fA u = fA v -> sub u v. move=> u v; rewrite /p /fA => /setP_P uE /setP_P vE sf t tu. move: (ta u) (ta v) => ta1 ta2; move: (uE _ tu) => tE. move: (f_equal (Vf^~t) sf); rewrite /f !LfV//; Ytac0; Ytac yv => //. have ij: injection (Lf fA p s1). apply: lf_injective. move=> A As3; rewrite /fA;apply /functionsP;red;saw. apply: lf_function; apply: ta. move=> u v us3 vs3 sf; apply: extensionality; apply: pb => //. by move: (inj_source_smaller ij); aw. move: (Exercise6_5b E F). rewrite -/s2 -/p. have ->: (cardinal (\Po (product E F)) = cardinal p). rewrite /p ! card_setP;apply: cpow_pr; fprops. by apply: cprod_inf3 => //; exists a. move=> pa. have pe:= (cleA pa (cleT pb prop1)). have pe':= (cleA (cleT prop1 pa) pb). by split; apply /card_eqP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)