# Library ZFC.Sets

Inductive Ens : Type :=
sup : A : Type, (AEns) → Ens.

Inductive EXType (P : Type) (Q : PProp) : Prop :=
EXTypei : x : P, Q xEXType P Q.

Inductive prod_t (A B : Type) : Type :=
pair_t : ABprod_t A B.

Inductive depprod (A : Type) (P : AType) : Type :=
dep_i : x : A, P xdepprod A P.

Definition EQ : EnsEnsProp.
simple induction 1; intros A f eq1.
simple induction 1; intros B g eq2.
apply and.
exact ( x : A, EXType _ (fun y : Beq1 x (g y))).
exact ( y : B, EXType _ (fun x : Aeq1 x (g y))).
Defined.

Definition IN (E1 E2 : Ens) : Prop :=
match E2 with
| sup A fEXType _ (fun y : AEQ E1 (f y))
end.

Definition INC : EnsEnsProp.
intros E1 E2.
exact ( E : Ens, IN E E1IN E E2).
Defined.

Theorem EQ_refl : E : Ens, EQ E E.
simple induction E.
intros A f HR.
simpl in |- ×.
split; intros.
x; auto.

y; auto.
Qed.

Theorem EQ_tran : E1 E2 E3 : Ens, EQ E1 E2EQ E2 E3EQ E1 E3.
simple induction E1; intros A1 f1 r1; simple induction E2; intros A2 f2 r2;
simple induction E3; intros A3 f3 r3; simpl in |- *;
intros e1 e2.
split; (elim e1; intros I1 I2; elim e2; intros I3 I4).
intros a1; elim (I1 a1); intros a2.
elim (I3 a2); intros a3.
a3.
apply r1 with (f2 a2); auto.
intros a3; elim (I4 a3); intros a2; elim (I2 a2); intros a1; a1.
apply r1 with (f2 a2); auto.
Qed.

Theorem EQ_sym : E1 E2 : Ens, EQ E1 E2EQ E2 E1.
simple induction E1; intros A1 f1 r1; simple induction E2; intros A2 f2 r2;
simpl in |- *; simple induction 1; intros e1 e2; split.
intros a2; elim (e2 a2); intros a1 H1; a1; auto.
intros a1; elim (e1 a1); intros a2 H2; a2; auto.
Qed.

Theorem EQ_INC : E E' : Ens, EQ E E'INC E E'.
simple induction E; intros A f r; simple induction E'; intros A' f' r';
simpl in |- *; simple induction 1; intros e1 e2; unfold INC in |- *;
simpl in |- ×.
intros C; simple induction 1; intros a ea; elim (e1 a); intros a' ea';
a'.
apply EQ_tran with (f a); assumption.
Qed.

Hint Resolve EQ_sym EQ_refl EQ_INC: zfc.

Theorem INC_EQ : E E' : Ens, INC E E'INC E' EEQ E E'.
simple induction E; intros A f r; simple induction E'; intros A' f' r';
unfold INC in |- *; simpl in |- *; intros I1 I2; split.
intros a; apply I1.
a; auto with zfc.
intros a'; cut (EXType A (fun x : AEQ (f' a') (f x))).
simple induction 1; intros a ea; a; auto with zfc.
apply I2; a'; auto with zfc.
Qed.

Hint Resolve INC_EQ: zfc.

Theorem IN_sound_left :
E E' E'' : Ens, EQ E E'IN E E''IN E' E''.
simple induction E''; intros A'' f'' r'' e; simpl in |- *; simple induction 1;
intros a'' p; a''; apply EQ_tran with E; auto with zfc v62.
Qed.

Theorem IN_sound_right :
E E' E'' : Ens, EQ E' E''IN E E'IN E E''.
simple induction E'; intros A' f' r'; simple induction E'';
intros A'' f'' r''; simpl in |- *; simple induction 1;
intros e1 e2; simple induction 1; intros a' e'; elim (e1 a');
intros a'' e''; a''; apply EQ_tran with (f' a');
assumption.

Qed.

Theorem INC_refl : E : Ens, INC E E.
unfold INC in |- *; auto with zfc v62.
Qed.

Theorem INC_tran : E E' E'' : Ens, INC E E'INC E' E''INC E E''.
unfold INC in |- *; auto with zfc v62.
Qed.

Theorem INC_sound_left :
E E' E'' : Ens, EQ E E'INC E E''INC E' E''.
simple induction E''; unfold INC in |- *; simpl in |- *;
intros A f HR e H1 E0 i; apply H1.
apply IN_sound_right with E'; auto with zfc v62.
Qed.

Theorem INC_sound_right :
E E' E'' : Ens, EQ E' E''INC E E'INC E E''.
simple induction E'; simple induction E''; unfold INC in |- *; simpl in |- *;
intros.
elim (H2 E0); try assumption; intros.
elim H1; intros HA HB; elim (HA x); intros.
x0; apply EQ_tran with (e x); auto with zfc v62.
Qed.