proposition: Lemma Exercice6_5h E: infinite_set E -> (permutations E) =c (\Po E).
proof: Proof. move=> isE. set s:= (permutations E). apply: cleA. by apply: Exercise6_5c. set aux:= ((\Po E) -s (fun_image E singleton)). have ->: cardinal (\Po E) = cardinal aux. rewrite /aux; set A := \Po E; set B:= fun_image _ _. symmetry; apply:(infinite_compl (infinite_powerset isE)). have -> : cardinal B = cardinal E. symmetry; apply /card_eqP;exists (Lf singleton E B); saw. apply: lf_bijective. move => t tE; apply /funI_P; ex_tac. move=> u v _ _ ss; have : inc u (singleton v) by rewrite - ss; fprops. by move /set1_P. by move=> y /funI_P. rewrite card_setP - cpowcr; apply:cantor; fprops. apply: surjective_cle. exists (Lf (fun z => (E -s (fixpoints z))) s aux). saw; apply: lf_surjective. move=> f /Zo_P [] /functionsP [ff sf tf] bf. apply /setC_P;split => //; first by apply /setP_P => t /setC_P []. move /funI_P=> [z zE sc]. move: (set1_1 z); rewrite - sc; move /setC_P => [_ ze]; case: ze. apply: Zo_i; first (by ue). rewrite - sf in zE. case: (inc_or_not (Vf f z) (fixpoints f)). move /Zo_P => [pa pb]; move: bf => [[_ injf] _]; apply: (injf _ _ pa zE pb). move: (Vf_target ff zE); rewrite tf; move=> pa pb. have : inc (Vf f z) (singleton z) by rewrite - sc; apply /setC_P;split => //. by move /set1_P. move=> F /setC_P [] /setP_P FE /funI_P ns. case: (Exercice6_5g F). move=> [u ysu]; case: ns; exists u => //; apply: FE; rewrite ysu; fprops. move=> [f /Zo_P [/Zo_P [pa pb] pc]]. pose g x:= Yo (inc x F) (Vf f x) x. move: pa pb => /functionsP [ff sf tf] [[_ fi] sjf]. have ta: lf_axiom g E E. rewrite /g;move=> x xE; simpl; Ytac xf =>//. apply: FE; rewrite -tf; apply: Vf_target => //; ue. have bg: (bijection (Lf g E E)). apply: lf_bijective => //. move=> u v uE vE; rewrite /g; Ytac uf; Ytac vf. by apply: fi; ue. by move => eql; rewrite -eql in vf; case: vf; rewrite -tf; Wtac. by move => eql; rewrite eql in uf; case: uf; rewrite -tf; Wtac. by []. move=> y yE; case: (inc_or_not y F) => yF. rewrite -tf in yF; move: ((proj2 sjf) _ yF) => [x]. by rewrite sf => xF ->; move: (FE _ xF) => xE; ex_tac; rewrite /g; Ytac0. by exists y => //; rewrite /g; Ytac0. exists (Lf g E E). by apply: Zo_i => //; apply /functionsP; saw; fct_tac. symmetry;set_extens t. by move => /setC_P [tE] /Zo_P;aw;rewrite LfV// /g; Ytac tF => //; case. move => tF; apply /setC_P;split => //; first by apply: FE. move /Zo_P; rewrite lf_source; move=> [tE]; rewrite /g LfV//; Ytac0 => tfi. by case: (pc _ tF). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)