(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Set Implicit Arguments.
Unset Strict Implicit.
Require Export Parts2.
(** Title "Cantor Bernstein theorem" *)
Comments
  "We prove that if there is an injection from A to B, and an injection from B to A".
Comments "then there is a bijection between A and B.".
Section Cantor_Bernstein.
Variable E F : Setoid.
Variable f : MAP E F.
Variable g : MAP F E.
Hypothesis finj : injective f.
Hypothesis ginj : injective g.

Let h (X : part_set E) := compl (image g (compl (image f X))).

Let h_incr : forall A B : part_set E, included A B -> included (h A) (h B).
(* Goal: @Equal (part_set E) (h x) (h y) *)
unfold h in |- *.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
auto with algebra.
Qed.
Hint Resolve h_incr: algebra.

Let PX : part_set (part_set E).
(* Goal: Carrier (part_set (part_set E)) *)
apply (Build_Predicate (Pred_fun:=fun A : part_set E => included A (h A))).
(* Goal: @surjective E F b *)
red in |- *.
(* Goal: forall (x y : Carrier (part_set E)) (_ : @included E x (h x)) (_ : @Equal (part_set E) y x), @included E y (h y) *)
intros x y H' H'0; try assumption.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply included_comp with x (h x); auto with algebra.
(* Goal: @Equal (part_set E) (h x) (h y) *)
unfold h in |- *.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
auto with algebra.
Defined.

Let X := union_part PX.

Let XhX : included X (h X).
(* Goal: @included E (h X) X *)
unfold X in |- *.
(* Goal: @included E (@union_part E PX) (h (@union_part E PX)) *)
apply union_part_upper_bound.
(* Goal: forall (A : Carrier (part_set E)) (_ : @in_part (part_set E) A PX), @included E A (h (@union_part E PX)) *)
intros A H'; try assumption.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply included_trans with (h A); auto with algebra.
Qed.

Let hXX : included (h X) X.
(* Goal: @included E (h X) X *)
unfold X in |- *.
(* Goal: @included E (h (@union_part E PX)) (@union_part E PX) *)
apply union_part_included.
(* Goal: @Equal F (@Ap F F (@comp_map_map F E F g1 g) x1) (@Ap F F (@comp_map_map F E F g1 g) x0) *)
(* Goal: @in_part E y (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @surjective E F b *)
simpl in |- *.
(* Goal: @included E (h (@union_part E PX)) (h (h (@union_part E PX))) *)
apply h_incr.
(* Goal: @included E X (h X) *)
exact XhX.
Qed.

Let PXeq : Equal (h X) X.
(* Goal: @Equal (part_set E) (h X) X *)
apply included_antisym.
(* Goal: @included E (h X) X *)
(* Goal: @included E X (h X) *)
exact hXX.
(* Goal: @included E X (h X) *)
exact XhX.
Qed.
Hint Resolve PXeq hXX XhX: algebra.

Let img : Equal (image g (compl (image f X))) (compl X).
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Trans with (compl (h X)); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
unfold h in |- *; auto with algebra.
Qed.
Hint Resolve img: algebra.
Hypothesis
  partial_section :
    forall (E F : Setoid) (f : MAP E F),
    injective f -> exists g : MAP F E, Equal (comp_map_map g f) (Id E).
Hypothesis
  map_extend :
    forall (E F : Setoid) (f g : MAP E F) (A : part_set E),
    exists b : MAP E F,
      (forall x : E, in_part x A -> Equal (b x) (f x)) /\
      (forall x : E, ~ in_part x A -> Equal (b x) (g x)).

Theorem Cantor_Berstein : exists b : MAP E F, bijective b.
(* Goal: @ex (Carrier (MAP E F)) (fun b : Carrier (MAP E F) => @bijective E F b) *)
case (partial_section ginj).
(* Goal: forall (x : Carrier (MAP E F)) (_ : @Equal (MAP F F) (@comp_map_map F E F x g) (Id F)), @ex (Carrier (MAP E F)) (fun b : Carrier (MAP E F) => @bijective E F b) *)
intros g1 H'; try assumption.
(* Goal: @ex (Carrier (MAP E F)) (fun b : Carrier (MAP E F) => @bijective E F b) *)
case (map_extend f g1 X).
(* Goal: forall (x : Carrier (MAP E F)) (_ : and (forall (x0 : Carrier E) (_ : @in_part E x0 X), @Equal F (@Ap E F x x0) (@Ap E F f x0)) (forall (x0 : Carrier E) (_ : not (@in_part E x0 X)), @Equal F (@Ap E F x x0) (@Ap E F g1 x0))), @ex (Carrier (MAP E F)) (fun b : Carrier (MAP E F) => @bijective E F b) *)
intros b H'1; try assumption.
(* Goal: @ex (Carrier (MAP E F)) (fun b : Carrier (MAP E F) => @bijective E F b) *)
exists b; try assumption.
(* Goal: @bijective E F b *)
elim H'1; intros H'2 H'3; try exact H'2; clear H'1.
(* Goal: @surjective E F b *)
red in |- *.
(* Goal: and (@injective E F b) (@surjective E F b) *)
split; [ try assumption | idtac ].
(* Goal: @surjective E F b *)
red in |- *.
(* Goal: forall (x y : Carrier E) (_ : @Equal F (@Ap E F b x) (@Ap E F b y)), @Equal E x y *)
(* Goal: @surjective E F b *)
intros x y H'0; try assumption.
(* Goal: @Equal E x y *)
(* Goal: @surjective E F b *)
case (compl_not_compl X x); intros.
(* Goal: @Equal E x y *)
(* Goal: @surjective E F b *)
case (compl_not_compl X y); intros.
(* Goal: @Equal E x y *)
(* Goal: @Equal E x y *)
(* Goal: @Equal E x y *)
(* Goal: @surjective E F b *)
apply finj.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Trans with (b y); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Trans with (b x); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Sym; auto with algebra.
(* Goal: forall _ : @in_part E x (@image F E g (@compl F (@image E F f X))), @Equal E x y *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @surjective E F b *)
cut (in_part y (image g (compl (image f X)))).
(* Goal: forall _ : @in_part E x (@image F E g (@compl F (@image E F f X))), @Equal E x y *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @Equal E x y *)
(* Goal: @surjective E F b *)
intros H'1; try assumption.
(* Goal: @Equal E x y *)
(* Goal: @in_part E y (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @surjective E F b *)
generalize (image_in H'1).
(* Goal: forall _ : @ex (Carrier F) (fun x0 : Carrier F => and (@in_part F x0 (@compl F (@image E F f X))) (@Equal E x (@Ap F E g x0))), @Equal E x y *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @Equal E x y *)
(* Goal: @surjective E F b *)
intros H'4; try assumption.
(* Goal: @Equal E x y *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @Equal E x y *)
(* Goal: @surjective E F b *)
elim H'4; intros x0 E0; try exact E0; clear H'4.
(* Goal: @Equal E x y *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @Equal E x y *)
(* Goal: @surjective E F b *)
elim E0; intros H'4 H'5; try exact H'5; clear E0.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
absurd (in_part x0 (compl (image f X))); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply not_in_comp_l with (Ap (Id F) x0); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply not_in_comp_l with (Ap (comp_map_map g1 g) x0); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply not_in_comp_l with (Ap g1 (Ap g x0)); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply not_in_comp_l with (Ap g1 y); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply not_in_comp_l with (Ap b y); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply not_in_comp_l with (Ap b x); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply not_in_comp_l with (Ap f x); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Sym; auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply in_part_comp_r with (compl X); auto with algebra.
(* Goal: @Equal E x y *)
(* Goal: @surjective E F b *)
case (compl_not_compl X y); intros.
(* Goal: @Equal E x y *)
(* Goal: @surjective E F b *)
cut (in_part x (image g (compl (image f X)))).
(* Goal: forall _ : @in_part E x (@image F E g (@compl F (@image E F f X))), @Equal E x y *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @Equal E x y *)
(* Goal: @surjective E F b *)
intros H'1; try assumption.
(* Goal: @Equal E x y *)
(* Goal: @in_part E y (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @surjective E F b *)
generalize (image_in H'1).
(* Goal: forall _ : @ex (Carrier F) (fun x0 : Carrier F => and (@in_part F x0 (@compl F (@image E F f X))) (@Equal E x (@Ap F E g x0))), @Equal E x y *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @Equal E x y *)
(* Goal: @surjective E F b *)
intros H'4; try assumption.
(* Goal: @Equal E x y *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @Equal E x y *)
(* Goal: @surjective E F b *)
elim H'4; intros x0 E0; try exact E0; clear H'4.
(* Goal: @Equal E x y *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @Equal E x y *)
(* Goal: @surjective E F b *)
elim E0; intros H'4 H'5; try exact H'5; clear E0.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
absurd (in_part x0 (compl (image f X))); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply not_in_comp_l with (Ap (Id F) x0); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply not_in_comp_l with (Ap (comp_map_map g1 g) x0); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply not_in_comp_l with (Ap g1 (Ap g x0)); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply not_in_comp_l with (Ap g1 x); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply not_in_comp_l with (Ap b x); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply not_in_comp_l with (Ap b y); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply not_in_comp_l with (Ap f y); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Sym; auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply in_part_comp_r with (compl X); auto with algebra.
(* Goal: @Equal E x y *)
(* Goal: @surjective E F b *)
cut (in_part x (image g (compl (image f X)))).
(* Goal: forall _ : @in_part E x (@image F E g (@compl F (@image E F f X))), @Equal E x y *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @surjective E F b *)
cut (in_part y (image g (compl (image f X)))).
(* Goal: forall (_ : @in_part E y (@image F E g (@compl F (@image E F f X)))) (_ : @in_part E x (@image F E g (@compl F (@image E F f X)))), @Equal E x y *)
(* Goal: @in_part E y (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @surjective E F b *)
intros H'1 H'4; try assumption.
(* Goal: @Equal E x y *)
(* Goal: @in_part E y (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @surjective E F b *)
generalize (image_in H'1).
(* Goal: forall _ : @ex (Carrier F) (fun x : Carrier F => and (@in_part F x (@compl F (@image E F f X))) (@Equal E y (@Ap F E g x))), @Equal E x y *)
(* Goal: @in_part E y (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @surjective E F b *)
generalize (image_in H'4).
(* Goal: forall (_ : @ex (Carrier F) (fun x0 : Carrier F => and (@in_part F x0 (@compl F (@image E F f X))) (@Equal E x (@Ap F E g x0)))) (_ : @ex (Carrier F) (fun x : Carrier F => and (@in_part F x (@compl F (@image E F f X))) (@Equal E y (@Ap F E g x)))), @Equal E x y *)
(* Goal: @in_part E y (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @surjective E F b *)
intros H'5 H'6; try assumption.
(* Goal: @Equal E x y *)
(* Goal: @in_part E y (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @surjective E F b *)
elim H'6; intros x0 E0; elim E0; intros H'7 H'8; try exact H'7; clear E0 H'6.
(* Goal: @Equal E x y *)
(* Goal: @in_part E y (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @surjective E F b *)
elim H'5; intros x1 E0; elim E0; intros H'6 H'9; try exact H'6; clear E0 H'5.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Trans with (Ap g x1); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Trans with (Ap g x0); auto with algebra.
(* Goal: @Equal E (@Ap F E g x1) (@Ap F E g x0) *)
(* Goal: @in_part E y (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @surjective E F b *)
cut (Equal x1 x0).
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
auto with algebra.
(* Goal: @Equal F x1 x0 *)
(* Goal: @in_part E y (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @surjective E F b *)
cut (Equal (Ap (Id F) x1) (Ap (Id F) x0)).
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
auto with algebra.
(* Goal: @Equal F (@Ap F F (Id F) x1) (@Ap F F (Id F) x0) *)
(* Goal: @in_part E y (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @surjective E F b *)
cut (Equal (Ap (comp_map_map g1 g) x1) (Ap (comp_map_map g1 g) x0)).
(* Goal: forall _ : @Equal F (@Ap F F (@comp_map_map F E F g1 g) x1) (@Ap F F (@comp_map_map F E F g1 g) x0), @Equal F (@Ap F F (Id F) x1) (@Ap F F (Id F) x0) *)
(* Goal: @Equal F (@Ap F F (@comp_map_map F E F g1 g) x1) (@Ap F F (@comp_map_map F E F g1 g) x0) *)
(* Goal: @in_part E y (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @surjective E F b *)
intros H'5; try assumption.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Trans with (Ap (comp_map_map g1 g) x0); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Trans with (Ap (comp_map_map g1 g) x1); auto with algebra.
(* Goal: @Equal F (@Ap F F (@comp_map_map F E F g1 g) x1) (@Ap F F (@comp_map_map F E F g1 g) x0) *)
(* Goal: @in_part E y (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @surjective E F b *)
simpl in |- *.
(* Goal: @Equal F (@comp_map_fun F E F g1 g x1) (@comp_map_fun F E F g1 g x0) *)
(* Goal: @in_part E y (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @in_part E x (@image F E g (@compl F (@image E F f X))) *)
(* Goal: @surjective E F b *)
unfold comp_map_fun in |- *.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Trans with (Ap g1 x); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Trans with (Ap g1 y); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Trans with (Ap b x); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Sym; auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Trans with (Ap b y); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply in_part_comp_r with (compl X); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply in_part_comp_r with (compl X); auto with algebra.
(* Goal: @surjective E F b *)
red in |- *.
(* Goal: forall y : Carrier F, @ex (Carrier E) (fun x : Carrier E => @Equal F y (@Ap E F b x)) *)
intros y; try assumption.
(* Goal: @ex (Carrier E) (fun x : Carrier E => @Equal F y (@Ap E F b x)) *)
case (compl_not_compl (image f X) y); intros.
(* Goal: @ex (Carrier E) (fun x : Carrier E => @Equal F y (@Ap E F b x)) *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => @Equal F y (@Ap E F b x)) *)
generalize (image_in H).
(* Goal: forall _ : @ex (Carrier E) (fun x : Carrier E => and (@in_part E x X) (@Equal F y (@Ap E F f x))), @ex (Carrier E) (fun x : Carrier E => @Equal F y (@Ap E F b x)) *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => @Equal F y (@Ap E F b x)) *)
intros H'0; try assumption.
(* Goal: @ex (Carrier E) (fun x : Carrier E => @Equal F y (@Ap E F b x)) *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => @Equal F y (@Ap E F b x)) *)
elim H'0; intros x E0; elim E0; intros H'1 H'4; try exact H'1; clear E0 H'0.
(* Goal: @ex (Carrier E) (fun x : Carrier E => @Equal F y (@Ap E F b x)) *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => @Equal F y (@Ap E F b x)) *)
exists x; try assumption.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Trans with (Ap f x); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Sym; auto with algebra.
(* Goal: @ex (Carrier E) (fun x : Carrier E => @Equal F y (@Ap E F b x)) *)
exists (g y); try assumption.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Trans with (Ap g1 (Ap g y)); auto with algebra.
(* Goal: @Equal F (@Ap E F g1 (@Ap F E g y)) (@Ap E F b (@Ap F E g y)) *)
apply Sym.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Trans with (Ap (Id F) y); auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply Trans with (Ap (comp_map_map g1 g) y); auto with algebra.
(* Goal: @Equal F (@Ap E F g1 (@Ap F E g y)) (@Ap E F b (@Ap F E g y)) *)
apply Sym.
(* Goal: @Equal F (@Ap E F b (@Ap F E g y)) (@Ap E F g1 (@Ap F E g y)) *)
apply H'3.
(* Goal: not (@in_part E (@Ap F E g y) X) *)
cut (in_part (Ap g y) (compl X)).
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
auto with algebra.
(* Goal: forall _ : @in_part E (@Ap F E g y) (@compl E X), not (@in_part E (@Ap F E g y) X) *)
(* Goal: @in_part E (@Ap F E g y) (@compl E X) *)
apply in_part_comp_r with (image g (compl (image f X))); auto with algebra.
Qed.
End Cantor_Bernstein.