(* 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 Classical_Prop.
Require Export Parts.
(** Title "Complement, images." *)
Comments "We define here complement of a part, image of a part by a map.".
Section Complement1.
Variable E : Setoid.

Lemma not_in_comp_l :
 forall (E : Setoid) (A : part_set E) (x y : E),
 ~ in_part x A -> Equal y x -> ~ in_part y A.
(* Goal: or (@in_part E x A) (not (@in_part E x A)) *)
unfold not in |- *.
(* Goal: forall (E : Setoid) (A : Carrier (part_set E)) (x y : Carrier E) (_ : forall _ : @in_part E x A, False) (_ : @Equal E y x) (_ : @in_part E y A), False *)
intros E0 A x y H' H'0 H'1; try assumption.
(* Goal: False *)
apply H'.
(* Goal: @in_part E0 x A *)
apply in_part_comp_l with y; auto with algebra.
Qed.

Lemma not_in_comp_r :
 forall (E : Setoid) (A B : part_set E) (x : E),
 ~ in_part x A -> Equal A B -> ~ in_part x B.
(* Goal: or (@in_part E x A) (not (@in_part E x A)) *)
unfold not in |- *.
(* Goal: forall (E : Setoid) (A B : Carrier (part_set E)) (x : Carrier E) (_ : forall _ : @in_part E x A, False) (_ : @Equal (part_set E) A B) (_ : @in_part E x B), False *)
intros E0 A B x H' H'0 H'1; try assumption.
(* Goal: False *)
apply H'.
(* Goal: @in_part E0 x A *)
apply in_part_comp_r with B; auto with algebra.
Qed.

Definition compl : part_set E -> part_set E.
(* Goal: forall _ : Carrier (part_set E), Carrier (part_set F) *)
intros A.
(* Goal: Carrier (part_set E) *)
apply (Build_Predicate (Pred_fun:=fun x : E => ~ in_part x A)).
(* Goal: forall A : Carrier (part_set E), @surjective (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image F (@part F (image A))) (surj_part_image A) *)
red in |- *.
(* Goal: forall (x y : Carrier E) (_ : not (@in_part E x A)) (_ : @Equal E y x), not (@in_part E y A) *)
intros x y H' H'0; try assumption.
(* Goal: not (@in_part E y A) *)
apply not_in_comp_l with x; auto with algebra.
Defined.

Lemma compl_in :
 forall (A : part_set E) (x : E), ~ in_part x A -> in_part x (compl A).
(* Goal: forall (A : Carrier (part_set E)) (x : Carrier E) (_ : @in_part E x A), @in_part F (@Ap E F f x) (image A) *)
simpl in |- *; auto with algebra.
Qed.
Hint Resolve compl_in: algebra.

Lemma in_compl :
 forall (A : part_set E) (x : E), in_part x (compl A) -> ~ in_part x A.
(* Goal: forall (A : Carrier (part_set E)) (x : Carrier E) (_ : @in_part E x A), @in_part F (@Ap E F f x) (image A) *)
simpl in |- *; auto with algebra.
Qed.

Lemma compl_comp :
 forall A B : part_set E, Equal A B -> Equal (compl A) (compl B).
(* Goal: forall (A : Carrier (part_set E)) (x : Carrier E) (_ : @in_part E x A), @in_part F (@Ap E F f x) (image A) *)
simpl in |- *; auto with algebra.
(* Goal: forall A : Predicate E, @eq_part E (compl (compl A)) A *)
unfold eq_part in |- *; auto with algebra.
(* Goal: forall (A B : Predicate E) (_ : forall x : Carrier E, and (forall (_ : forall _ : @in_part E x A, False) (_ : @in_part E x B), False) (forall (_ : forall _ : @in_part E x B, False) (_ : @in_part E x A), False)) (x : Carrier E), and (forall _ : @in_part E x A, @in_part E x B) (forall _ : @in_part E x B, @in_part E x A) *)
intros A B H' x; try assumption.
(* Goal: and (forall _ : @in_part E x A, @in_part E x B) (forall _ : @in_part E x B, @in_part E x A) *)
elim (H' x).
(* Goal: or (@in_part E x A) (not (@in_part E x A)) *)
simpl in |- *; unfold not in |- *.
(* Goal: forall (_ : forall _ : @in_part E x A, @in_part E x B) (_ : forall _ : @in_part E x B, @in_part E x A), and (forall (_ : forall _ : @in_part E x A, False) (_ : @in_part E x B), False) (forall (_ : forall _ : @in_part E x B, False) (_ : @in_part E x A), False) *)
intuition.
Qed.
Hint Resolve compl_comp: algebra.

Lemma compl_comp_rev :
 forall A B : part_set E, Equal (compl A) (compl B) -> Equal A B.
(* Goal: forall (A : Carrier (part_set E)) (x : Carrier E) (_ : @in_part E x A), @in_part F (@Ap E F f x) (image A) *)
simpl in |- *; auto with algebra.
(* Goal: forall A : Predicate E, @eq_part E (compl (compl A)) A *)
unfold eq_part in |- *; auto with algebra.
(* Goal: or (@in_part E x A) (not (@in_part E x A)) *)
simpl in |- *; unfold not in |- *.
(* Goal: forall (A B : Predicate E) (_ : forall x : Carrier E, and (forall (_ : forall _ : @in_part E x A, False) (_ : @in_part E x B), False) (forall (_ : forall _ : @in_part E x B, False) (_ : @in_part E x A), False)) (x : Carrier E), and (forall _ : @in_part E x A, @in_part E x B) (forall _ : @in_part E x B, @in_part E x A) *)
intros A B H' x; try assumption.
(* Goal: and (forall _ : @in_part E x A, @in_part E x B) (forall _ : @in_part E x B, @in_part E x A) *)
elim (H' x).
(* Goal: forall _ : forall _ : forall _ : @in_part E x A, False, False, @in_part E x A *)
(* Goal: forall (_ : @in_part E x A) (_ : forall _ : @in_part E x A, False), False *)
apply NNPP.
(* Goal: forall (_ : @in_part E x A) (_ : forall _ : @in_part E x A, False), False *)
tauto.
Qed.

Lemma compl_compl : forall A : part_set E, Equal (compl (compl A)) A.
(* Goal: forall (A : Carrier (part_set E)) (x : Carrier E) (_ : @in_part E x A), @in_part F (@Ap E F f x) (image A) *)
simpl in |- *; auto with algebra.
(* Goal: forall A : Predicate E, @eq_part E (compl (compl A)) A *)
unfold eq_part in |- *; auto with algebra.
(* Goal: or (@in_part E x A) (not (@in_part E x A)) *)
simpl in |- *; unfold not in |- *.
(* Goal: forall (A : Carrier (part_set E)) (_ : Carrier (@set_of_subtype_image E (@part E A))), Carrier (@set_of_subtype_image F (@part F (image A))) *)
intros A x; try assumption.
(* Goal: and (forall _ : forall _ : forall _ : @in_part E x A, False, False, @in_part E x A) (forall (_ : @in_part E x A) (_ : forall _ : @in_part E x A, False), False) *)
split; [ try assumption | idtac ].
(* Goal: forall _ : forall _ : forall _ : @in_part E x A, False, False, @in_part E x A *)
(* Goal: forall (_ : @in_part E x A) (_ : forall _ : @in_part E x A, False), False *)
apply NNPP.
(* Goal: forall (_ : @in_part E x A) (_ : forall _ : @in_part E x A, False), False *)
tauto.
Qed.
Hint Resolve compl_compl: algebra.

Lemma compl_not_in :
 forall (A : part_set E) (x : E), in_part x A -> ~ in_part x (compl A).
(* Goal: forall (A : Carrier (part_set E)) (x : Carrier E) (_ : @in_part E x A), @in_part F (@Ap E F f x) (image A) *)
simpl in |- *; auto with algebra.
Qed.
Hint Resolve compl_not_in: algebra.

Lemma not_in_compl :
 forall (A : part_set E) (x : E), in_part x (compl A) -> ~ in_part x A.
(* Goal: forall (A : Carrier (part_set E)) (x : Carrier E) (_ : @in_part E x A), @in_part F (@Ap E F f x) (image A) *)
simpl in |- *; auto with algebra.
Qed.

Lemma compl_included :
 forall A B : part_set E, included A B -> included (compl B) (compl A).
(* Goal: @included F (image A) (image B) *)
unfold included in |- *.
(* Goal: forall (A : Carrier (part_set E)) (x : Carrier E) (_ : @in_part E x A), @in_part F (@Ap E F f x) (image A) *)
simpl in |- *; auto with algebra.
Qed.

Lemma compl_not_compl :
 forall (A : part_set E) (x : E), in_part x A \/ in_part x (compl A).
(* Goal: forall (A : Carrier (part_set E)) (_ : Carrier (@set_of_subtype_image E (@part E A))), Carrier (@set_of_subtype_image F (@part F (image A))) *)
intros A x; try assumption.
(* Goal: forall (subtype_elt0 : Carrier E) (subtype_prf : @Pred_fun E A subtype_elt0) (subtype_elt1 : Carrier E) (subtype_prf0 : @Pred_fun E A subtype_elt1) (_ : @Equal E (@subtype_elt E A (@Build_subtype E A subtype_elt1 subtype_prf0)) (@subtype_elt E A (@Build_subtype E A subtype_elt0 subtype_prf))), @Equal F (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt1 subtype_prf0))) (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt0 subtype_prf))) *)
simpl in |- *.
(* Goal: or (@in_part E x A) (not (@in_part E x A)) *)
unfold not in |- *.
(* Goal: forall (_ : forall _ : @in_part E x A, @in_part E x B) (_ : forall _ : @in_part E x B, @in_part E x A), and (forall (_ : forall _ : @in_part E x A, False) (_ : @in_part E x B), False) (forall (_ : forall _ : @in_part E x B, False) (_ : @in_part E x A), False) *)
apply NNPP; intuition.
Qed.
End Complement1.
Hint Resolve compl_included compl_not_in compl_compl compl_comp compl_in:
  algebra.
Section Images1.
Variable E F : Setoid.
Variable f : MAP E F.

Definition image : part_set E -> part_set F.
(* Goal: forall _ : Carrier (part_set E), Carrier (part_set F) *)
intros A.
apply
 (Build_Predicate
    (Pred_fun:=fun y : F => exists x : E, in_part x A /\ Equal y (f x))).
(* Goal: forall A : Carrier (part_set E), @surjective (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image F (@part F (image A))) (surj_part_image A) *)
red in |- *.
(* Goal: forall (x y : Carrier F) (_ : @ex (Carrier E) (fun x0 : Carrier E => and (@in_part E x0 A) (@Equal F x (@Ap E F f x0)))) (_ : @Equal F y x), @ex (Carrier E) (fun x0 : Carrier E => and (@in_part E x0 A) (@Equal F y (@Ap E F f x0))) *)
intros y y' H' H'0; try assumption.
(* Goal: @ex (Carrier E) (fun x : Carrier E => and (@in_part E x A) (@Equal F y' (@Ap E F f x))) *)
elim H'; intros x E0; elim E0; intros H'1 H'2; try exact H'1; clear E0 H'.
(* Goal: and (forall _ : forall _ : forall _ : @in_part E x A, False, False, @in_part E x A) (forall (_ : @in_part E x A) (_ : forall _ : @in_part E x A, False), False) *)
exists x; split; [ try assumption | idtac ].
(* Goal: @Equal F y' (@Ap E F f x) *)
apply Trans with y; auto with algebra.
Defined.

Lemma image_in :
 forall (A : part_set E) (y : F),
 in_part y (image A) -> exists x : E, in_part x A /\ Equal y (f x).
(* Goal: forall (A : Carrier (part_set E)) (x : Carrier E) (_ : @in_part E x A), @in_part F (@Ap E F f x) (image A) *)
simpl in |- *; auto with algebra.
Qed.

Lemma in_image :
 forall (A : part_set E) (x : E) (y : F),
 in_part x A -> Equal y (f x) -> in_part y (image A).
(* Goal: forall (A : Carrier (part_set E)) (x : Carrier E) (_ : @in_part E x A), @in_part F (@Ap E F f x) (image A) *)
simpl in |- *; auto with algebra.
(* Goal: forall (A : Predicate E) (x : Carrier E) (y : Carrier F) (_ : @in_part E x A) (_ : @Equal F y (@Ap E F f x)), @ex (Carrier E) (fun x0 : Carrier E => and (@in_part E x0 A) (@Equal F y (@Ap E F f x0))) *)
intros A x y H' H'0; try assumption.
(* Goal: @ex (Carrier E) (fun x0 : Carrier E => and (@in_part E x0 A) (@Equal F (@Ap E F f x) (@Ap E F f x0))) *)
exists x; split; [ try assumption | idtac ]; auto with algebra.
Qed.
Hint Resolve in_image: algebra.

Lemma image_included :
 forall A B : part_set E, included A B -> included (image A) (image B).
(* Goal: forall (A B : Carrier (part_set E)) (_ : @Equal (part_set E) A B), @Equal (part_set F) (image A) (image B) *)
intros A B H'; try assumption.
(* Goal: @included F (image A) (image B) *)
unfold included in |- *.
(* Goal: forall (x : Carrier F) (_ : @in_part F x (image A)), @in_part F x (image B) *)
intros x H'0; try assumption.
(* Goal: @in_part F x (image B) *)
elim H'0.
(* Goal: forall (x0 : Carrier E) (_ : and (@in_part E x0 A) (@Equal F x (@Ap E F f x0))), @in_part F x (image B) *)
intros x0 H'1; try assumption.
(* Goal: @in_part F x (image B) *)
apply in_image with (x := x0); auto with algebra.
(* Goal: @in_part E x0 B *)
(* Goal: @Equal F x (@Ap E F f x0) *)
red in H'.
(* Goal: @in_part E x0 B *)
(* Goal: @Equal F x (@Ap E F f x0) *)
elim H'1.
(* Goal: forall (subtype_elt : Carrier E) (_ : @Pred_fun E A subtype_elt) (subtype_elt0 : Carrier E) (_ : @Pred_fun E A subtype_elt0) (_ : @Equal E subtype_elt0 subtype_elt), @Equal F (@Ap E F f subtype_elt0) (@Ap E F f subtype_elt) *)
auto with algebra.
(* Goal: forall (subtype_elt : Carrier E) (_ : @Pred_fun E A subtype_elt) (subtype_elt0 : Carrier E) (_ : @Pred_fun E A subtype_elt0) (_ : @Equal E subtype_elt0 subtype_elt), @Equal F (@Ap E F f subtype_elt0) (@Ap E F f subtype_elt) *)
elim H'1; auto with algebra.
Qed.
Hint Resolve image_included: algebra.

Lemma image_comp :
 forall A B : part_set E, Equal A B -> Equal (image A) (image B).
(* Goal: forall (A B : Carrier (part_set E)) (_ : @Equal (part_set E) A B), @Equal (part_set F) (image A) (image B) *)
intros A B H'; try assumption.
(* Goal: forall (subtype_elt : Carrier E) (_ : @Pred_fun E A subtype_elt) (subtype_elt0 : Carrier E) (_ : @Pred_fun E A subtype_elt0) (_ : @Equal E subtype_elt0 subtype_elt), @Equal F (@Ap E F f subtype_elt0) (@Ap E F f subtype_elt) *)
apply included_antisym; auto with algebra.
Qed.
Hint Resolve image_comp: algebra.

Lemma image_in_image :
 forall (A : part_set E) (x : E), in_part x A -> in_part (f x) (image A).
(* Goal: forall (A : Carrier (part_set E)) (x : Carrier E) (_ : @in_part E x A), @in_part F (@Ap E F f x) (image A) *)
simpl in |- *; auto with algebra.
(* Goal: forall (A : Predicate E) (x : Carrier E) (_ : @in_part E x A), @ex (Carrier E) (fun x0 : Carrier E => and (@in_part E x0 A) (@Equal F (@Ap E F f x) (@Ap E F f x0))) *)
intros A x H'; try assumption.
(* Goal: @ex (Carrier E) (fun x0 : Carrier E => and (@in_part E x0 A) (@Equal F (@Ap E F f x) (@Ap E F f x0))) *)
exists x; split; [ try assumption | idtac ]; auto with algebra.
Qed.
Hint Resolve image_in_image: algebra.

Definition image_map := image (full E).

Let surj_set_image_fun : E -> image_map.
(* Goal: forall _ : Carrier E, Carrier (@set_of_subtype_image F (@part F image_map)) *)
intros x; try assumption.
(* Goal: forall y : @subtype F image_map, @ex (Carrier E) (fun x : Carrier E => @Equal F (@subtype_elt F image_map y) (@Ap E F f x)) *)
unfold image_map in |- *.
(* Goal: forall (subtype_elt0 : Carrier E) (subtype_prf : @Pred_fun E A subtype_elt0) (subtype_elt1 : Carrier E) (subtype_prf0 : @Pred_fun E A subtype_elt1) (_ : @Equal E (@subtype_elt E A (@Build_subtype E A subtype_elt1 subtype_prf0)) (@subtype_elt E A (@Build_subtype E A subtype_elt0 subtype_prf))), @Equal F (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt1 subtype_prf0))) (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt0 subtype_prf))) *)
simpl in |- *.
(* Goal: @subtype F (image (full E)) *)
cut (in_part (f x) (image (full E))).
(* Goal: forall _ : @in_part F (@Ap E F f x) (image (full E)), @subtype F (image (full E)) *)
(* Goal: @in_part F (@Ap E F f x) (image (full E)) *)
intros H'; try assumption.
(* Goal: @subtype F (image (full E)) *)
(* Goal: @in_part F (@Ap E F f x) (image (full E)) *)
apply (Build_subtype (P:=image (full E)) (subtype_elt:=f x) H').
(* Goal: forall (subtype_elt : Carrier E) (_ : @Pred_fun E A subtype_elt) (subtype_elt0 : Carrier E) (_ : @Pred_fun E A subtype_elt0) (_ : @Equal E subtype_elt0 subtype_elt), @Equal F (@Ap E F f subtype_elt0) (@Ap E F f subtype_elt) *)
auto with algebra.
Defined.

Definition surj_set_image : MAP E image_map.
(* Goal: Carrier (MAP E (@set_of_subtype_image F (@part F image_map))) *)
apply (Build_Map (Ap:=surj_set_image_fun)).
(* Goal: forall A : Carrier (part_set E), @surjective (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image F (@part F (image A))) (surj_part_image A) *)
red in |- *.
(* Goal: forall (subtype_elt0 : Carrier E) (subtype_prf : @Pred_fun E A subtype_elt0) (subtype_elt1 : Carrier E) (subtype_prf0 : @Pred_fun E A subtype_elt1) (_ : @Equal E (@subtype_elt E A (@Build_subtype E A subtype_elt1 subtype_prf0)) (@subtype_elt E A (@Build_subtype E A subtype_elt0 subtype_prf))), @Equal F (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt1 subtype_prf0))) (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt0 subtype_prf))) *)
simpl in |- *.
(* Goal: forall (x y : @subtype E A) (_ : @subtype_image_equal E (@subtype E A) (@subtype_elt E A) x y), @subtype_image_equal F (@subtype F (image A)) (@subtype_elt F (image A)) (@surj_part_image_fun A x) (@surj_part_image_fun A y) *)
unfold subtype_image_equal in |- *.
(* Goal: forall (subtype_elt0 : Carrier E) (subtype_prf : @Pred_fun E A subtype_elt0) (subtype_elt1 : Carrier E) (subtype_prf0 : @Pred_fun E A subtype_elt1) (_ : @Equal E (@subtype_elt E A (@Build_subtype E A subtype_elt1 subtype_prf0)) (@subtype_elt E A (@Build_subtype E A subtype_elt0 subtype_prf))), @Equal F (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt1 subtype_prf0))) (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt0 subtype_prf))) *)
simpl in |- *.
(* Goal: forall (subtype_elt : Carrier E) (_ : @Pred_fun E A subtype_elt) (subtype_elt0 : Carrier E) (_ : @Pred_fun E A subtype_elt0) (_ : @Equal E subtype_elt0 subtype_elt), @Equal F (@Ap E F f subtype_elt0) (@Ap E F f subtype_elt) *)
auto with algebra.
Defined.

Lemma surj_set_image_surjective : surjective surj_set_image.
(* Goal: forall A : Carrier (part_set E), @surjective (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image F (@part F (image A))) (surj_part_image A) *)
red in |- *.
(* Goal: forall (subtype_elt0 : Carrier E) (subtype_prf : @Pred_fun E A subtype_elt0) (subtype_elt1 : Carrier E) (subtype_prf0 : @Pred_fun E A subtype_elt1) (_ : @Equal E (@subtype_elt E A (@Build_subtype E A subtype_elt1 subtype_prf0)) (@subtype_elt E A (@Build_subtype E A subtype_elt0 subtype_prf))), @Equal F (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt1 subtype_prf0))) (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt0 subtype_prf))) *)
simpl in |- *.
(* Goal: forall (x y : @subtype E A) (_ : @subtype_image_equal E (@subtype E A) (@subtype_elt E A) x y), @subtype_image_equal F (@subtype F (image A)) (@subtype_elt F (image A)) (@surj_part_image_fun A x) (@surj_part_image_fun A y) *)
unfold subtype_image_equal in |- *.
(* Goal: forall (subtype_elt0 : Carrier E) (subtype_prf : @Pred_fun E A subtype_elt0) (subtype_elt1 : Carrier E) (subtype_prf0 : @Pred_fun E A subtype_elt1) (_ : @Equal E (@subtype_elt E A (@Build_subtype E A subtype_elt1 subtype_prf0)) (@subtype_elt E A (@Build_subtype E A subtype_elt0 subtype_prf))), @Equal F (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt1 subtype_prf0))) (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt0 subtype_prf))) *)
simpl in |- *.
(* Goal: forall y : @subtype F image_map, @ex (Carrier E) (fun x : Carrier E => @Equal F (@subtype_elt F image_map y) (@Ap E F f x)) *)
unfold image_map in |- *.
(* Goal: forall y : @subtype F (image (full E)), @ex (Carrier E) (fun x : Carrier E => @Equal F (@subtype_elt F (image (full E)) y) (@Ap E F f x)) *)
intros y; try assumption.
(* Goal: forall (subtype_elt0 : Carrier E) (subtype_prf : @Pred_fun E A subtype_elt0) (_ : @Equal E (@subtype_elt E A (@Build_subtype E A subtype_elt0 subtype_prf)) (@subtype_elt E A y)), @Equal F (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt0 subtype_prf))) (@subtype_elt F (image A) (@surj_part_image_fun A y)) *)
elim y.
(* Goal: forall (subtype_elt0 : Carrier F) (subtype_prf : @Pred_fun F (image (full E)) subtype_elt0), @ex (Carrier E) (fun x : Carrier E => @Equal F (@subtype_elt F (image (full E)) (@Build_subtype F (image (full E)) subtype_elt0 subtype_prf)) (@Ap E F f x)) *)
intros x' subtype_prf; try assumption.
(* Goal: @ex (Carrier E) (fun x : Carrier E => @Equal F (@subtype_elt F (image (full E)) (@Build_subtype F (image (full E)) x' subtype_prf)) (@Ap E F f x)) *)
elim subtype_prf.
(* Goal: forall (x : Carrier E) (_ : and (@in_part E x A) (@Equal F (@subtype_elt F (image A) y) (@Ap E F f x))), @ex (Carrier (@set_of_subtype_image E (@part E A))) (fun x0 : Carrier (@set_of_subtype_image E (@part E A)) => @Equal (@set_of_subtype_image F (@part F (image A))) y (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image F (@part F (image A))) (surj_part_image A) x0)) *)
intros x H'; try assumption.
(* Goal: @ex (Carrier E) (fun x : Carrier E => @Equal F (@subtype_elt F (image (full E)) (@Build_subtype F (image (full E)) x' subtype_prf)) (@Ap E F f x)) *)
exists x; try assumption.
(* Goal: @ex (Carrier (@set_of_subtype_image E (@part E A))) (fun x : Carrier (@set_of_subtype_image E (@part E A)) => @Equal (@set_of_subtype_image F (@part F (image A))) y (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image F (@part F (image A))) (surj_part_image A) x)) *)
elim H'; intros H'0 H'1; try exact H'1; clear H'.
Qed.

Let surj_part_image_fun : forall A : part_set E, A -> image A.
(* Goal: forall (A : Carrier (part_set E)) (_ : Carrier (@set_of_subtype_image E (@part E A))), Carrier (@set_of_subtype_image F (@part F (image A))) *)
intros A x; try assumption.
(* Goal: forall _ : @Equal E (@subtype_elt E A x) (@subtype_elt E A y), @Equal F (@subtype_elt F (image A) (@surj_part_image_fun A x)) (@subtype_elt F (image A) (@surj_part_image_fun A y)) *)
elim x.
(* Goal: forall (subtype_elt : Carrier E) (_ : @Pred_fun E A subtype_elt), Carrier (@set_of_subtype_image F (@part F (image A))) *)
intros x' H'; try assumption.
(* Goal: Carrier (@set_of_subtype_image F (@part F (image A))) *)
cut (in_part (f x') (image A)).
(* Goal: forall _ : @in_part F (@Ap E F f x') (image A), Carrier (@set_of_subtype_image F (@part F (image A))) *)
(* Goal: @in_part F (@Ap E F f x') (image A) *)
intros H'0; try assumption.
(* Goal: forall (subtype_elt0 : Carrier E) (subtype_prf : @Pred_fun E A subtype_elt0) (subtype_elt1 : Carrier E) (subtype_prf0 : @Pred_fun E A subtype_elt1) (_ : @Equal E (@subtype_elt E A (@Build_subtype E A subtype_elt1 subtype_prf0)) (@subtype_elt E A (@Build_subtype E A subtype_elt0 subtype_prf))), @Equal F (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt1 subtype_prf0))) (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt0 subtype_prf))) *)
simpl in |- *.
(* Goal: @subtype F (image A) *)
(* Goal: @in_part F (@Ap E F f x') (image A) *)
apply (Build_subtype (P:=image A) (subtype_elt:=f x') H'0).
(* Goal: forall (subtype_elt : Carrier E) (_ : @Pred_fun E A subtype_elt) (subtype_elt0 : Carrier E) (_ : @Pred_fun E A subtype_elt0) (_ : @Equal E subtype_elt0 subtype_elt), @Equal F (@Ap E F f subtype_elt0) (@Ap E F f subtype_elt) *)
auto with algebra.
Defined.

Definition surj_part_image : forall A : part_set E, MAP A (image A).
(* Goal: forall A : Carrier (part_set E), Carrier (MAP (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image F (@part F (image A)))) *)
intros A; try assumption.
(* Goal: Carrier (MAP (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image F (@part F (image A)))) *)
apply (Build_Map (Ap:=surj_part_image_fun (A:=A))).
(* Goal: forall A : Carrier (part_set E), @surjective (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image F (@part F (image A))) (surj_part_image A) *)
red in |- *.
(* Goal: forall (subtype_elt0 : Carrier E) (subtype_prf : @Pred_fun E A subtype_elt0) (subtype_elt1 : Carrier E) (subtype_prf0 : @Pred_fun E A subtype_elt1) (_ : @Equal E (@subtype_elt E A (@Build_subtype E A subtype_elt1 subtype_prf0)) (@subtype_elt E A (@Build_subtype E A subtype_elt0 subtype_prf))), @Equal F (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt1 subtype_prf0))) (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt0 subtype_prf))) *)
simpl in |- *.
(* Goal: forall (x y : @subtype E A) (_ : @subtype_image_equal E (@subtype E A) (@subtype_elt E A) x y), @subtype_image_equal F (@subtype F (image A)) (@subtype_elt F (image A)) (@surj_part_image_fun A x) (@surj_part_image_fun A y) *)
unfold subtype_image_equal in |- *.
(* Goal: forall (x y : @subtype E A) (_ : @Equal E (@subtype_elt E A x) (@subtype_elt E A y)), @Equal F (@subtype_elt F (image A) (@surj_part_image_fun A x)) (@subtype_elt F (image A) (@surj_part_image_fun A y)) *)
intros x y; try assumption.
(* Goal: forall _ : @Equal E (@subtype_elt E A x) (@subtype_elt E A y), @Equal F (@subtype_elt F (image A) (@surj_part_image_fun A x)) (@subtype_elt F (image A) (@surj_part_image_fun A y)) *)
elim x.
(* Goal: forall (subtype_elt0 : Carrier E) (subtype_prf : @Pred_fun E A subtype_elt0) (_ : @Equal E (@subtype_elt E A (@Build_subtype E A subtype_elt0 subtype_prf)) (@subtype_elt E A y)), @Equal F (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt0 subtype_prf))) (@subtype_elt F (image A) (@surj_part_image_fun A y)) *)
elim y.
(* Goal: forall (subtype_elt0 : Carrier E) (subtype_prf : @Pred_fun E A subtype_elt0) (subtype_elt1 : Carrier E) (subtype_prf0 : @Pred_fun E A subtype_elt1) (_ : @Equal E (@subtype_elt E A (@Build_subtype E A subtype_elt1 subtype_prf0)) (@subtype_elt E A (@Build_subtype E A subtype_elt0 subtype_prf))), @Equal F (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt1 subtype_prf0))) (@subtype_elt F (image A) (@surj_part_image_fun A (@Build_subtype E A subtype_elt0 subtype_prf))) *)
simpl in |- *.
(* Goal: forall (subtype_elt : Carrier E) (_ : @Pred_fun E A subtype_elt) (subtype_elt0 : Carrier E) (_ : @Pred_fun E A subtype_elt0) (_ : @Equal E subtype_elt0 subtype_elt), @Equal F (@Ap E F f subtype_elt0) (@Ap E F f subtype_elt) *)
auto with algebra.
Defined.

Lemma surj_part_image_surjective :
 forall A : part_set E, surjective (surj_part_image A).
(* Goal: forall A : Carrier (part_set E), @surjective (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image F (@part F (image A))) (surj_part_image A) *)
red in |- *.
(* Goal: forall (A : Carrier (part_set E)) (y : Carrier (@set_of_subtype_image F (@part F (image A)))), @ex (Carrier (@set_of_subtype_image E (@part E A))) (fun x : Carrier (@set_of_subtype_image E (@part E A)) => @Equal (@set_of_subtype_image F (@part F (image A))) y (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image F (@part F (image A))) (surj_part_image A) x)) *)
intros A y; try assumption.
(* Goal: @ex (Carrier (@set_of_subtype_image E (@part E A))) (fun x : Carrier (@set_of_subtype_image E (@part E A)) => @Equal (@set_of_subtype_image F (@part F (image A))) y (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image F (@part F (image A))) (surj_part_image A) x)) *)
case (image_in (subtype_prf y)).
(* Goal: forall (x : Carrier E) (_ : and (@in_part E x A) (@Equal F (@subtype_elt F (image A) y) (@Ap E F f x))), @ex (Carrier (@set_of_subtype_image E (@part E A))) (fun x0 : Carrier (@set_of_subtype_image E (@part E A)) => @Equal (@set_of_subtype_image F (@part F (image A))) y (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image F (@part F (image A))) (surj_part_image A) x0)) *)
intros x H'; try assumption.
(* Goal: @ex (Carrier (@set_of_subtype_image E (@part E A))) (fun x : Carrier (@set_of_subtype_image E (@part E A)) => @Equal (@set_of_subtype_image F (@part F (image A))) y (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image F (@part F (image A))) (surj_part_image A) x)) *)
elim H'; intros H'0 H'1; try exact H'1; clear H'.
(* Goal: @ex (Carrier (@set_of_subtype_image E (@part E A))) (fun x : Carrier (@set_of_subtype_image E (@part E A)) => @Equal (@set_of_subtype_image F (@part F (image A))) y (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image F (@part F (image A))) (surj_part_image A) x)) *)
exists (Build_subtype H'0); try assumption.
Qed.
End Images1.
Hint Resolve in_image image_included image_comp image_in_image
  surj_set_image_surjective surj_part_image_surjective: algebra.













