Parameter Ens : Type.

Parameter IN : Ens → Ens → Prop.

Definition SUB (A B : Ens) := ∀ C : Ens, IN C A → IN C B.

Record EQ (A B : Ens) : Prop :=
  {EQ_forwards : SUB A B; EQ_backwards : SUB B A}.

Axiom excluded_middle : ∀ P : Prop, ¬ ¬ P → P.

Theorem false_implies_everything : ∀ P : Prop, False → P.
Proof False_ind.


Definition DOESNT_EXIST (P : Ens → Prop) := ∀ A : Ens, ¬ P A.

Definition EXISTS (P : Ens → Prop) := ¬ DOESNT_EXIST P.


Parameter CHOICE : ∀ P : Ens → Prop, Ens.
Axiom CHOICE_pr : ∀ (P : Ens → Prop) (h : EXISTS P), P (CHOICE P).


Parameter EmptySet : Ens.
Axiom EmptySet_pr : DOESNT_EXIST (fun X : Ens ⇒ IN X EmptySet).


Definition Bounded_By (A : Ens) (P : Ens → Prop) :=
  ∀ X : Ens, P X → IN X A.

Definition Bounded (P : Ens → Prop) :=
  EXISTS (fun A : Ens ⇒ Bounded_By A P).


Parameter union : ∀ A B : Ens, Ens.
Axiom union_pr1 : ∀ A B : Ens, SUB A (union A B).
Axiom union_pr2 : ∀ A B : Ens, SUB B (union A B).

Axiom
  union_pr3 :
    ∀ (A B C : Ens) (h : SUB A C) (k : SUB B C), SUB (union A B) C.

Record nested_IN (A B C : Ens) : Prop :=
  {nested_IN_ab : IN A B; nested_IN_bc : IN B C}.

Definition b_in_Union_a (A B : Ens) :=
  EXISTS (fun C : Ens ⇒ nested_IN B C A).

Axiom Union_bounded : ∀ F : Ens, Bounded (b_in_Union_a F).


Parameter Singleton : Ens → Ens.
Axiom Singleton_pr1 : ∀ X : Ens, IN X (Singleton X).
Axiom Singleton_pr2 : ∀ (X Y : Ens) (h : IN Y (Singleton X)), EQ X Y.


Axiom Extensionality : ∀ (X Y Z : Ens) (h : EQ X Y) (k : IN Y Z), IN X Z.


Axiom Powerset_bounded : ∀ X : Ens, Bounded (fun Y : Ens ⇒ SUB Y X).


Parameter REPLACEMENT : ∀ P : Ens → Prop, Ens.

Axiom
  REPLACEMENT_pr1 :
    ∀ (P : Ens → Prop) (b : Bounded P) (X : Ens),
    P X → IN X (REPLACEMENT P).

Axiom
  REPLACEMENT_pr2 :
    ∀ (P : Ens → Prop) (b : Bounded P) (X : Ens),
    IN X (REPLACEMENT P) → P X.


Definition Zero := EmptySet.

Definition Next (X : Ens) : Ens := union X (Singleton X).

Record Contains_NN (X : Ens) : Prop :=
  {Contains_NN_zero : IN Zero X;
   Contains_NN_nexts : ∀ (A : Ens) (h : IN A X), IN (Next A) X}.

Axiom Infinity_exists : EXISTS Contains_NN.



Section EXISTS_th1_proof.
Variable P : Ens → Prop.
Variable X : Ens.
Hypothesis p : P X.
Hypothesis h : DOESNT_EXIST P.

Let step1 : ¬ P X.
Proof h X.

Lemma EXISTS_th1_proof_Out : False.
Proof step1 p.

End EXISTS_th1_proof.

Theorem EXISTS_th1 : ∀ (P : Ens → Prop) (X : Ens) (p : P X), EXISTS P.
Proof EXISTS_th1_proof_Out.


Section subset_reflexive.
Variable A : Ens.
Variable B : Ens.
Hypothesis h : IN B A.

Lemma subset_reflexive_Out : IN B A.
Proof h.

End subset_reflexive.

Theorem SUB_refl : ∀ A : Ens, SUB A A.
Proof subset_reflexive_Out.

Section equality_reflexive.
Variable A : Ens.

Let step1_1 : SUB A A.
Proof SUB_refl A.

Lemma equality_reflexive_Out : EQ A A.
Proof Build_EQ A A step1_1 step1_1.

End equality_reflexive.

Theorem EQ_refl : ∀ A : Ens, EQ A A.
Proof equality_reflexive_Out.

Section equality_symmetric.
Variable A : Ens.
Variable B : Ens.
Hypothesis h : EQ A B.

Let stepfor : SUB A B.
Proof EQ_forwards A B h.

Let stepback : SUB B A.
Proof EQ_backwards A B h.

Lemma equality_symmetric_Out : EQ B A.
Proof Build_EQ B A stepback stepfor.

End equality_symmetric.

Theorem EQ_symm : ∀ A B : Ens, EQ A B → EQ B A.
Proof equality_symmetric_Out.


Definition NEQ (A B : Ens) := ¬ EQ A B.

Section neq_symm_proof.
Variable A : Ens.
Variable B : Ens.
Hypothesis k : NEQ A B.
Hypothesis m : EQ B A.

Let step1 : EQ A B.
Proof EQ_symm B A m.

Lemma neq_symm_Out : False.
Proof k step1.

End neq_symm_proof.

Theorem NEQ_symm : ∀ (A B : Ens) (k : NEQ A B), NEQ B A.
Proof neq_symm_Out.


Section SUB_trans_proof.
Variable A : Ens.
Variable B : Ens.
Variable C : Ens.
Hypothesis h : SUB A B.
Hypothesis k : SUB B C.

Variable X : Ens.
Hypothesis m : IN X A.

Let step1 : IN X B.
Proof h X m.

Lemma SUB_trans_proof_Out : IN X C.
Proof k X step1.

End SUB_trans_proof.

Theorem SUB_trans : ∀ (A B C : Ens) (h : SUB A B) (k : SUB B C), SUB A C.
Proof SUB_trans_proof_Out.

Section EQ_trans_proof.
Variable A : Ens.
Variable B : Ens.
Variable C : Ens.
Hypothesis h : EQ A B.
Hypothesis k : EQ B C.

Let step1 : SUB A B.
Proof EQ_forwards A B h.

Let step2 : SUB B A.
Proof EQ_backwards A B h.

Let step3 : SUB B C.
Proof EQ_forwards B C k.

Let step4 : SUB C B.
Proof EQ_backwards B C k.

Let step5 : SUB A C.
Proof SUB_trans A B C step1 step3.

Let step6 : SUB C A.
Proof SUB_trans C B A step4 step2.

Lemma EQ_trans_proof_Out : EQ A C.
Proof Build_EQ A C step5 step6.

End EQ_trans_proof.

Theorem EQ_trans : ∀ (A B C : Ens) (h : EQ A B) (k : EQ B C), EQ A C.
Proof EQ_trans_proof_Out.


Record StrictSUB (A B : Ens) : Prop :=
  {StrictSUB_sub : SUB A B; StrictSUB_neq : ¬ EQ A B}.

Section strictsub_trans1_proof.
Variable A : Ens.
Variable B : Ens.
Variable C : Ens.
Hypothesis h : StrictSUB A B.
Hypothesis k : SUB B C.

Let h1 : SUB A B.
Proof StrictSUB_sub A B h.

Let h2 : ¬ EQ A B.
Proof StrictSUB_neq A B h.

Let step1 : SUB A C.
Proof SUB_trans A B C h1 k.

Section strictsub_trans1a.
Hypothesis m : EQ A C.
Let step2 : SUB C A. Proof EQ_backwards A C m.
Let step3 : SUB B A. Proof SUB_trans B C A k step2.

Let step4 : EQ A B. Proof Build_EQ A B h1 step3.

Lemma strictsub_trans1a_Out : False.
Proof h2 step4.

End strictsub_trans1a.

Let step5 : ¬ EQ A C. Proof strictsub_trans1a_Out.

Lemma strictsub_trans1_Out : StrictSUB A C.
Proof Build_StrictSUB A C step1 step5.

End strictsub_trans1_proof.

Theorem StrictSUB_trans1 :
 ∀ (A B C : Ens) (h : StrictSUB A B) (k : SUB B C), StrictSUB A C.
Proof strictsub_trans1_Out.



Section emptyset_empty.

Variable X : Ens.
Hypothesis h : IN X EmptySet.

Lemma emptyset_empty_Out : False.
Proof EmptySet_pr X h.

End emptyset_empty.

Theorem EmptySet_th1 : ∀ (X : Ens) (h : IN X EmptySet), False.
Proof emptyset_empty_Out.

Section emptyset_subset_everything.
Variable A : Ens.
Section emptyset_subset_everything_2.
Variable B : Ens.
Hypothesis h : IN B EmptySet.
Let step1 : False. Proof EmptySet_th1 B h.
Lemma emptyset_subset_everything_2_Out : IN B A.
Proof false_implies_everything (IN B A) step1.
End emptyset_subset_everything_2.
Let step2 : ∀ (B : Ens) (h : IN B EmptySet), IN B A.
Proof emptyset_subset_everything_2_Out.
Lemma emptyset_subset_everything_Out : SUB EmptySet A.
Proof step2.
End emptyset_subset_everything.

Theorem EmptySet_th2 : ∀ A : Ens, SUB EmptySet A.
Proof emptyset_subset_everything_Out.

Definition Its_empty (A : Ens) := ∀ X : Ens, ¬ IN X A.

Section its_empty_implies_equals_emptyset_proof.
Variable A : Ens.
Hypothesis k : Its_empty A.

Section ieieep1.
Variable X : Ens.
Hypothesis i : IN X A.

Let step1_1 : False.
Proof k X i.

Lemma ieieep1_Out : IN X EmptySet.
Proof false_implies_everything (IN X EmptySet) step1_1.

End ieieep1.

Let step1 : SUB A EmptySet.
Proof ieieep1_Out.

Section ieieep2.
Variable X : Ens.
Hypothesis i : IN X EmptySet.

Let step2_1 : False.
Proof EmptySet_th1 X i.

Lemma ieieep2_Out : IN X A.
Proof false_implies_everything (IN X A) step2_1.

End ieieep2.

Let step2 : SUB EmptySet A.
Proof ieieep2_Out.

Lemma ieieep_Out : EQ A EmptySet.
Proof Build_EQ A EmptySet step1 step2.

End its_empty_implies_equals_emptyset_proof.

Theorem its_empty_implies_equals_emptyset :
 ∀ (A : Ens) (k : Its_empty A), EQ A EmptySet.
Proof ieieep_Out.

Theorem Its_empty_emptyset : Its_empty EmptySet.
Proof EmptySet_th1.

Definition Its_nonempty (A : Ens) := ¬ Its_empty A.

Section Its_nonempty_proof.
Variable X : Ens.
Variable A : Ens.
Hypothesis h : IN X A.
Hypothesis h2 : Its_empty A.
Definition Its_nonempty_proof_Out : False := h2 X h.

End Its_nonempty_proof.

Theorem Its_nonempty_th1 : ∀ (X A : Ens) (h : IN X A), Its_nonempty A.

Proof Its_nonempty_proof_Out.


Section nothing_strictsub_Zero.
Variable X : Ens.
Hypothesis h : StrictSUB X Zero.
Let step1 : SUB X Zero.
Proof StrictSUB_sub X Zero h.
Let step2 : Its_empty X.
Proof fun (Y : Ens) (m : IN Y X) ⇒ EmptySet_th1 Y (step1 Y m).

Let step3 : EQ X Zero.
Proof its_empty_implies_equals_emptyset X step2.

Definition nothing_strictsub_Zero_Out : False := StrictSUB_neq X Zero h step3.

End nothing_strictsub_Zero.

Theorem Nothing_strictsub_Zero : ∀ X : Ens, ¬ StrictSUB X Zero.
Proof nothing_strictsub_Zero_Out.


Section Bounded_th1_proof.
Variable P : Ens → Prop.
Variable A : Ens.
Hypothesis h : ∀ X : Ens, P X → IN X A.
Let step1 : Bounded_By A P. Proof h.
Definition Bounded_th1_proof_Out : EXISTS (fun A : Ens ⇒ Bounded_By A P) :=
  EXISTS_th1 (fun B : Ens ⇒ Bounded_By B P) A step1.

End Bounded_th1_proof.

Theorem Bounded_th1 :
 ∀ (P : Ens → Prop) (A : Ens) (h : ∀ X : Ens, P X → IN X A),
 Bounded P.
Proof Bounded_th1_proof_Out.

Theorem Bounded_th2 :
 ∀ (P : Ens → Prop) (A : Ens) (h : Bounded_By A P), Bounded P.
Proof
  fun (P : Ens → Prop) (A : Ens) (h : Bounded_By A P) ⇒ Bounded_th1 P A h.

Definition Bounded_CHOICE (P : Ens → Prop) := REPLACEMENT P.

Theorem Bounded_CHOICE_pr :
 ∀ (P : Ens → Prop) (b : Bounded P), Bounded_By (Bounded_CHOICE P) P.
Proof fun (P : Ens → Prop) (b : Bounded P) ⇒ REPLACEMENT_pr1 P b.

Definition SUBPROP (P Q : Ens → Prop) := ∀ X : Ens, P X → Q X.

Section Bounded_subprops1.
Variable P : Ens → Prop.
Variable Q : Ens → Prop.
Hypothesis s : SUBPROP P Q.
Variable A : Ens.
Hypothesis h : Bounded_By A Q.

Section boundedsubprops1.
Variable X : Ens.
Hypothesis k : P X.
Let step1 : Q X. Proof s X k.
Definition boundedsubprops1_Out : IN X A := h X step1.
End boundedsubprops1.
Definition Bounded_subprops1_Out : Bounded_By A P := boundedsubprops1_Out.

End Bounded_subprops1.

Theorem Bounded_subprops_th1 :
 ∀ (P Q : Ens → Prop) (s : SUBPROP P Q) (A : Ens) (h : Bounded_By A Q),
 Bounded_By A P.
Proof Bounded_subprops1_Out.

Section Bounded_subprops2.
Variable P : Ens → Prop.
Variable Q : Ens → Prop.
Hypothesis s : SUBPROP P Q.
Hypothesis b : Bounded Q.

Let A : Ens := Bounded_CHOICE Q.
Let h : Bounded_By A Q. Proof Bounded_CHOICE_pr Q b.

Let step1 : Bounded_By A P.
Proof Bounded_subprops_th1 P Q s A h.
Lemma Bounded_sub2_Out : Bounded P.
Proof Bounded_th2 P A step1.

End Bounded_subprops2.

Theorem Bounded_subprops_th2 :
 ∀ (P Q : Ens → Prop) (s : SUBPROP P Q) (b : Bounded Q), Bounded P.
Proof Bounded_sub2_Out.


Record Restriction (P : Ens → Prop) (A X : Ens) : Prop :=
  {remaining_property : P X; the_restriction : IN X A}.

Section restriction_bounded_proof.
Variable P : Ens → Prop.
Variable A : Ens.

Let R := Restriction P A.

Let t : Bounded_By A R. Proof fun (X : Ens) (h : R X) ⇒ the_restriction P A X h.

Definition restriction_bounded_Out : Bounded R :=
  EXISTS_th1 (fun Y : Ens ⇒ Bounded_By Y R) A t.

End restriction_bounded_proof.

Theorem Restriction_bounded :
 ∀ (P : Ens → Prop) (A : Ens), Bounded (Restriction P A).
Proof restriction_bounded_Out.

Definition Set_Of (A : Ens) (P : Ens → Prop) :=
  REPLACEMENT (Restriction P A).

Theorem Set_Of_pr1 :
 ∀ (A : Ens) (P : Ens → Prop) (X : Ens),
 Restriction P A X → IN X (Set_Of A P).
Proof
  fun (A : Ens) (P : Ens → Prop) ⇒
  REPLACEMENT_pr1 (Restriction P A) (Restriction_bounded P A).

Theorem Set_Of_pr2 :
 ∀ (A : Ens) (P : Ens → Prop) (X : Ens),
 IN X (Set_Of A P) → Restriction P A X.
Proof
  fun (A : Ens) (P : Ens → Prop) ⇒
  REPLACEMENT_pr2 (Restriction P A) (Restriction_bounded P A).

Theorem Set_Of_th1 :
 ∀ (A : Ens) (P : Ens → Prop) (X : Ens) (h : IN X A) (k : P X),
 IN X (Set_Of A P).
Proof
  fun (A : Ens) (P : Ens → Prop) (X : Ens) (h : IN X A) (k : P X) ⇒
  Set_Of_pr1 A P X (Build_Restriction P A X k h).

Theorem Set_Of_th2 :
 ∀ (A : Ens) (P : Ens → Prop) (X : Ens) (h : IN X (Set_Of A P)), P X.
Proof
  fun (A : Ens) (P : Ens → Prop) (X : Ens) (h : IN X (Set_Of A P)) ⇒
  remaining_property P A X (Set_Of_pr2 A P X h).

Theorem Set_Of_th3 :
 ∀ (A : Ens) (P : Ens → Prop) (X : Ens) (h : IN X (Set_Of A P)), IN X A.
Proof
  fun (A : Ens) (P : Ens → Prop) (X : Ens) (h : IN X (Set_Of A P)) ⇒
  the_restriction P A X (Set_Of_pr2 A P X h).

Theorem Set_Of_th4 : ∀ (A : Ens) (P : Ens → Prop), SUB (Set_Of A P) A.
Proof Set_Of_th3.



Definition intersection (A B : Ens) := Set_Of A (fun X : Ens ⇒ IN X B).

Theorem intersection_th1 : ∀ A B : Ens, SUB (intersection A B) A.
Proof
  fun (A B U : Ens) (i : IN U (intersection A B)) ⇒
  Set_Of_th3 A (fun X : Ens ⇒ IN X B) U i.

Theorem intersection_th2 : ∀ A B : Ens, SUB (intersection A B) B.
Proof
  fun (A B U : Ens) (i : IN U (intersection A B)) ⇒
  Set_Of_th2 A (fun X : Ens ⇒ IN X B) U i.

Theorem intersection_th3 :
 ∀ (A B X : Ens) (i : IN X A) (j : IN X B), IN X (intersection A B).
Proof
  fun (A B X : Ens) (i : IN X A) (j : IN X B) ⇒
  Set_Of_th1 A (fun U : Ens ⇒ IN U B) X i j.

Section intersection4.
Variable A B C : Ens.
Hypothesis s : SUB C A.
Hypothesis t : SUB C B.

Variable X : Ens.
Hypothesis i : IN X C.
Let step1 : IN X A.
Proof s X i.
Let step2 : IN X B.
Proof t X i.

Lemma intersection4_Out : IN X (intersection A B).
Proof intersection_th3 A B X step1 step2.

End intersection4.

Theorem intersection_th4 :
 ∀ (A B C : Ens) (s : SUB C A) (t : SUB C B), SUB C (intersection A B).
Proof intersection4_Out.


Definition IntersectionProp (F : Ens → Ens) (X : Ens) :=
  ∀ Y : Ens, IN X (F Y).

Section Intersection_section1.
Variable F : Ens → Ens.

Let A := F EmptySet.

Section Intersection_section1_1.
Variable Z : Ens.
Hypothesis h : IntersectionProp F Z.

Definition Intersection_section1_1_Out : IN Z A := h EmptySet.

End Intersection_section1_1.

Let step1 : ∀ (Z : Ens) (h : IntersectionProp F Z), IN Z A.
Proof Intersection_section1_1_Out.

Let step2 : Bounded_By A (IntersectionProp F).
Proof step1.

Definition Intersection_section1_Out : Bounded (IntersectionProp F) :=
  Bounded_th2 (IntersectionProp F) A step2.

End Intersection_section1.

Definition Intersection_Bounded :
  ∀ F : Ens → Ens, Bounded (IntersectionProp F) :=
  Intersection_section1_Out.

Definition Intersection (F : Ens → Ens) : Ens :=
  REPLACEMENT (IntersectionProp F).

Theorem Intersection_pr1 :
 ∀ (F : Ens → Ens) (X : Ens),
 IntersectionProp F X → IN X (Intersection F).
Proof
  fun F : Ens → Ens ⇒
  REPLACEMENT_pr1 (IntersectionProp F) (Intersection_Bounded F).

Theorem Intersection_pr2 :
 ∀ (F : Ens → Ens) (X : Ens),
 IN X (Intersection F) → IntersectionProp F X.
Proof
  fun F : Ens → Ens ⇒
  REPLACEMENT_pr2 (IntersectionProp F) (Intersection_Bounded F).

Theorem Intersection_th1 :
 ∀ (F : Ens → Ens) (X : Ens) (h : ∀ Y : Ens, IN X (F Y)),
 IN X (Intersection F).
Proof Intersection_pr1.

Theorem Intersection_th2 :
 ∀ (F : Ens → Ens) (X Y : Ens) (i : IN X (Intersection F)), IN X (F Y).
Proof
  fun (F : Ens → Ens) (X Y : Ens) (i : IN X (Intersection F)) ⇒
  Intersection_pr2 F X i Y.


Section Singleton_th1_proof.
Variable X : Ens.
Variable A : Ens.
Hypothesis h : IN X A.

Let B := Singleton X.

Section Singleton_th1_sub1.
Variable C : Ens.
Hypothesis h2 : IN C B.

Let step1 : EQ X C.
Proof Singleton_pr2 X C h2.

Let step2 : EQ C X.
Proof EQ_symm X C step1.

Definition Singleton_th1_sub1_Out : IN C A := Extensionality C X A step2 h.

End Singleton_th1_sub1.

Definition Singleton_th1_proof_Out : SUB B A := Singleton_th1_sub1_Out.

End Singleton_th1_proof.

Theorem Singleton_th1 : ∀ (X A : Ens) (h : IN X A), SUB (Singleton X) A.
Proof Singleton_th1_sub1_Out.

Section Singleton_th2_proof.
Variable X : Ens.
Let B := Singleton X.
Let step1 : IN X B. Proof Singleton_pr1 X.

Hypothesis h : Its_empty B.

Let step2 : IN X B → False.
Proof h X.

Definition Singleton_th2_proof_Out : False := step2 step1.

End Singleton_th2_proof.

Theorem Singleton_th2 : ∀ X : Ens, Its_nonempty (Singleton X).
Proof Singleton_th2_proof_Out.



Section union_th1_proof.
Variable A : Ens.
Variable B : Ens.
Let U := union A B.
Variable X : Ens.
Hypothesis h : IN X A.

Let step1 : SUB A U.
Proof union_pr1 A B.
Definition union_th1_Out : IN X U := step1 X h.

End union_th1_proof.

Theorem union_th1 : ∀ (A B X : Ens) (h : IN X A), IN X (union A B).
Proof union_th1_Out.

Section union_th2_proof.
Variable A : Ens.
Variable B : Ens.
Let U := union A B.
Variable X : Ens.
Hypothesis h : IN X B.

Let step1 : SUB B U.
Proof union_pr2 A B.
Definition union_th2_Out : IN X U := step1 X h.

End union_th2_proof.

Theorem union_th2 : ∀ (A B X : Ens) (h : IN X B), IN X (union A B).
Proof union_th2_Out.

Section union_th3_proof.
Variable A : Ens.
Variable B : Ens.
Let U := union A B.
Variable X : Ens.
Hypothesis h : ¬ IN X A.
Hypothesis k : ¬ IN X B.
Hypothesis m : IN X U.

Record union_th3_property (Y : Ens) : Prop :=
  {union_th3_property_in_the_union : IN Y U;
   union_th3_property_not_equal_X : ¬ EQ X Y}.

Let step1 : Bounded_By U union_th3_property.
Proof
  fun (Y : Ens) (h : union_th3_property Y) ⇒
  union_th3_property_in_the_union Y h.

Let b : Bounded union_th3_property.
Proof Bounded_th2 union_th3_property U step1.

Let V := REPLACEMENT union_th3_property.

Let V_pr1 : ∀ X : Ens, union_th3_property X → IN X V.
Proof REPLACEMENT_pr1 union_th3_property b.

Let V_pr2 : ∀ X : Ens, IN X V → union_th3_property X.
Proof REPLACEMENT_pr2 union_th3_property b.

Section A_sub_V_proof.
Variable Z : Ens.
Hypothesis h2 : IN Z A.

Section A_sub_V_proof1.
Hypothesis h3 : EQ X Z.

Let step1_1 : IN X A.
Proof Extensionality X Z A h3 h2.

Definition A_sub_V_proof1_Out : False := h step1_1.

End A_sub_V_proof1.

Let step2 : ¬ EQ X Z.
Proof A_sub_V_proof1_Out.

Let step3 : IN Z U.
Proof union_th1 A B Z h2.

Let step4 : union_th3_property Z.
Proof Build_union_th3_property Z step3 step2.

Lemma A_sub_V_proof_Out : IN Z V.
Proof V_pr1 Z step4.

End A_sub_V_proof.

Let A_sub_V : SUB A V. Proof A_sub_V_proof_Out.

Section B_sub_V_proof.
Variable Z : Ens.
Hypothesis h2 : IN Z B.

Section B_sub_V_proof1.
Hypothesis h3 : EQ X Z.

Let step1_1 : IN X B.
Proof Extensionality X Z B h3 h2.

Lemma B_sub_V_proof1_Out : False.
Proof k step1_1.

End B_sub_V_proof1.

Let step2 : ¬ EQ X Z. Proof B_sub_V_proof1_Out.

Let step3 : IN Z U.
Proof union_th2 A B Z h2.

Let step4 : union_th3_property Z.
Proof Build_union_th3_property Z step3 step2.

Definition B_sub_V_proof_Out : IN Z V := V_pr1 Z step4.

End B_sub_V_proof.

Let B_sub_V : SUB B V. Proof B_sub_V_proof_Out.

Let U_sub_V : SUB U V.
Proof union_pr3 A B V A_sub_V B_sub_V.

Let X_in_V : IN X V.
Proof U_sub_V X m.

Let step5 : union_th3_property X.
Proof V_pr2 X X_in_V.

Let step6 : ¬ EQ X X.
Proof union_th3_property_not_equal_X X step5.

Let step7 : EQ X X. Proof EQ_refl X.

Lemma union_th3_proof_Out : False.
Proof step6 step7.

End union_th3_proof.

Theorem union_th3 :
 ∀ (A B X : Ens) (h : ¬ IN X A) (k : ¬ IN X B), ¬ IN X (union A B).
Proof union_th3_proof_Out.

Section union_th4_proof.
Variable P : Prop.
Variable A B X : Ens.
Hypothesis i : IN X (union A B).
Hypothesis a : IN X A → P.
Hypothesis b : IN X B → P.

Section ut4contra.
Hypothesis contra : ¬ P.

Section ut4a.
Hypothesis j : IN X A.
Let step1 : P.
Proof a j.
Lemma step2 : False.
Proof contra step1.
End ut4a.
Let step3 : ¬ IN X A.
Proof step2.

Section ut4b.
Hypothesis k : IN X B.
Let step4 : P.
Proof b k.
Lemma step5 : False.
Proof contra step4.
End ut4b.
Let step6 : ¬ IN X B.
Proof step5.

Let step7 : ¬ IN X (union A B).
Proof union_th3 A B X step3 step6.
Lemma step8 : False.
Proof step7 i.

End ut4contra.

Lemma union_th4_Out : P.
Proof excluded_middle P step8.

End union_th4_proof.

Theorem union_th4 :
 ∀ (P : Prop) (A B X : Ens) (i : IN X (union A B))
   (a : IN X A → P) (b : IN X B → P), P.
Proof union_th4_Out.

Section union_refl_proof.
Variable A : Ens.

Let U := union A A.

Let step1 : SUB A U.
Proof union_pr1 A A.
Let step2 : SUB A A. Proof SUB_refl A.
Let step3 : SUB U A. Proof union_pr3 A A A step2 step2.

Lemma union_refl_proof_Out : EQ A U.
Proof Build_EQ A U step1 step3.

End union_refl_proof.

Theorem union_refl : ∀ A : Ens, EQ A (union A A).
Proof union_refl_proof_Out.

Section union_symm_proof.
Variable A : Ens.
Variable B : Ens.
Let U := union A B.
Let V := union B A.

Let step1 : SUB A U.
Proof union_pr1 A B.
Let step2 : SUB B U.
Proof union_pr2 A B.

Let step3 : SUB B V.
Proof union_pr1 B A.
Let step4 : SUB A V.
Proof union_pr2 B A.

Let step5 : SUB U V.
Proof union_pr3 A B V step4 step3.
Let step6 : SUB V U.
Proof union_pr3 B A U step2 step1.

Lemma union_symm_proof_Out : EQ U V.
Proof Build_EQ U V step5 step6.

End union_symm_proof.

Theorem union_symm : ∀ A B : Ens, EQ (union A B) (union B A).
Proof union_symm_proof_Out.


Definition Union (F : Ens) : Ens := REPLACEMENT (b_in_Union_a F).

Theorem Union_pr1 :
 ∀ (F X : Ens) (h : EXISTS (fun U : Ens ⇒ nested_IN X U F)),
 IN X (Union F).
Proof
  fun (F X : Ens) (h : EXISTS (fun U : Ens ⇒ nested_IN X U F)) ⇒
  REPLACEMENT_pr1 (b_in_Union_a F) (Union_bounded F) X h.

Theorem Union_pr2 :
 ∀ (F X : Ens) (i : IN X (Union F)),
 EXISTS (fun U : Ens ⇒ nested_IN X U F).
Proof fun F : Ens ⇒ REPLACEMENT_pr2 (b_in_Union_a F) (Union_bounded F).

Definition Union_intermediate (F X : Ens) (i : IN X (Union F)) : Ens :=
  CHOICE (fun U : Ens ⇒ nested_IN X U F).

Theorem Union_intermediate_pr :
 ∀ (F X : Ens) (i : IN X (Union F)),
 nested_IN X (Union_intermediate F X i) F.
Proof
  fun (F X : Ens) (i : IN X (Union F)) ⇒
  CHOICE_pr (fun U : Ens ⇒ nested_IN X U F) (Union_pr2 F X i).

Theorem Union_intermediate_th1 :
 ∀ (F X : Ens) (i : IN X (Union F)), IN X (Union_intermediate F X i).
Proof
  fun (F X : Ens) (i : IN X (Union F)) ⇒
  nested_IN_ab X (Union_intermediate F X i) F (Union_intermediate_pr F X i).

Theorem Union_intermediate_th2 :
 ∀ (F X : Ens) (i : IN X (Union F)), IN (Union_intermediate F X i) F.
Proof
  fun (F X : Ens) (i : IN X (Union F)) ⇒
  nested_IN_bc X (Union_intermediate F X i) F (Union_intermediate_pr F X i).

Section Union_th1_proof.
Variable F : Ens.
Variable X : Ens.
Variable U : Ens.
Hypothesis h : IN X U.
Hypothesis k : IN U F.

Let step1 : nested_IN X U F.
Proof Build_nested_IN X U F h k.

Let step2 : EXISTS (fun U1 : Ens ⇒ nested_IN X U1 F).
Proof EXISTS_th1 (fun U1 : Ens ⇒ nested_IN X U1 F) U step1.

Lemma union_th1_OutA : IN X (Union F).
Proof Union_pr1 F X step2.

End Union_th1_proof.

Theorem Union_th1 :
 ∀ (F X U : Ens) (h : IN X U) (k : IN U F), IN X (Union F).
Proof union_th1_OutA.


Definition has_leq_0_elements := Its_empty.

Theorem zero_has_leq_0_elements : has_leq_0_elements Zero.
Proof EmptySet_th1.

Definition has_geq_1_elements (A : Ens) := ¬ has_leq_0_elements A.


Definition Choose_an_element (A : Ens) (k : has_geq_1_elements A) : Ens :=
  CHOICE (fun X : Ens ⇒ IN X A).

Theorem Choose_an_element_pr :
 ∀ (A : Ens) (k : has_geq_1_elements A), IN (Choose_an_element A k) A.
Proof
  fun (A : Ens) (k : has_geq_1_elements A) ⇒
  CHOICE_pr (fun X : Ens ⇒ IN X A) k.

Section given_an_element.
Variable A : Ens.
Variable X : Ens.
Variable k : IN X A.
Hypothesis m : has_leq_0_elements A.

Definition given_an_element_Out : False := m X k.

End given_an_element.

Theorem has_geq_1_elements_th1 :
 ∀ (A X : Ens) (k : IN X A), has_geq_1_elements A.
Proof given_an_element_Out.


Theorem Singletons_have_geq_1_elements :
 ∀ X : Ens, has_geq_1_elements (Singleton X).
Proof Singleton_th2.

Definition has_leq_1_elements (A : Ens) :=
  ∀ (X Y : Ens) (k : IN X A) (l : IN Y A), EQ X Y.

Section has_leq_0_implies_leq_1.
Variable A : Ens.
Hypothesis q : has_leq_0_elements A.
Variable X : Ens.
Variable Y : Ens.
Hypothesis k : IN X A.

Let step1 : False.
Proof q X k.

Let step2 : EQ X Y := false_implies_everything (EQ X Y) step1.

Definition has_leq_0_implies_leq_1_Out (l : IN Y A) : EQ X Y := step2.


End has_leq_0_implies_leq_1.

Theorem has_leq_0_elements_implies_leq_1 :
 ∀ (A : Ens) (q : has_leq_0_elements A), has_leq_1_elements A.
Proof has_leq_0_implies_leq_1_Out.

Section singletons_have_leq_1_elements_proof.
Variable A : Ens.

Let S := Singleton A.

Variable X : Ens.
Variable Y : Ens.

Hypothesis iXS : IN X S.
Hypothesis iYS : IN Y S.

Let step1 : EQ A X := Singleton_pr2 A X iXS.

Let step2 : EQ A Y := Singleton_pr2 A Y iYS.

Let step3 : EQ X A := EQ_symm A X step1.

Definition singletons_have_leq_1_elements_Out : EQ X Y :=
  EQ_trans X A Y step3 step2.

End singletons_have_leq_1_elements_proof.

Theorem Singletons_have_leq_1_elements :
 ∀ A : Ens, has_leq_1_elements (Singleton A).
Proof singletons_have_leq_1_elements_Out.

Definition has_geq_2_elements (A : Ens) := ¬ has_leq_1_elements A.

Section when_given_two_distinct_elements.
Variable A : Ens.
Variable X : Ens.
Variable Y : Ens.
Hypothesis k : IN X A.
Hypothesis l : IN Y A.
Hypothesis m : ¬ EQ X Y.

Hypothesis h : has_leq_1_elements A.

Definition when_given_two_distinct_elements_Out : False := m (h X Y k l).

End when_given_two_distinct_elements.

Theorem has_geq_2_elements_th1 :
 ∀ (A X Y : Ens) (k : IN X A) (l : IN Y A) (m : ¬ EQ X Y),
 has_geq_2_elements A.
Proof when_given_two_distinct_elements_Out.


Definition Doubleton (X Y : Ens) := union (Singleton X) (Singleton Y).

Section doubleton_th1_proof.
Variable X : Ens.
Variable Y : Ens.

Let D := Doubleton X Y.

Let iXsX : IN X (Singleton X) := Singleton_pr1 X.

Definition doubleton_th1_Out : IN X D :=
  union_th1 (Singleton X) (Singleton Y) X iXsX.

End doubleton_th1_proof.

Theorem Doubleton_th1 : ∀ X Y : Ens, IN X (Doubleton X Y).
Proof doubleton_th1_Out.

Section doubleton_th2_proof.
Variable X : Ens.
Variable Y : Ens.

Let D := Doubleton X Y.

Let iYsY : IN Y (Singleton Y) := Singleton_pr1 Y.

Definition doubleton_th2_Out : IN Y D :=
  union_th2 (Singleton X) (Singleton Y) Y iYsY.

End doubleton_th2_proof.

Theorem Doubleton_th2 : ∀ X Y : Ens, IN Y (Doubleton X Y).
Proof doubleton_th2_Out.

Section doubleton_th3_proof.
Variable X : Ens.
Variable Y : Ens.
Variable A : Ens.
Hypothesis iXA : IN X A.
Hypothesis iYA : IN Y A.

Let D := Doubleton X Y.

Let sXsubA : SUB (Singleton X) A := Singleton_th1 X A iXA.

Let sYsubA : SUB (Singleton Y) A := Singleton_th1 Y A iYA.

Definition doubleton_th3_Out : SUB D A :=
  union_pr3 (Singleton X) (Singleton Y) A sXsubA sYsubA.

End doubleton_th3_proof.

Theorem Doubleton_th3 :
 ∀ (X Y A : Ens) (iXA : IN X A) (iYA : IN Y A), SUB (Doubleton X Y) A.
Proof doubleton_th3_Out.

Section doubleton_th4_proof.
Variable X : Ens.
Variable Y : Ens.
Variable Z : Ens.
Hypothesis k : IN Z (Doubleton X Y).
Hypothesis m : ¬ EQ Z X.
Hypothesis n : ¬ EQ Z Y.

Let D := Doubleton X Y.

Let sX := Singleton X.
Let sY := Singleton Y.

Section doubleton_th4_sub1.
Hypothesis u : IN Z sX.

Let step1_1 : EQ X Z := Singleton_pr2 X Z u.

Let step1_2 : EQ Z X := EQ_symm X Z step1_1.

Definition doubleton_th4_sub1_Out : False := m step1_2.

End doubleton_th4_sub1.

Let step1 : ¬ IN Z sX := doubleton_th4_sub1_Out.

Section doubleton_th4_sub2.
Hypothesis u : IN Z sY.

Let step2_1 : EQ Y Z := Singleton_pr2 Y Z u.

Let step2_2 : EQ Z Y := EQ_symm Y Z step2_1.

Definition doubleton_th4_sub2_Out : False := n step2_2.

End doubleton_th4_sub2.

Let step2 : ¬ IN Z sY := doubleton_th4_sub2_Out.

Let step3 : ¬ IN Z D := union_th3 sX sY Z step1 step2.

Definition doubleton_th4_Out : False := step3 k.

End doubleton_th4_proof.

Theorem Doubleton_th4 :
 ∀ (X Y Z : Ens) (k : IN Z (Doubleton X Y)) (m : ¬ EQ Z X)
   (n : ¬ EQ Z Y), False.
Proof doubleton_th4_Out.

Section doubleton_th4a_proof.
Variable X : Ens.
Variable Y : Ens.
Variable Z : Ens.
Hypothesis k : IN Z (Doubleton X Y).
Hypothesis m : ¬ EQ Z X.

Let step1 : ¬ ¬ EQ Z Y := Doubleton_th4 X Y Z k m.

Definition doubleton_th4a_Out : EQ Z Y := excluded_middle (EQ Z Y) step1.

End doubleton_th4a_proof.

Theorem Doubleton_th4_a :
 ∀ (X Y Z : Ens) (k : IN Z (Doubleton X Y)) (m : ¬ EQ Z X), EQ Z Y.
Proof doubleton_th4a_Out.

Section doubleton_th4b_proof.
Variable X : Ens.
Variable Y : Ens.
Variable Z : Ens.
Hypothesis k : IN Z (Doubleton X Y).
Hypothesis n : ¬ EQ Z Y.

Let step1 : ¬ ¬ EQ Z X := fun m : ¬ EQ Z X ⇒ Doubleton_th4 X Y Z k m n.

Definition doubleton_th4b_Out : EQ Z X := excluded_middle (EQ Z X) step1.

End doubleton_th4b_proof.

Theorem Doubleton_th4_b :
 ∀ (X Y Z : Ens) (k : IN Z (Doubleton X Y)) (n : ¬ EQ Z Y), EQ Z X.
Proof doubleton_th4b_Out.

Section distinct_doubletons_have_geq_2_elements_proof.
Variable X : Ens.
Variable Y : Ens.
Hypothesis n : ¬ EQ X Y.

Let D := Doubleton X Y.
Hypothesis h : has_leq_1_elements D.

Let iXD : IN X D := Doubleton_th1 X Y.

Let iYD : IN Y D := Doubleton_th2 X Y.

Let step1 : EQ X Y := h X Y iXD iYD.

Definition distinct_doubletons_have_geq_2_elements_Out : False := n step1.

End distinct_doubletons_have_geq_2_elements_proof.

Theorem distinct_Doubletons_have_geq_2_elements :
 ∀ (X Y : Ens) (n : ¬ EQ X Y), has_geq_2_elements (Doubleton X Y).
Proof distinct_doubletons_have_geq_2_elements_Out.


Section big_extensionality_proof.

Variable P : Ens → Prop.
Variable X : Ens.
Variable Y : Ens.
Hypothesis m : P X.
Hypothesis k : EQ X Y.

Let D := Doubleton X Y.

Let iXD : IN X D := Doubleton_th1 X Y.
Let iYD : IN Y D := Doubleton_th2 X Y.

Let eYX : EQ Y X := EQ_symm X Y k.

Let S := Set_Of D P.

Let iXS : IN X S := Set_Of_th1 D P X iXD m.

Let iYS : IN Y S := Extensionality Y X S eYX iXS.

Definition big_extensionality_Out : P Y := Set_Of_th2 D P Y iYS.

End big_extensionality_proof.

Theorem Big_Extensionality :
 ∀ (P : Ens → Prop) (X Y : Ens) (p : P X) (e : EQ X Y), P Y.
Proof big_extensionality_Out.


Theorem Substitute :
 ∀ (X Y : Ens) (P : Ens → Prop) (e : EQ X Y) (p : P Y), P X.
Proof
  fun (X Y : Ens) (P : Ens → Prop) (e : EQ X Y) (p : P Y) ⇒
  Big_Extensionality P Y X p (EQ_symm X Y e).


Section zero_different_from_one.
Variable X : Ens.
Variable Y : Ens.
Hypothesis m : has_leq_0_elements X.
Hypothesis n : has_geq_1_elements Y.

Hypothesis h : EQ X Y.

Let step1 : has_leq_0_elements Y :=
  Big_Extensionality has_leq_0_elements X Y m h.

Definition zero_different_from_one_Out : False := n step1.

End zero_different_from_one.

Theorem counting_lem1 :
 ∀ (X Y : Ens) (m : has_leq_0_elements X) (n : has_geq_1_elements Y),
 ¬ EQ X Y.
Proof zero_different_from_one_Out.

Section one_different_from_two.
Variable X : Ens.
Variable Y : Ens.
Hypothesis m : has_leq_1_elements X.
Hypothesis n : has_geq_2_elements Y.

Hypothesis h : EQ X Y.

Let step1 : has_leq_1_elements Y :=
  Big_Extensionality has_leq_1_elements X Y m h.

Definition one_different_from_two_Out : False := n step1.

End one_different_from_two.

Theorem counting_lem2 :
 ∀ (X Y : Ens) (m : has_leq_1_elements X) (n : has_geq_2_elements Y),
 ¬ EQ X Y.
Proof one_different_from_two_Out.


Definition First (X : Ens) : Ens := Singleton X.
Definition Second (X : Ens) : Ens := Doubleton Zero (Singleton X).

Definition PAIR (X Y : Ens) : Ens := Doubleton (First X) (Second Y).

Section first_uniqueness.
Variable A : Ens.
Variable B : Ens.
Hypothesis m : EQ (First A) (First B).

Let F := First A.
Let G := First B.

Let FsubG : SUB F G := EQ_forwards F G m.

Let iAF : IN A F := Singleton_pr1 A.

Let iBF : IN A G := FsubG A iAF.

Let step1 : EQ B A := Singleton_pr2 B A iBF.

Definition first_uniqueness_Out : EQ A B := EQ_symm B A step1.

End first_uniqueness.

Theorem First_uniqueness :
 ∀ (A B : Ens) (m : EQ (First A) (First B)), EQ A B.
Proof first_uniqueness_Out.

Theorem Singleton_uniqueness :
 ∀ (A B : Ens) (m : EQ (Singleton A) (Singleton B)), EQ A B.
Proof First_uniqueness.

Record pairwise_EQ (A B C D : Ens) : Prop :=
  {pairwise_EQ_ac : EQ A C; pairwise_EQ_bd : EQ B D}.

Section doubleton_uniqueness_proof.

Variable P : Ens → Prop.

Variable A : Ens.
Variable B : Ens.
Variable C : Ens.
Variable D : Ens.

Hypothesis pA : P A.
Hypothesis nB : ¬ P B.

Hypothesis pC : P C.
Hypothesis nD : ¬ P D.

Hypothesis e : EQ (Doubleton A B) (Doubleton C D).

Let Doub := Doubleton C D.

Let iA : IN A (Doubleton A B) := Doubleton_th1 A B.

Let iB : IN B (Doubleton A B) := Doubleton_th2 A B.

Let step1 : SUB (Doubleton A B) Doub := EQ_forwards (Doubleton A B) Doub e.

Let iAdoub : IN A Doub := step1 A iA.

Let iBdoub : IN B Doub := step1 B iB.

Section doubleton_uniqueness_1.
Hypothesis k : EQ A D.


Let step1_2 : P D := Big_Extensionality P A D pA k.

Definition doubleton_uniqueness_1_Out : False := nD step1_2.

End doubleton_uniqueness_1.

Let step2 : NEQ A D := doubleton_uniqueness_1_Out.

Section doubleton_uniqueness_2.
Hypothesis k : EQ B C.

Let step1_1 : EQ C B := EQ_symm B C k.


Let step1_2 : P B := Big_Extensionality P C B pC step1_1.

Definition doubleton_uniqueness_2_Out : False := nB step1_2.

End doubleton_uniqueness_2.

Let step3 : NEQ B C := doubleton_uniqueness_2_Out.


Let conclusionAC : EQ A C := Doubleton_th4_b C D A iAdoub step2.

Let conclusionBD : EQ B D := Doubleton_th4_a C D B iBdoub step3.

Definition doubleton_uniqueness_Out : pairwise_EQ A B C D :=
  Build_pairwise_EQ A B C D conclusionAC conclusionBD.

End doubleton_uniqueness_proof.

Theorem Doubleton_uniqueness :
 ∀ (P : Ens → Prop) (A B C D : Ens) (pA : P A)
   (nB : ¬ P B) (pC : P C) (nD : ¬ P D)
   (e : EQ (Doubleton A B) (Doubleton C D)), pairwise_EQ A B C D.
Proof doubleton_uniqueness_Out.

Section second_has_geq_2_elements_proof.

Variable A : Ens.
Hypothesis k : has_leq_1_elements A.

Let sA := Singleton A.
Let E := Second A.


Let step1 : has_geq_1_elements sA := Singletons_have_geq_1_elements A.

Section second_geq_2_a.
Hypothesis m : EQ Zero sA.

Let stepa_1 : has_leq_0_elements sA :=
  Big_Extensionality has_leq_0_elements Zero sA zero_has_leq_0_elements m.

Definition second_geq_2_a_Out : False := step1 stepa_1.

End second_geq_2_a.

Let step2 : NEQ Zero sA := second_geq_2_a_Out.

Definition second_has_geq_2_elements_Out : has_geq_2_elements E :=
  distinct_Doubletons_have_geq_2_elements Zero sA step2.

End second_has_geq_2_elements_proof.

Theorem Second_has_geq_2_elements :
 ∀ A : Ens, has_geq_2_elements (Second A).
Proof second_has_geq_2_elements_Out.

Section second_uniqueness_proof.

Variable A : Ens.
Variable B : Ens.
Hypothesis k : EQ (Second A) (Second B).


Let sA := Singleton A.
Let sB := Singleton B.

Let step1 : has_geq_1_elements sA := Singletons_have_geq_1_elements A.

Let step2 : has_geq_1_elements sB := Singletons_have_geq_1_elements B.

Let step3 : pairwise_EQ Zero sA Zero sB :=
  Doubleton_uniqueness has_leq_0_elements Zero sA Zero sB
    zero_has_leq_0_elements step1 zero_has_leq_0_elements step2 k.

Definition second_uniqueness_Out : EQ A B :=
  Singleton_uniqueness A B (pairwise_EQ_bd Zero sA Zero sB step3).

End second_uniqueness_proof.

Theorem Second_uniqueness :
 ∀ (A B : Ens) (k : EQ (Second A) (Second B)), EQ A B.
Proof second_uniqueness_Out.

Section pair_uniqueness_proof.
Variable A : Ens.
Variable B : Ens.
Variable C : Ens.
Variable D : Ens.
Hypothesis e : EQ (PAIR A B) (PAIR C D).

Let fA := First A.
Let fC := First C.
Let secB := Second B.
Let secD := Second D.

Let step1 : has_leq_1_elements fA := Singletons_have_leq_1_elements A.

Let step2 : has_leq_1_elements fC := Singletons_have_leq_1_elements C.

Let step3 : has_geq_2_elements secB := Second_has_geq_2_elements B.

Let step4 : has_geq_2_elements secD := Second_has_geq_2_elements D.

Let step5 : pairwise_EQ fA secB fC secD :=
  Doubleton_uniqueness has_leq_1_elements fA secB fC secD step1 step3 step2
    step4 e.

Let step6 : EQ fA fC := pairwise_EQ_ac fA secB fC secD step5.

Let step7 : EQ secB secD := pairwise_EQ_bd fA secB fC secD step5.

Let step8 : EQ A C := First_uniqueness A C step6.

Let step9 : EQ B D := Second_uniqueness B D step7.

Definition pair_uniqueness_Out : pairwise_EQ A B C D :=
  Build_pairwise_EQ A B C D step8 step9.

End pair_uniqueness_proof.


Theorem PAIR_uniqueness :
 ∀ (A B C D : Ens) (e : EQ (PAIR A B) (PAIR C D)), pairwise_EQ A B C D.
Proof pair_uniqueness_Out.

Theorem PAIR_uni_ac :
 ∀ (A B C D : Ens) (e : EQ (PAIR A B) (PAIR C D)), EQ A C.
Proof
  fun (A B C D : Ens) (e : EQ (PAIR A B) (PAIR C D)) ⇒
  pairwise_EQ_ac A B C D (PAIR_uniqueness A B C D e).

Theorem PAIR_uni_bd :
 ∀ (A B C D : Ens) (e : EQ (PAIR A B) (PAIR C D)), EQ B D.
Proof
  fun (A B C D : Ens) (e : EQ (PAIR A B) (PAIR C D)) ⇒
  pairwise_EQ_bd A B C D (PAIR_uniqueness A B C D e).

Definition is_a_pair (M : Ens) :=
  EXISTS (fun A : Ens ⇒ EXISTS (fun B : Ens ⇒ EQ M (PAIR A B))).

Section a_pair_is_a_pair_proof.
Variable A : Ens.
Variable B : Ens.

Let M := PAIR A B.

Let step1 : EQ M (PAIR A B) := EQ_refl M.

Let step2 : EXISTS (fun B1 : Ens ⇒ EQ M (PAIR A B1)) :=
  EXISTS_th1 (fun B1 : Ens ⇒ EQ M (PAIR A B1)) B step1.

Definition a_pair_is_a_pair_Out : is_a_pair M :=
  EXISTS_th1 (fun A1 : Ens ⇒ EXISTS (fun B1 : Ens ⇒ EQ M (PAIR A1 B1))) A
    step2.

End a_pair_is_a_pair_proof.

Theorem a_pair_is_a_pair : ∀ A B : Ens, is_a_pair (PAIR A B).
Proof a_pair_is_a_pair_Out.

Theorem a_pair_is_a_pair_th2 :
 ∀ (A B U : Ens) (i : EQ (PAIR A B) U), is_a_pair U.
Proof
  fun (A B U : Ens) (i : EQ (PAIR A B) U) ⇒
  Big_Extensionality (fun V : Ens ⇒ is_a_pair V) (PAIR A B) U
    (a_pair_is_a_pair A B) i.


Definition PR1 (M : Ens) :=
  CHOICE (fun A : Ens ⇒ EXISTS (fun B : Ens ⇒ EQ M (PAIR A B))).

Theorem PAIR_proj1_pr1 :
 ∀ (M : Ens) (p : is_a_pair M),
 EXISTS (fun B : Ens ⇒ EQ M (PAIR (PR1 M) B)).
 Proof
   fun (M : Ens) (p : is_a_pair M) ⇒
   CHOICE_pr (fun A : Ens ⇒ EXISTS (fun B : Ens ⇒ EQ M (PAIR A B))) p.

Definition PR2 (M : Ens) := CHOICE (fun B : Ens ⇒ EQ M (PAIR (PR1 M) B)).

Theorem PAIR_proj_th1 :
 ∀ (M : Ens) (p : is_a_pair M), EQ M (PAIR (PR1 M) (PR2 M)).
Proof
  fun (M : Ens) (p : is_a_pair M) ⇒
  CHOICE_pr (fun B : Ens ⇒ EQ M (PAIR (PR1 M) B)) (PAIR_proj1_pr1 M p).

Section pair_proj2_proof.
Variable X Y : Ens.

Let M := PAIR X Y.

Let step1 : is_a_pair M.
Proof a_pair_is_a_pair X Y.

Let step2 : EQ M (PAIR (PR1 M) (PR2 M)).
Proof PAIR_proj_th1 M step1.

Lemma pair_proj2_Out : pairwise_EQ X Y (PR1 M) (PR2 M).
Proof PAIR_uniqueness X Y (PR1 M) (PR2 M) step2.

End pair_proj2_proof.

Theorem PAIR_proj_th2 :
 ∀ X Y : Ens, pairwise_EQ X Y (PR1 (PAIR X Y)) (PR2 (PAIR X Y)).
Proof pair_proj2_Out.

Theorem PAIR_proj_th3 : ∀ X Y : Ens, EQ X (PR1 (PAIR X Y)).
Proof
  fun X Y : Ens ⇒
  pairwise_EQ_ac X Y (PR1 (PAIR X Y)) (PR2 (PAIR X Y)) (PAIR_proj_th2 X Y).

Theorem PAIR_proj_th4 : ∀ X Y : Ens, EQ Y (PR2 (PAIR X Y)).
Proof
  fun X Y : Ens ⇒
  pairwise_EQ_bd X Y (PR1 (PAIR X Y)) (PR2 (PAIR X Y)) (PAIR_proj_th2 X Y).


Section PAIR_proj_uni_proof.
Variable M : Ens.
Hypothesis m : is_a_pair M.
Variable N : Ens.
Hypothesis n : is_a_pair N.
Hypothesis e : EQ (PR1 M) (PR1 N).
Hypothesis f : EQ (PR2 M) (PR2 N).

Let M1 := PR1 M.
Let M2 := PR2 M.
Let N1 := PR1 N.
Let N2 := PR2 N.

Let M12 := PAIR M1 M2.
Let N12 := PAIR N1 N2.

Let U := PAIR M1 N2.

Let step1 : EQ M12 M12 := EQ_refl M12.

Let step2 : EQ M12 U :=
  Big_Extensionality (fun X : Ens ⇒ EQ M12 (PAIR M1 X)) M2 N2 step1 f.

Let step3 : EQ U U := EQ_refl U.

Let step4 : EQ U N12 :=
  Big_Extensionality (fun X : Ens ⇒ EQ U (PAIR X N2)) M1 N1 step3 e.

Let step5 : EQ M12 N12 := EQ_trans M12 U N12 step2 step4.

Let step6 : EQ M M12 := PAIR_proj_th1 M m.

Let step7 : EQ N N12 := PAIR_proj_th1 N n.

Let step8 : EQ N12 N := EQ_symm N N12 step7.

Let step9 : EQ M N12 := EQ_trans M M12 N12 step6 step5.

Definition PAIR_proj_uni_Out : EQ M N := EQ_trans M N12 N step9 step8.

End PAIR_proj_uni_proof.


Theorem PAIR_proj_uni :
 ∀ (M : Ens) (m : is_a_pair M) (N : Ens) (n : is_a_pair N)
   (e : EQ (PR1 M) (PR1 N)) (f : EQ (PR2 M) (PR2 N)),
 EQ M N.
Proof PAIR_proj_uni_Out.


Definition Powerset (X : Ens) := REPLACEMENT (fun Y : Ens ⇒ SUB Y X).

Theorem Powerset_pr1 : ∀ (X Y : Ens) (h : SUB Y X), IN Y (Powerset X).
Proof
  fun X : Ens ⇒
  REPLACEMENT_pr1 (fun Y : Ens ⇒ SUB Y X) (Powerset_bounded X).

Theorem Powerset_pr2 : ∀ (X Y : Ens) (i : IN Y (Powerset X)), SUB Y X.
Proof
  fun X : Ens ⇒
  REPLACEMENT_pr2 (fun Y : Ens ⇒ SUB Y X) (Powerset_bounded X).

Section power0.
Variable A : Ens.

Let step1 : SUB Zero A.
Proof EmptySet_th2 A.

Lemma power0_Out : IN Zero (Powerset A).
Proof Powerset_pr1 A Zero step1.
End power0.

Theorem Powerset_th1 : ∀ A : Ens, IN Zero (Powerset A).
Proof power0_Out.

Section power1.
Variable A X Y : Ens.
Hypothesis x : IN X (Powerset A).
Hypothesis y : IN Y (Powerset A).

Let step1 : SUB X A.
Proof Powerset_pr2 A X x.

Let step2 : SUB Y A.
Proof Powerset_pr2 A Y y.

Let step3 : SUB (union X Y) A.
Proof union_pr3 X Y A step1 step2.

Lemma power1_Out1 : IN (union X Y) (Powerset A).
Proof Powerset_pr1 A (union X Y) step3.

Let step4 : SUB (intersection X Y) X.
Proof intersection_th1 X Y.

Let step5 : SUB (intersection X Y) A.
Proof SUB_trans (intersection X Y) X A step4 step1.

Lemma power1_Out2 : IN (intersection X Y) (Powerset A).
Proof Powerset_pr1 A (intersection X Y) step5.

End power1.

Theorem Powerset_th2 :
 ∀ (A X Y : Ens) (x : IN X (Powerset A)) (y : IN Y (Powerset A)),
 IN (union X Y) (Powerset A).
Proof power1_Out1.

Theorem Powerset_th3 :
 ∀ (A X Y : Ens) (x : IN X (Powerset A)),
 
 IN (intersection X Y) (Powerset A).
Proof power1_Out2.

Section power2.
Variable A X : Ens.
Hypothesis i : IN X A.

Let step1 : SUB (Singleton X) A.
Proof Singleton_th1 X A i.

Lemma power2_Out : IN (Singleton X) (Powerset A).
Proof Powerset_pr1 A (Singleton X) step1.

End power2.

Theorem Powerset_th4 :
 ∀ (A X : Ens) (x : IN X A), IN (Singleton X) (Powerset A).
Proof power2_Out.

Section power3.
Variable A X Y : Ens.
Hypothesis x : IN X A.
Hypothesis y : IN Y A.

Let step1 : IN (Singleton X) (Powerset A).
Proof Powerset_th4 A X x.
Let step2 : IN (Singleton Y) (Powerset A).
Proof Powerset_th4 A Y y.

Lemma power3_Out : IN (Doubleton X Y) (Powerset A).
Proof Powerset_th2 A (Singleton X) (Singleton Y) step1 step2.

End power3.

Theorem Powerset_th5 :
 ∀ (A X Y : Ens) (x : IN X A) (y : IN Y A),
 IN (Doubleton X Y) (Powerset A).
Proof power3_Out.

Section power4.
Variable A X : Ens.
Hypothesis x : IN X A.

Let sX := Singleton X.
Let P := Powerset A.

Let step1 : IN Zero P.
Proof Powerset_th1 A.

Let step2 : IN sX P.
Proof Powerset_th4 A X x.

Lemma power4_Out : IN (Second X) (Powerset P).
Proof Powerset_th5 P Zero sX step1 step2.

End power4.

Theorem Powerset_th6 :
 ∀ (A X : Ens) (x : IN X A), IN (Second X) (Powerset (Powerset A)).
Proof power4_Out.

Section power5.
Variable A B : Ens.
Hypothesis a : SUB A B.

Variable X : Ens.
Hypothesis x : IN X (Powerset A).

Let step1 : SUB X A.
Proof Powerset_pr2 A X x.

Let step2 : SUB X B.
Proof SUB_trans X A B step1 a.

Lemma power5_Out : IN X (Powerset B).
Proof Powerset_pr1 B X step2.

End power5.

Theorem Powerset_th7 :
 ∀ (A B : Ens) (a : SUB A B), SUB (Powerset A) (Powerset B).
Proof power5_Out.


Definition Element_of_NN (Y : Ens) :=
  ∀ (X : Ens) (k : Contains_NN X), IN Y X.

Section Zero_element_of_NN_proof.
Variable X : Ens.
Hypothesis k : Contains_NN X.

Definition Zero_element_of_NN_proof_Out : IN Zero X := Contains_NN_zero X k.
End Zero_element_of_NN_proof.

Theorem Zero_element_of_NN : Element_of_NN Zero.
Proof Zero_element_of_NN_proof_Out.

Section Nexts_element_of_NN_proof.
Variable A : Ens.
Hypothesis h : Element_of_NN A.
Variable X : Ens.
Hypothesis k : Contains_NN X.

Let N := Next A.

Let j : IN A X := h X k.

Definition Nexts_element_of_NN_proof_Out : IN N X :=
  Contains_NN_nexts X k A j.

End Nexts_element_of_NN_proof.

Theorem Nexts_element_of_NN :
 ∀ (A : Ens) (h : Element_of_NN A), Element_of_NN (Next A).
Proof Nexts_element_of_NN_proof_Out.

Definition Set_containing_NN := CHOICE Contains_NN.

Theorem Set_containing_NN_pr : Contains_NN Set_containing_NN.
Proof CHOICE_pr Contains_NN Infinity_exists.

Section Bounded_NN_proof.
Hypothesis u : DOESNT_EXIST (fun A : Ens ⇒ Bounded_By A Element_of_NN).

Let step1 : ∀ A : Ens, ¬ Bounded_By A Element_of_NN := u.

Let B : Ens := Set_containing_NN.
Let v : Contains_NN B := Set_containing_NN_pr.

Section Bounded_NN_proof2.
Variable Z : Ens.
Hypothesis w : Element_of_NN Z.

Definition Bounded_NN_proof2_Out : IN Z B := w B v.

End Bounded_NN_proof2.

Let step2 : Bounded_By B Element_of_NN := Bounded_NN_proof2_Out.

Definition Bounded_NN_proof_Out : False := step1 B step2.

End Bounded_NN_proof.

Theorem Bounded_NN_pre : EXISTS (fun A : Ens ⇒ Bounded_By A Element_of_NN).
Proof Bounded_NN_proof_Out.

Theorem Bounded_NN : Bounded Element_of_NN.
Proof Bounded_NN_pre.

Definition Naturals := REPLACEMENT Element_of_NN.

Theorem Naturals_pr1 : ∀ X : Ens, Element_of_NN X → IN X Naturals.
Proof REPLACEMENT_pr1 Element_of_NN Bounded_NN.

Theorem Naturals_pr2 : ∀ X : Ens, IN X Naturals → Element_of_NN X.
Proof REPLACEMENT_pr2 Element_of_NN Bounded_NN.


Theorem Zero_in_Naturals : IN Zero Naturals.
Proof Naturals_pr1 Zero Zero_element_of_NN.

Theorem Nexts_in_Naturals :
 ∀ (A : Ens) (h : IN A Naturals), IN (Next A) Naturals.
Proof
  fun (A : Ens) (h : IN A Naturals) ⇒
  Naturals_pr1 (Next A) (Nexts_element_of_NN A (Naturals_pr2 A h)).

Theorem Contains_NN_Naturals : Contains_NN Naturals.
Proof Build_Contains_NN Naturals Zero_in_Naturals Nexts_in_Naturals.

Section Naturals_th1_proof.
Variable X : Ens.
Hypothesis h : Contains_NN X.

Variable B : Ens.
Hypothesis k : IN B Naturals.

Let step1 : Element_of_NN B := Naturals_pr2 B k.

Definition Naturals_th1_proof_Out : IN B X := step1 X h.

End Naturals_th1_proof.

Theorem Naturals_th1 : ∀ (X : Ens) (h : Contains_NN X), SUB Naturals X.
Proof Naturals_th1_proof_Out.

Section A_sub_next_A_proof.
Variable A : Ens.
Let N := Next A.

Definition A_sub_next_A_Out : SUB A N := union_pr1 A (Singleton A).

End A_sub_next_A_proof.

Theorem anything_sub_next_of_itself : ∀ A : Ens, SUB A (Next A).
Proof A_sub_next_A_Out.

Section A_in_next_A_proof.
Variable A : Ens.
Let N := Next A.

Let step1 : IN A (Singleton A) := Singleton_pr1 A.

Definition A_in_next_A_Out : IN A N := union_th2 A (Singleton A) A step1.

End A_in_next_A_proof.

Theorem anything_in_next_of_itself : ∀ A : Ens, IN A (Next A).
Proof A_in_next_A_Out.


Section naturals_inductionA_proof.

Variable P : Ens → Prop.
Hypothesis IH_zero : P Zero.
Hypothesis
  IH_nexts : ∀ (A : Ens) (h : IN A Naturals) (k : P A), P (Next A).

Let S := Set_Of Naturals P.

Let step1 : IN Zero S := Set_Of_th1 Naturals P Zero Zero_in_Naturals IH_zero.

Let step2 : SUB S Naturals := Set_Of_th4 Naturals P.

Let step3 (A : Ens) (h : IN A S) : P A := Set_Of_th2 Naturals P A h.

Let step4 (A : Ens) (h : IN A S) : P (Next A) :=
  IH_nexts A (step2 A h) (step3 A h).

Let step5 (B : Ens) (h : IN B Naturals) (k : P B) :
  IN B S := Set_Of_th1 Naturals P B h k.

Section naturals_inductionA1.
Variable A : Ens.
Hypothesis h : IN A S.
Let N := Next A.

Let step1_1 : P N := step4 A h.

Let step1_2 : IN N Naturals := Nexts_in_Naturals A (step2 A h).

Definition naturals_inductionA1_Out : IN N S := step5 N step1_2 step1_1.

End naturals_inductionA1.

Let step6 : ∀ (A : Ens) (h : IN A S), IN (Next A) S :=
  naturals_inductionA1_Out.

Let step7 : Contains_NN S := Build_Contains_NN S step1 step6.

Variable B : Ens.
Hypothesis p : IN B Naturals.

Let step8 : Element_of_NN B := Naturals_pr2 B p.

Let step9 : IN B S := step8 S step7.

Definition naturals_inductionA_Out : P B := step3 B step9.

End naturals_inductionA_proof.

Definition naturals_induction_nexts (P : Ens → Prop) :=
  ∀ (A : Ens) (h : IN A Naturals) (k : P A), P (Next A).

Theorem naturals_inductionA :
 ∀ (P : Ens → Prop) (IH_zero : P Zero)
   (IH_nexts : naturals_induction_nexts P) (B : Ens)
   (p : IN B Naturals), P B.
Proof naturals_inductionA_Out.


Definition in_then_strictsub (N : Ens) :=
  ∀ X : Ens, IN X N → StrictSUB X N.

Definition not_in_itself (X : Ens) := ¬ IN X X.

Record naturals_main_ind_hyp (N : Ens) : Prop :=
  {naturals_main_ind1 : in_then_strictsub N;
   naturals_main_ind2 : not_in_itself N}.


Section strictsub_next_proof.
Variable A : Ens.
Hypothesis h : not_in_itself A.
Let N := Next A.

Let step1 : SUB A N := anything_sub_next_of_itself A.

Section strictsub_next1.
Hypothesis k : EQ A N.
Let step2 : SUB N A := EQ_backwards A N k.
Let step3 : IN A N := anything_in_next_of_itself A.
Let step4 : IN A A := step2 A step3.
Definition strictsub_next1_Out : False := h step4.

End strictsub_next1.

Let step5 : ¬ EQ A N := strictsub_next1_Out.

Definition strictsub_next_Out : StrictSUB A N :=
  Build_StrictSUB A N step1 step5.

End strictsub_next_proof.

Theorem some_things_strictsub_their_nexts :
 ∀ (A : Ens) (h : not_in_itself A), StrictSUB A (Next A).
Proof strictsub_next_Out.


Section in_then_strictsub_Zero_proof.
Variable X : Ens.
Hypothesis h : IN X Zero.
Let step1 : False := EmptySet_th1 X h.
Definition in_iff_strictsub_Zero_Out : StrictSUB X Zero :=
  false_implies_everything (StrictSUB X Zero) step1.

End in_then_strictsub_Zero_proof.

Theorem in_then_strictsub_Zero :
 ∀ X : Ens, IN X Zero → StrictSUB X Zero.
Proof in_iff_strictsub_Zero_Out.

Section not_in_itself_Zero.
Hypothesis h : IN Zero Zero.
Definition not_in_itself_Zero_Out : False := EmptySet_th1 Zero h.

End not_in_itself_Zero.

Theorem zero_not_in_itself : not_in_itself Zero.
Proof not_in_itself_Zero_Out.

Theorem naturals_main_ind_for_Zero : naturals_main_ind_hyp Zero.
Proof
  Build_naturals_main_ind_hyp Zero in_then_strictsub_Zero zero_not_in_itself.

Section naturals_main_induction_step.
Variable A : Ens.
Hypothesis h : naturals_main_ind_hyp A.

Let h1 : in_then_strictsub A := naturals_main_ind1 A h.

Let h2 : not_in_itself A := naturals_main_ind2 A h.

Let N := Next A.

Let in_A_N : IN A N := anything_in_next_of_itself A.

Let sub_A_N : SUB A N := anything_sub_next_of_itself A.

Section naturals_main_induction2.
Hypothesis k : IN N N.

Section naturals_main_induction2a.
Hypothesis l : EQ A N.
Let step2a1 : IN A N := Extensionality A N N l k.
Let step2a2 : SUB N A := EQ_backwards A N l.
Let step2a3 : IN A A := step2a2 A step2a1.

Definition naturals_main_induction2a_Out : False := h2 step2a3.

End naturals_main_induction2a.

Let step2_1 : ¬ EQ A N := naturals_main_induction2a_Out.

Section naturals_main_induction2b.
Hypothesis m : IN N (Singleton A).
Let step2b1 : EQ A N := Singleton_pr2 A N m.
Definition naturals_main_induction2b_Out : False := step2_1 step2b1.

End naturals_main_induction2b.

Let step2_2 : ¬ IN N (Singleton A) := naturals_main_induction2b_Out.

Section naturals_main_induction2c.
Hypothesis n : IN N A.

Let step2c1 : StrictSUB N A := h1 N n.
Let step2c2 : SUB N A := StrictSUB_sub N A step2c1.
Let step2c3 : IN A N := anything_in_next_of_itself A.
Let step2c4 : IN A A := step2c2 A step2c3.

Definition naturals_main_induction2c_Out : False := h2 step2c4.

End naturals_main_induction2c.

Let step2_3 : ¬ IN N A := naturals_main_induction2c_Out.

Let step2_4 : ¬ IN N N := union_th3 A (Singleton A) N step2_3 step2_2.

Definition naturals_main_induction2_Out : False := step2_4 k.

End naturals_main_induction2.

Let sublemma1 : not_in_itself N := naturals_main_induction2_Out.

Section naturals_main_induction3.
Variable X : Ens.
Hypothesis p : IN X N.

Section naturals_main_induction3em.
Hypothesis contra : ¬ StrictSUB X N.

Section naturals_main_induction3a.
Hypothesis q : IN X A.

Let step3a1 : StrictSUB X A := h1 X q.

Let step3a2 : StrictSUB X N := StrictSUB_trans1 X A N step3a1 sub_A_N.

Definition naturals_main_induction3a_Out : False := contra step3a2.

End naturals_main_induction3a.

Let step3_1 : ¬ IN X A := naturals_main_induction3a_Out.

Section naturals_main_induction3b.
Hypothesis r : IN X (Singleton A).

Let r_bis : EQ A X := Singleton_pr2 A X r.

Let subXA : SUB X A := EQ_backwards A X r_bis.
Let subAX : SUB A X := EQ_forwards A X r_bis.

Let step3b1 : SUB A N := sub_A_N.

Let step3b2 : SUB X N := SUB_trans X A N subXA step3b1.

Section naturals_main_induction3bI.
Hypothesis s : EQ X N.
Let step3bI1 : EQ A N := EQ_trans A X N r_bis s.
Let step3bI2 : SUB N A := EQ_backwards A N step3bI1.
Let step3bI3 : IN A A := step3bI2 A in_A_N.

Definition naturals_main_induction3bI_Out : False := h2 step3bI3.

End naturals_main_induction3bI.

Let step3b3 : ¬ EQ X N := naturals_main_induction3bI_Out.

Let step3b4 : StrictSUB X N := Build_StrictSUB X N step3b2 step3b3.

Definition naturals_main_induction3b_Out : False := contra step3b4.

End naturals_main_induction3b.

Let step3_2 : ¬ IN X (Singleton A) := naturals_main_induction3b_Out.

Let step3_3 : ¬ IN X N := union_th3 A (Singleton A) X step3_1 step3_2.

Definition naturals_main_induction3em_Out : False := step3_3 p.

End naturals_main_induction3em.

Let sublemma2 : ¬ ¬ StrictSUB X N := naturals_main_induction3em_Out.

Definition naturals_main_induction3_Out : StrictSUB X N :=
  excluded_middle (StrictSUB X N) sublemma2.

End naturals_main_induction3.

Let sublemma3 : in_then_strictsub N := naturals_main_induction3_Out.

Definition naturals_main_induction_step_Out : naturals_main_ind_hyp N :=
  Build_naturals_main_ind_hyp N sublemma3 sublemma1.

End naturals_main_induction_step.

Theorem naturals_main_induction_next :
 ∀ (A : Ens) (h : naturals_main_ind_hyp A),
 naturals_main_ind_hyp (Next A).
Proof naturals_main_induction_step_Out.


Theorem naturals_main_induction_next_1 :
 naturals_induction_nexts naturals_main_ind_hyp.
Proof
  fun (A : Ens) (u : IN A Naturals) (h : naturals_main_ind_hyp A) ⇒
  naturals_main_induction_next A h.

Theorem naturals_main_th1 :
 ∀ (B : Ens) (i : IN B Naturals), naturals_main_ind_hyp B.
Proof
  naturals_inductionA naturals_main_ind_hyp naturals_main_ind_for_Zero
    naturals_main_induction_next_1.

Theorem naturals_main_th2 :
 ∀ (B : Ens) (i : IN B Naturals), in_then_strictsub B.
Proof
  fun (B : Ens) (i : IN B Naturals) ⇒
  naturals_main_ind1 B (naturals_main_th1 B i).

Theorem naturals_main_th2_rewrite :
 ∀ (B : Ens) (i : IN B Naturals) (A : Ens) (j : IN A B), StrictSUB A B.
Proof naturals_main_th2.

Theorem naturals_main_th3 :
 ∀ (B : Ens) (i : IN B Naturals), not_in_itself B.
Proof
  fun (B : Ens) (i : IN B Naturals) ⇒
  naturals_main_ind2 B (naturals_main_th1 B i).

Theorem naturals_main_th3_rewrite :
 ∀ (B : Ens) (i : IN B Naturals), ¬ IN B B.
Proof naturals_main_th3.



Definition UnionPlus (F : Ens) := union F (Union F).

Definition Total (R : Ens) := UnionPlus (UnionPlus (UnionPlus R)).

Theorem UnionPlus_th1 : ∀ (X F : Ens) (i : IN X F), IN X (UnionPlus F).
Proof fun (X F : Ens) (i : IN X F) ⇒ union_th1 F (Union F) X i.

Theorem UnionPlus_th2 :
 ∀ (X U F : Ens) (i : IN X U) (j : IN U F), IN X (UnionPlus F).
Proof
  fun (X U F : Ens) (i : IN X U) (j : IN U F) ⇒
  union_th2 F (Union F) X (Union_th1 F X U i j).

Section total_th1_proof.
Variable X F : Ens.
Hypothesis i : IN X F.

Let step1 : IN X (UnionPlus F).
Proof UnionPlus_th1 X F i.

Let step2 : IN X (UnionPlus (UnionPlus F)).
Proof UnionPlus_th1 X (UnionPlus F) step1.

Lemma total_th1_Out : IN X (Total F).
Proof UnionPlus_th1 X (UnionPlus (UnionPlus F)) step2.

End total_th1_proof.

Theorem Total_th1 : ∀ (X F : Ens) (i : IN X F), IN X (Total F).
Proof total_th1_Out.

Section total_th2_proof.
Variable X Y F : Ens.
Hypothesis i : IN X Y.
Hypothesis j : IN Y F.

Let step1 : IN X (UnionPlus F).
Proof UnionPlus_th2 X Y F i j.

Let step2 : IN X (UnionPlus (UnionPlus F)).
Proof UnionPlus_th1 X (UnionPlus F) step1.

Lemma total_th2_Out : IN X (Total F).
Proof UnionPlus_th1 X (UnionPlus (UnionPlus F)) step2.

End total_th2_proof.

Theorem Total_th2 :
 ∀ (X Y F : Ens) (i : IN X Y) (j : IN Y F), IN X (Total F).
Proof total_th2_Out.

Section total_th3_proof.
Variable X Y Z F : Ens.
Hypothesis i : IN X Y.
Hypothesis j : IN Y Z.
Hypothesis k : IN Z F.

Let step1 : IN Y (UnionPlus F).
Proof UnionPlus_th2 Y Z F j k.

Let step2 : IN X (UnionPlus (UnionPlus F)).
Proof UnionPlus_th2 X Y (UnionPlus F) i step1.

Lemma total_th3_Out : IN X (Total F).
Proof UnionPlus_th1 X (UnionPlus (UnionPlus F)) step2.

End total_th3_proof.

Theorem Total_th3 :
 ∀ (X Y Z F : Ens) (i : IN X Y) (j : IN Y Z) (k : IN Z F),
 IN X (Total F).
Proof total_th3_Out.

Section total_th4_proof.
Variable X Y Z W F : Ens.
Hypothesis i : IN X Y.
Hypothesis j : IN Y Z.
Hypothesis k : IN Z W.
Hypothesis l : IN W F.

Let step1 : IN Z (UnionPlus F).
Proof UnionPlus_th2 Z W F k l.

Let step2 : IN Y (UnionPlus (UnionPlus F)).
Proof UnionPlus_th2 Y Z (UnionPlus F) j step1.

Lemma total_th4_Out : IN X (Total F).
Proof UnionPlus_th2 X Y (UnionPlus (UnionPlus F)) i step2.

End total_th4_proof.

Theorem Total_th4 :
 ∀ (X Y Z W F : Ens) (i : IN X Y) (j : IN Y Z) (k : IN Z W) (l : IN W F),
 IN X (Total F).
Proof total_th4_Out.

Section total_and_pairs_1.
Variable R : Ens.
Variable A B : Ens.
Hypothesis i : IN (PAIR A B) R.

Let step1 : IN A (First A).
Proof Singleton_pr1 A.

Let step2 : IN B (Singleton B).
Proof Singleton_pr1 B.

Let step3 : IN (Singleton B) (Second B).
Proof Doubleton_th2 Zero (Singleton B).

Let step4 : IN (First A) (PAIR A B).
Proof Doubleton_th1 (First A) (Second B).

Let step5 : IN (Second B) (PAIR A B).
Proof Doubleton_th2 (First A) (Second B).

Lemma total_and_pairs_1_OutA : IN A (Total R).
Proof Total_th3 A (First A) (PAIR A B) R step1 step4 i.

Lemma total_and_pairs_1_OutB : IN B (Total R).
Proof Total_th4 B (Singleton B) (Second B) (PAIR A B) R step2 step3 step5 i.

End total_and_pairs_1.

Theorem Relation_Total_th1 :
 ∀ (R A B : Ens) (i : IN (PAIR A B) R), IN A (Total R).
Proof total_and_pairs_1_OutA.

Theorem Relation_Total_th2 :
 ∀ (R A B : Ens) (i : IN (PAIR A B) R), IN B (Total R).
Proof total_and_pairs_1_OutB.



Definition Domain_prop (R X : Ens) := EXISTS (fun Y : Ens ⇒ IN (PAIR X Y) R).

Definition Range_prop (R Y : Ens) := EXISTS (fun X : Ens ⇒ IN (PAIR X Y) R).


Definition EV (R X : Ens) := CHOICE (fun Y : Ens ⇒ IN (PAIR X Y) R).

Theorem EV_pr :
 ∀ (R X : Ens) (p : Domain_prop R X), IN (PAIR X (EV R X)) R.
Proof
  fun (R X : Ens) (p : Domain_prop R X) ⇒
  CHOICE_pr (fun Y : Ens ⇒ IN (PAIR X Y) R) p.

Definition inverse_EV (R Y : Ens) := CHOICE (fun X : Ens ⇒ IN (PAIR X Y) R).

Theorem inverse_EV_pr :
 ∀ (R Y : Ens) (p : Range_prop R Y), IN (PAIR (inverse_EV R Y) Y) R.
Proof
  fun (R Y : Ens) (p : Range_prop R Y) ⇒
  CHOICE_pr (fun X : Ens ⇒ IN (PAIR X Y) R) p.


Section Domain_prop_bounded_proof.
Variable R : Ens.

Let T := Total R.

Section Domain_prop_bounded_proof_1.
Variable X : Ens.
Hypothesis p : Domain_prop R X.

Let Y := EV R X.

Let step1_1 : IN (PAIR X Y) R.
Proof EV_pr R X p.

Lemma Domain_prop_bounded_proof_1_Out : IN X T.
Proof Relation_Total_th1 R X Y step1_1.

End Domain_prop_bounded_proof_1.

Let step1 : Bounded_By T (Domain_prop R).
Proof Domain_prop_bounded_proof_1_Out.

Lemma Domain_prop_bounded_Out : Bounded (Domain_prop R).
Proof Bounded_th2 (Domain_prop R) T step1.

End Domain_prop_bounded_proof.

Theorem Domain_prop_bounded : ∀ R : Ens, Bounded (Domain_prop R).
Proof Domain_prop_bounded_Out.

Section Range_prop_bounded_proof.
Variable R : Ens.

Let T := Total R.

Section Range_prop_bounded_proof_1.
Variable Y : Ens.
Hypothesis p : Range_prop R Y.

Let X := inverse_EV R Y.

Let step1_1 : IN (PAIR X Y) R.
Proof inverse_EV_pr R Y p.

Lemma Range_prop_bounded_proof_1_Out : IN Y T.
Proof Relation_Total_th2 R X Y step1_1.

End Range_prop_bounded_proof_1.

Let step1 : Bounded_By T (Range_prop R).
Proof Range_prop_bounded_proof_1_Out.

Lemma Range_prop_bounded_Out : Bounded (Range_prop R).
Proof Bounded_th2 (Range_prop R) T step1.

End Range_prop_bounded_proof.

Theorem Range_prop_bounded : ∀ R : Ens, Bounded (Range_prop R).
Proof Range_prop_bounded_Out.


Definition Domain (R : Ens) := REPLACEMENT (Domain_prop R).

Theorem Domain_pr1 :
 ∀ (R X : Ens) (p : Domain_prop R X), IN X (Domain R).
Proof fun R : Ens ⇒ REPLACEMENT_pr1 (Domain_prop R) (Domain_prop_bounded R).

Theorem Domain_pr2 :
 ∀ (R X : Ens) (i : IN X (Domain R)), Domain_prop R X.
Proof fun R : Ens ⇒ REPLACEMENT_pr2 (Domain_prop R) (Domain_prop_bounded R).

Theorem EV_th1 :
 ∀ (R X : Ens) (i : IN X (Domain R)), IN (PAIR X (EV R X)) R.
Proof fun (R X : Ens) (i : IN X (Domain R)) ⇒ EV_pr R X (Domain_pr2 R X i).

Section Domain_th1_proof.
Variable R : Ens.
Variable X Y : Ens.
Hypothesis i : IN (PAIR X Y) R.

Let step1 : Domain_prop R X.
Proof EXISTS_th1 (fun Y1 : Ens ⇒ IN (PAIR X Y1) R) Y i.

Lemma Domain_th1_Out : IN X (Domain R).
Proof Domain_pr1 R X step1.

End Domain_th1_proof.

Theorem Domain_th1 :
 ∀ (R X Y : Ens) (i : IN (PAIR X Y) R), IN X (Domain R).
Proof Domain_th1_Out.


Definition Range (R : Ens) := REPLACEMENT (Range_prop R).

Theorem Range_pr1 : ∀ (R X : Ens) (p : Range_prop R X), IN X (Range R).
Proof fun R : Ens ⇒ REPLACEMENT_pr1 (Range_prop R) (Range_prop_bounded R).

Theorem Range_pr2 : ∀ (R X : Ens) (i : IN X (Range R)), Range_prop R X.
Proof fun R : Ens ⇒ REPLACEMENT_pr2 (Range_prop R) (Range_prop_bounded R).

Theorem inverse_EV_th1 :
 ∀ (R Y : Ens) (i : IN Y (Range R)), IN (PAIR (inverse_EV R Y) Y) R.
Proof
  fun (R Y : Ens) (i : IN Y (Range R)) ⇒ inverse_EV_pr R Y (Range_pr2 R Y i).

Section Range_th1_proof.
Variable R : Ens.
Variable X Y : Ens.
Hypothesis i : IN (PAIR X Y) R.

Let step1 : Range_prop R Y.
Proof EXISTS_th1 (fun X1 : Ens ⇒ IN (PAIR X1 Y) R) X i.

Lemma Range_th1_Out : IN Y (Range R).
Proof Range_pr1 R Y step1.

End Range_th1_proof.

Theorem Range_th1 :
 ∀ (R X Y : Ens) (i : IN (PAIR X Y) R), IN Y (Range R).
Proof Range_th1_Out.


Section eval_in_range_proof.

Variable R X : Ens.
Hypothesis i : IN X (Domain R).

Let Y := EV R X.

Let step1 : IN (PAIR X Y) R.
Proof EV_th1 R X i.

Lemma eval_in_range_Out : IN Y (Range R).
Proof Range_th1 R X Y step1.

End eval_in_range_proof.

Theorem EV_in_range :
 ∀ (R X : Ens) (i : IN X (Domain R)), IN (EV R X) (Range R).
Proof eval_in_range_Out.


Section inv_eval_in_domain_proof.

Variable R Y : Ens.
Hypothesis i : IN Y (Range R).

Let X := inverse_EV R Y.

Let step0 : Range_prop R Y.
Proof Range_pr2 R Y i.

Let step1 : IN (PAIR X Y) R.
Proof inverse_EV_pr R Y step0.

Lemma inv_eval_in_domain_Out : IN X (Domain R).
Proof Domain_th1 R X Y step1.

End inv_eval_in_domain_proof.

Theorem inverse_EV_in_domain :
 ∀ (R Y : Ens) (i : IN Y (Range R)), IN (inverse_EV R Y) (Domain R).
Proof inv_eval_in_domain_Out.


Definition is_a_relation (R : Ens) :=
  ∀ (X : Ens) (i : IN X R), is_a_pair X.

Section relation_1.
Variable R : Ens.
Hypothesis r : is_a_relation R.
Variable S : Ens.
Hypothesis h : SUB S R.

Variable X : Ens.
Hypothesis i : IN X S.

Let step1 : IN X R.
Proof h X i.

Lemma relation_1_Out : is_a_pair X.
Proof r X step1.

End relation_1.

Theorem relation_sub :
 ∀ (R : Ens) (r : is_a_relation R) (S : Ens), SUB S R → is_a_relation S.
Proof relation_1_Out.

Definition well_definedness (F : Ens) :=
  ∀ (X Y Z : Ens) (i : IN (PAIR X Y) F) (j : IN (PAIR X Z) F), EQ Y Z.

Section well_def_1.
Variable F : Ens.
Hypothesis w : well_definedness F.
Variable R : Ens.
Hypothesis h : SUB R F.

Variable X Y Z : Ens.
Hypothesis i : IN (PAIR X Y) R.
Hypothesis j : IN (PAIR X Z) R.

Let step1 : IN (PAIR X Y) F.
Proof h (PAIR X Y) i.

Let step2 : IN (PAIR X Z) F.
Proof h (PAIR X Z) j.

Lemma well_def_1_Out : EQ Y Z.
Proof w X Y Z step1 step2.

End well_def_1.

Theorem well_definedness_sub :
 ∀ (F : Ens) (w : well_definedness F) (R : Ens) (h : SUB R F),
 well_definedness R.
Proof well_def_1_Out.

Record is_a_function (F : Ens) : Prop :=
  {function_is_a_relation : is_a_relation F;
   function_well_definedness : well_definedness F}.

Theorem function_sub :
 ∀ (F : Ens) (f : is_a_function F) (G : Ens) (s : SUB G F),
 is_a_function G.
Proof
  fun (F : Ens) (f : is_a_function F) (G : Ens) (s : SUB G F) ⇒
  Build_is_a_function G (relation_sub F (function_is_a_relation F f) G s)
    (well_definedness_sub F (function_well_definedness F f) G s).

Record is_a_function_on (D F : Ens) : Prop :=
  {function_on_fn : is_a_function F; function_on_dom : EQ D (Domain F)}.

Theorem function_is_a_function_on :
 ∀ (F : Ens) (f : is_a_function F), is_a_function_on (Domain F) F.
Proof
  fun (F : Ens) (f : is_a_function F) ⇒
  Build_is_a_function_on (Domain F) F f (EQ_refl (Domain F)).

Section function_section_1.
Variable F : Ens.
Hypothesis f : is_a_function F.
Variable X Y : Ens.
Hypothesis i : IN (PAIR X Y) F.

Let step1 : IN X (Domain F).
Proof Domain_th1 F X Y i.

Let V := EV F X.

Let step3 : IN (PAIR X V) F.
Proof EV_th1 F X step1.

Let step5 : well_definedness F.
Proof function_well_definedness F f.

Lemma function_1_Out_F : EQ Y V.
Proof step5 X Y V i step3.

End function_section_1.

Theorem function_th1 :
 ∀ (F : Ens) (f : is_a_function F) (X Y : Ens) (i : IN (PAIR X Y) F),
 EQ Y (EV F X).
Proof function_1_Out_F.

Definition Extensionally_equivalent (F G : Ens) :=
  ∀ (X : Ens) (i : IN X (Domain F)) (j : IN X (Domain G)),
  EQ (EV F X) (EV G X).

Section ee_symm_proof.
Variable F G : Ens.
Hypothesis e : Extensionally_equivalent F G.

Variable X : Ens.
Hypothesis i : IN X (Domain G).
Hypothesis j : IN X (Domain F).

Let step1 : EQ (EV F X) (EV G X).
Proof e X j i.

Lemma ee_symm_Out : EQ (EV G X) (EV F X).
Proof EQ_symm (EV F X) (EV G X) step1.

End ee_symm_proof.

Theorem ex_eq_symm :
 ∀ F G : Ens,
 Extensionally_equivalent F G → Extensionally_equivalent G F.
Proof ee_symm_Out.

Section ee_sub_proof.
Variable F G : Ens.
Hypothesis f : is_a_function F.
Hypothesis g : is_a_function G.
Hypothesis s : SUB (Domain F) (Domain G).
Hypothesis e : Extensionally_equivalent F G.

Variable M : Ens.
Hypothesis i : IN M F.

Let step1 : is_a_relation F.
Proof function_is_a_relation F f.

Let step2 : is_a_pair M.
Proof step1 M i.

Let X := PR1 M.
Let Y := PR2 M.

Let step3 : EQ M (PAIR X Y).
Proof PAIR_proj_th1 M step2.

Let step4 : EQ (PAIR X Y) M.
Proof EQ_symm M (PAIR X Y) step3.

Let step5 : IN (PAIR X Y) F.
Proof Extensionality (PAIR X Y) M F step4 i.

Let V := EV F X.

Let step6 : EQ Y V.
Proof function_th1 F f X Y step5.

Let step7 : IN X (Domain F).
Proof Domain_th1 F X Y step5.

Let step8 : IN X (Domain G).
Proof s X step7.

Let W := EV G X.

Let step9 : EQ V W.
Proof e X step7 step8.

Let step10 : EQ Y W.
Proof EQ_trans Y V W step6 step9.

Let step10a : EQ W Y.
Proof EQ_symm Y W step10.

Let step11 : IN (PAIR X W) G.
Proof EV_th1 G X step8.

Let step12 : IN (PAIR X Y) G.
Proof
  Big_Extensionality (fun Y1 : Ens ⇒ IN (PAIR X Y1) G) W Y step11 step10a.

Lemma ee_sub_Out : IN M G.
Proof Extensionality M (PAIR X Y) G step3 step12.

End ee_sub_proof.

Theorem ex_eq_sub :
 ∀ (F G : Ens) (f : is_a_function F) (s : SUB (Domain F) (Domain G))
   (e : Extensionally_equivalent F G), SUB F G.
Proof ee_sub_Out.

Section ee_eq_proof.
Variable F G : Ens.
Hypothesis f : is_a_function F.
Hypothesis g : is_a_function G.
Hypothesis d : EQ (Domain F) (Domain G).
Hypothesis e : Extensionally_equivalent F G.

Let step1 : SUB (Domain F) (Domain G).
Proof EQ_forwards (Domain F) (Domain G) d.

Let step2 : SUB (Domain G) (Domain F).
Proof EQ_backwards (Domain F) (Domain G) d.

Let step3 : Extensionally_equivalent G F.
Proof ex_eq_symm F G e.

Let step4 : SUB F G.
Proof ex_eq_sub F G f step1 e.

Let step5 : SUB G F.
Proof ex_eq_sub G F g step2 step3.

Lemma ee_eq_Out : EQ F G.
Proof Build_EQ F G step4 step5.

End ee_eq_proof.

Theorem Extensionality_for_functions :
 ∀ (F G : Ens) (f : is_a_function F) (g : is_a_function G)
   (d : EQ (Domain F) (Domain G)) (e : Extensionally_equivalent F G),
 EQ F G.
Proof ee_eq_Out.


Section function_evaluation_proof.
Variable F X Y : Ens.
Hypothesis f : is_a_function F.
Hypothesis i : IN (PAIR X Y) F.

Let Z := EV F X.

Let step1 : IN X (Domain F).
Proof Domain_th1 F X Y i.

Let step2 : IN (PAIR X Z) F.
Proof EV_th1 F X step1.

Lemma fe_Out : EQ Y Z.
Proof function_well_definedness F f X Y Z i step2.

End function_evaluation_proof.

Theorem function_evaluation :
 ∀ (F X Y : Ens) (f : is_a_function F) (i : IN (PAIR X Y) F),
 EQ Y (EV F X).
Proof fe_Out.


Definition restricted_to (A F : Ens) :=
  Set_Of F (fun M : Ens ⇒ IN (PR1 M) A).

Theorem restricted_to_th1 :
 ∀ (A F U : Ens) (i : IN U F) (j : IN (PR1 U) A),
 IN U (restricted_to A F).
Proof
  fun (A F U : Ens) (i : IN U F) (j : IN (PR1 U) A) ⇒
  Set_Of_th1 F (fun M : Ens ⇒ IN (PR1 M) A) U i j.

Theorem restricted_to_th2 :
 ∀ (A F U : Ens) (i : IN U (restricted_to A F)), IN (PR1 U) A.
Proof
  fun (A F U : Ens) (i : IN U (restricted_to A F)) ⇒
  Set_Of_th2 F (fun M : Ens ⇒ IN (PR1 M) A) U i.

Theorem restricted_to_th3 :
 ∀ (A F U : Ens) (i : IN U (restricted_to A F)), IN U F.
Proof
  fun (A F U : Ens) (i : IN U (restricted_to A F)) ⇒
  Set_Of_th3 F (fun M : Ens ⇒ IN (PR1 M) A) U i.

Theorem restricted_to_th4 : ∀ A F : Ens, SUB (restricted_to A F) F.
Proof fun A F : Ens ⇒ restricted_to_th3 A F.

Section restricted_to_1.
Variable A F : Ens.

Section res_to_1a.
Variable X : Ens.
Hypothesis i : IN X (Domain (restricted_to A F)).

Let Y := EV (restricted_to A F) X.

Let stepa1 : IN (PAIR X Y) (restricted_to A F).
Proof EV_th1 (restricted_to A F) X