proposition: Theorem CantorBernstein_v1 X Y f g : injection_prop f X Y -> injection_prop g Y X -> bijection_prop (cantor_bernstein_bij_v1 X Y f g) X Y.
proof: Proof. move=> [[ff1 if1] sf1 tf1] [if2 sf2 tf2]. rewrite /cantor_bernstein_bij_v1. set Z := Vfs g Y. set f3 := inverse_fun (restriction1 g (source g)). have f3p: bijection_prop f3 Z Y. move:(restriction1_fb if2 (@sub_refl (source g))) => fb. apply: inverse_bij_bp; split => //; rewrite /restriction1; aw; ue. pose h w := Vf g (Vf f w). set (A := Zo (\Po X)(fun x=> forall y, inc y x -> inc (Vf g (Vf f y)) x)). set D := intersection (Zo A (sub (X -s Z))). set f4 := (Lf (fun y => Yo (inc y D) (h y) y) X Z). suff f4p: (bijection_prop f4 X Z). exact: (compose_bp f4p f3p). rewrite /f4; saw. have fg := (proj1 if2). move: (f_range_graph fg) => rg2. move: (ImfE fg); rewrite /Imf sf2 -/Z => zv. have FE: sub Z X by rewrite zv -tf2; apply f_range_graph. have tf: (forall x, inc x X -> inc (h x) Z). move=> x xs. apply/(Vf_image_P fg); first by rewrite - sf2;fprops. exists (Vf f x) => //;Wtac. have fi:{inc X &, injective h}. rewrite - sf1 /g; move=> x y xs ys sg; apply: (if1 _ _ xs ys). apply: (proj2 if2) => //;rewrite sf2 -tf1;Wtac. have AE:sub A (\Po X) by apply: Zo_S. set (B:= X -s Z). set (C:= Zo A (sub B)). have EC: inc X C. apply: Zo_i; last by apply: sub_setC. apply: Zo_i; fprops; first by apply :setP_Ti. by move => y yx; apply: FE; apply: tf. have p1: forall x, inc x C -> sub D x. move=> x xC t tD; apply: (setI_hi tD xC). have DA: inc D A. apply: Zop_i; first by apply: setI_s1. move=> y yD; apply: setI_i; first by ex_tac. move=> t tC; move: (setI_hi yD tC) => yt. by move: tC => /Zo_P [] /Zo_hi tp _; apply: tp. have DC: inc D C. apply: Zo_i => //t tD; apply /setI_i ; first by ex_tac. by move=> y /Zo_P [_]; apply. have BD: sub B D by move: DC => /Zo_P []. have cEB: (X -s B = Z) by apply: setC_K. have Dst: (forall y, inc y D -> inc (h y) D) by move: DA => /Zo_P []. apply: lf_bijective. move=> y yE /=; Ytac yD; first by apply: tf. rewrite - cEB; apply/setC_P; split => //; fprops. move=> u v uE vE; Ytac uD; Ytac vD => //; try (apply: fi => //). by move=> hi; rewrite -hi in vD; case: vD; apply: Dst. by move=> hi; rewrite hi in uD; case: uD; apply: Dst. move=> y yF; move: (yF); rewrite - cEB => /setC_P [yE nyB]. case: (inc_or_not y D) => yD; last by exists y => //; Ytac0. have DE:sub D X by move: DA => /Zo_P [] /setP_P. set (T:= D -s1 y). have BT: sub B T. by move=> t tB; apply /setC1_P; split; [ apply: BD | dneg ty; rewrite -ty]. have TA: (~ (inc T A)). move=> TA. by move: ((p1 _ (Zo_i TA BT)) _ yD) => /setC1_P [_]. have [x xT nfT]: exists2 x, inc x T & ~ (inc (h x) T). ex_middle bad; case: TA;apply: Zo_i => //. apply /setP_P; apply: sub_trans DE; apply: sub_setC. move=> z zT; case: (inc_or_not (h z) T) => //; move => nfzt; case:bad; ex_tac. move: xT => /setC1_P [xD nxy]. exists x; first by apply: DE. Ytac0;ex_middle fxy; case: nfT; apply /setC1_P; split; fprops. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)