proposition: Lemma Cantor_Bernstein2_full f g (E:= source f) (F:= source g) (h:= fun x => E -s (Vfs g (F -s (Vfs f x)))) (m:= union (Zo (\Po E) (fun x => sub x (h x)))) (T:= Vfs g (F -s (Vfs f m))) (p := fun a y => [/\ inc y F, ~ inc y (Vfs f m) & a = Vf g y]) (f2:= Lf (fun a =>Yo (inc a T) (select (p a) F) (Vf f a)) E F): injection f -> injection g -> source f = target g -> source g = target f -> bijection_prop f2 (source f)(source g).
proof: Proof. move=> [ff injf] [fg injg] sf sg. have p1: (forall x, sub x E -> sub (h x) E) by move=> x xE; apply: sub_setC. have p2: (forall x y, sub x y -> sub y E -> sub (h x) (h y)). move=> x y xy yE; rewrite /h => t /setC_P [tE ti]. apply /setC_P;split => //; dneg aux. have q1: sub x (source f) by apply: sub_trans yE. have pa: sub (F -s Vfs f y) (source g) by apply:sub_setC. have pb: sub (F -s Vfs f x) (source g) by apply:sub_setC. move /(Vf_image_P fg pa): aux => [u] /setC_P [uF nuy] Wu. apply /(Vf_image_P fg pb); exists u => //;apply /setC_P;split =>//; dneg aux2. move /(Vf_image_P ff q1): aux2 => [s sx ->]; apply /(Vf_image_P ff yE). by exists s=> //; apply: xy. move: (Cantor_Bernstein_aux p1 p2) => []. rewrite -/m /h -/T => mE hm. have sc: sub (F -s (Vfs f m)) (source g) by apply: sub_setC. set Pa := (Vf_image_P fg sc); set Pb := (Vf_image_P ff mE). have TE: (sub T E) by move=> t /Pa [u] /setC_P [uF _] ->; rewrite /E sf; Wtac. move: (setC_K TE); rewrite hm => cEm. have sp: forall a, inc a T -> p a (select (p a) F). move => a aT; apply: (proj1 (select_pr _ _)). by move: aT => /Pa [u] /setC_P [uF num] Wu;ex_tac. move => // x y xF [_ _ xa] yF [_ _ ya]. by apply: injg => //; rewrite -xa -ya. rewrite /f2/bijection_prop; saw; apply: lf_bijective. + move=> z zE /=;Ytac zT; [ exact (proj31 (sp _ zT)) | rewrite /F; Wtac]. + move=> u v uE vE; rewrite /f2; Ytac uT; Ytac vT=> aux. - by move: (sp _ uT) (sp _ vT)=> [_ _ W1] [_ _ W2]; rewrite W1 W2 aux. - move: (sp _ uT) => [f1u nf1i Wf1] ; case: nf1i; apply /Pb. by rewrite aux;exists v => //; rewrite -hm;apply /setC_P. - move: (sp _ vT) => [f1u nf1i Wf1]; case: nf1i; apply /Pb. by rewrite -aux;exists u => //; rewrite -hm;apply /setC_P. - by apply: injf. + move=> y yF; case: (inc_or_not y (Vfs f m)). move /Pb => [u um Wy]; exists u; first by apply: (mE). by rewrite /f2 Y_false //; move: um; rewrite - hm => /setC_P []. move=> aux; exists (Vf g y); first by rewrite /E; Wtac. have wt: inc (Vf g y) T by apply /Pa; exists y => //; apply /setC_P. rewrite /f2; Ytac0; move: (sp _ wt) => [q1 q2 q3]. by symmetry; apply: injg. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)