proposition: Lemma Exercise6_3 E: infinite_set E -> (\Po E) \Eq (Zo (\Po E) (fun z => z \Eq E)).
proof: Proof. move=> isE; set Qo:= Zo _ _. apply /card_eqP;apply: cleA; last first. have sQ: (sub Qo (\Po E)) by apply: Zo_S. apply: (sub_smaller sQ). set (n:= cardinal E). have cnn: (n +c n = n). have cnn: (n <=c n) by rewrite /n; fprops. move: isE => /infinite_setP isE. apply: (csum_inf cnn isE). have enE: n =c E by rewrite /n; aw. set (E1:= E *s1 C0); set(E2:= E *s1 C1). have d12: (disjoint E1 E2) by apply: disjointU2_pr; fprops. move: (csum2_pr5 d12); rewrite - csum2cl - csum2cr. rewrite !cardinal_indexed cnn; move /card_eqP => [g [bg sg tg]]. have fg: function g by fct_tac. pose barX X:= ((X *s1 C0) \cup E2). pose f X := Vfs g (barX X). have barXp: forall X, sub X E -> sub (barX X) (source g). move => X XE s; rewrite sg; case /setU2_P => //; last by fprops. move/indexed_P=> [ps PX Qs]; apply /setU2_P;left; apply /indexed_P; aw. by split => //; apply XE. have sfE:(forall X, sub X E -> sub (f X) E). move=> X XE t; move: (barXp _ XE) => bE; move /(Vf_image_P fg bE). rewrite -tg;move=> [u ub ->]; apply: Vf_target => //;apply: bE => //. have ei: (forall X, sub X E -> (f X) \Eq E). move=> X XE; move: (sfE _ XE) => ssfE. apply/card_eqP;apply: (cleA (sub_smaller ssfE)). have <-: (cardinal E2 = cardinal E) by exact: cardinal_indexed. have sE2: (sub E2 (source g)) by rewrite sg;apply: subsetU2r. move: (bg) => [bg1 _]. move/card_eqP: (Eq_restriction1 sE2 bg1) => ->. apply:sub_smaller;apply: dirim_S; apply: subsetU2r. have ta: (lf_axiom f (\Po E) Qo). move => X /setP_P XE; apply: Zo_i;fprops;apply /setP_P; apply: sfE =>//. set (F:= Lf f (\Po E) Qo). have ->: (\Po E = source F) by rewrite /F; aw. have ->: (Qo = target F) by rewrite /F; aw. apply: inj_source_smaller. apply: lf_injective => // a b /setP_P aE /setP_P bE; move: aE bE. suff: forall u v, sub u E -> sub v E -> f u = f v -> sub u v. move=> h ae ve sf; apply: extensionality; apply: h => //. move => u v uE vE sf t tu. have p1: (inc (J t C0) (barX u)) by apply :setU2_1;apply :indexed_pi. move: (barXp _ uE) => p2; move: (barXp _ vE) => p2a; move: (p2 _ p1) => p3. have :(inc (Vf g (J t C0)) (f u)) by apply/(Vf_image_P fg p2); ex_tac. rewrite sf => /(Vf_image_P fg p2a) [w wb wv]; move: (p2a _ wb)=> wsg. move: bg => [[_ ig] _]; move: (ig _ _ p3 wsg wv) => wv2. move: wb; rewrite - wv2 => /setU2_P; case; move /indexed_P => [_]; aw; trivial. by move => _ bad; case: C0_ne_C1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)