Basic Infrastructure starting from Set Theory Axioms

Basic Logic and Set Theory

Object. The name Eps_i is a term of type (set → prop) → set.

Axiom. (Eps_i_ax) We take the following as an axiom:

∀P : set → prop, ∀x : set, P x → P (Eps_i P)

Definition. We define True to be ∀p : prop, p → p of type prop.

Definition. We define False to be ∀p : prop, p of type prop.

Definition. We define not to be λA : prop ⇒ A → False of type prop → prop.

Notation. We use ¬ as a prefix operator with priority 700 corresponding to applying term not.

Definition. We define and to be λA B : prop ⇒ ∀p : prop, (A → B → p) → p of type prop → prop → prop.

Notation. We use ∧ as an infix operator with priority 780 and which associates to the left corresponding to applying term and.

Definition. We define or to be λA B : prop ⇒ ∀p : prop, (A → p) → (B → p) → p of type prop → prop → prop.

Notation. We use ∨ as an infix operator with priority 785 and which associates to the left corresponding to applying term or.

Definition. We define iff to be λA B : prop ⇒ and (A → B) (B → A) of type prop → prop → prop.

Notation. We use ↔ as an infix operator with priority 805 and no associativity corresponding to applying term iff.

Beginning of Section Eq

Variable A : SType

Definition. We define eq to be λx y : A ⇒ ∀Q : A → A → prop, Q x y → Q y x of type A → A → prop.

Definition. We define neq to be λx y : A ⇒ ¬ eq x y of type A → A → prop.

End of Section Eq

Notation. We use = as an infix operator with priority 502 and no associativity corresponding to applying term eq.

Notation. We use ≠ as an infix operator with priority 502 and no associativity corresponding to applying term neq.

Beginning of Section FE

Variable A B : SType

Axiom. (func_ext) We take the following as an axiom:

∀f g : A → B, (∀x : A, f x = g x) → f = g

End of Section FE

Beginning of Section Ex

Variable A : SType

Definition. We define ex to be λQ : A → prop ⇒ ∀P : prop, (∀x : A, Q x → P) → P of type (A → prop) → prop.

End of Section Ex

Notation. We use ∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex.

Axiom. (prop_ext) We take the following as an axiom:

∀p q : prop, iff p q → p = q

Object. The name In is a term of type set → set → prop.

Notation. We use ∈ as an infix operator with priority 500 and no associativity corresponding to applying term In. Furthermore, we may write ∀ x ∈ A, B to mean ∀ x : set, x ∈ A → B.

Definition. We define Subq to be λA B ⇒ ∀x ∈ A, x ∈ B of type set → set → prop.

Notation. We use ⊆ as an infix operator with priority 500 and no associativity corresponding to applying term Subq. Furthermore, we may write ∀ x ⊆ A, B to mean ∀ x : set, x ⊆ A → B.

Axiom. (set_ext) We take the following as an axiom:

∀X Y : set, X ⊆ Y → Y ⊆ X → X = Y

Axiom. (In_ind) We take the following as an axiom:

∀P : set → prop, (∀X : set, (∀x ∈ X, P x) → P X) → ∀X : set, P X

Notation. We use ∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex and handling ∈ or ⊆ ascriptions using and.

Object. The name Empty is a term of type set.

Axiom. (EmptyAx) We take the following as an axiom:

¬ ∃x : set, x ∈ Empty

Object. The name ⋃ is a term of type set → set.

Axiom. (UnionEq) We take the following as an axiom:

∀X x, x ∈ ⋃ X ↔ ∃Y, x ∈ Y ∧ Y ∈ X

Object. The name 𝒫 is a term of type set → set.

Axiom. (PowerEq) We take the following as an axiom:

∀X Y : set, Y ∈ 𝒫 X ↔ Y ⊆ X

Object. The name Repl is a term of type set → (set → set) → set.

Notation. {B| x ∈ A} is notation for Repl A (λ x . B).

Axiom. (ReplEq) We take the following as an axiom:

∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} ↔ ∃x ∈ A, y = F x

Definition. We define TransSet to be λU : set ⇒ ∀x ∈ U, x ⊆ U of type set → prop.

Definition. We define Union_closed to be λU : set ⇒ ∀X : set, X ∈ U → ⋃ X ∈ U of type set → prop.

Definition. We define Power_closed to be λU : set ⇒ ∀X : set, X ∈ U → 𝒫 X ∈ U of type set → prop.

Definition. We define Repl_closed to be λU : set ⇒ ∀X : set, X ∈ U → ∀F : set → set, (∀x : set, x ∈ X → F x ∈ U) → {F x|x ∈ X} ∈ U of type set → prop.

Definition. We define ZF_closed to be λU : set ⇒ Union_closed U ∧ Power_closed U ∧ Repl_closed U of type set → prop.

Object. The name UnivOf is a term of type set → set.

Axiom. (UnivOf_In) We take the following as an axiom:

∀N : set, N ∈ UnivOf N

Axiom. (UnivOf_TransSet) We take the following as an axiom:

∀N : set, TransSet (UnivOf N)

Axiom. (UnivOf_ZF_closed) We take the following as an axiom:

∀N : set, ZF_closed (UnivOf N)

Axiom. (UnivOf_Min) We take the following as an axiom:

∀N U : set, N ∈ U → TransSet U → ZF_closed U → UnivOf N ⊆ U

Theorem. (FalseE) The following is provable:

False → ∀p : prop, p

Proof:

An exact proof term for the current goal is (λH ⇒ H).

∎

Theorem. (TrueI) The following is provable:

True

Proof:

An exact proof term for the current goal is (λp H ⇒ H).

∎

Theorem. (andI) The following is provable:

∀A B : prop, A → B → A ∧ B

Proof:

An exact proof term for the current goal is (λA B a b P H ⇒ H a b).

∎

Try to prove it yourself. Main Goal

Theorem. (andEL) The following is provable:

∀A B : prop, A ∧ B → A

Proof:

An exact proof term for the current goal is (λA B H ⇒ H A (λa b ⇒ a)).

∎

Try to prove it yourself. Main Goal

Theorem. (andER) The following is provable:

∀A B : prop, A ∧ B → B

Proof:

An exact proof term for the current goal is (λA B H ⇒ H B (λa b ⇒ b)).

∎

Try to prove it yourself. Main Goal

Theorem. (orIL) The following is provable:

∀A B : prop, A → A ∨ B

Proof:

An exact proof term for the current goal is (λA B a P H1 H2 ⇒ H1 a).

∎

Try to prove it yourself. Main Goal

Theorem. (orIR) The following is provable:

∀A B : prop, B → A ∨ B

Proof:

An exact proof term for the current goal is (λA B b P H1 H2 ⇒ H2 b).

∎

Try to prove it yourself. Main Goal

Beginning of Section PropN

Variable P1 P2 P3 : prop

Theorem. (and3I) The following is provable:

P1 → P2 → P3 → P1 ∧ P2 ∧ P3

Proof:

An exact proof term for the current goal is (λH1 H2 H3 ⇒ andI (P1 ∧ P2) P3 (andI P1 P2 H1 H2) H3).

∎

Try to prove it yourself. Main Goal

Theorem. (and3E) The following is provable:

P1 ∧ P2 ∧ P3 → (∀p : prop, (P1 → P2 → P3 → p) → p)

Proof:

An exact proof term for the current goal is (λu p H ⇒ u p (λu u3 ⇒ u p (λu1 u2 ⇒ H u1 u2 u3))).

∎

Try to prove it yourself. Main Goal

Theorem. (or3I1) The following is provable:

P1 → P1 ∨ P2 ∨ P3

Proof:

An exact proof term for the current goal is (λu ⇒ orIL (P1 ∨ P2) P3 (orIL P1 P2 u)).

∎

Try to prove it yourself. Main Goal

Theorem. (or3I2) The following is provable:

P2 → P1 ∨ P2 ∨ P3

Proof:

An exact proof term for the current goal is (λu ⇒ orIL (P1 ∨ P2) P3 (orIR P1 P2 u)).

∎

Try to prove it yourself. Main Goal

Theorem. (or3I3) The following is provable:

P3 → P1 ∨ P2 ∨ P3

Proof:

An exact proof term for the current goal is (orIR (P1 ∨ P2) P3).

∎

Try to prove it yourself. Main Goal

Theorem. (or3E) The following is provable:

P1 ∨ P2 ∨ P3 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → p)

Proof:

An exact proof term for the current goal is (λu p H1 H2 H3 ⇒ u p (λu ⇒ u p H1 H2) H3).

∎

Try to prove it yourself. Main Goal

Variable P4 : prop

Theorem. (and4I) The following is provable:

P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4

Proof:

An exact proof term for the current goal is (λH1 H2 H3 H4 ⇒ andI (P1 ∧ P2 ∧ P3) P4 (and3I H1 H2 H3) H4).

∎

Try to prove it yourself. Main Goal

Variable P5 : prop

Theorem. (and5I) The following is provable:

P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5

Proof:

An exact proof term for the current goal is (λH1 H2 H3 H4 H5 ⇒ andI (P1 ∧ P2 ∧ P3 ∧ P4) P5 (and4I H1 H2 H3 H4) H5).

∎

Try to prove it yourself. Main Goal

End of Section PropN

Theorem. (not_or_and_demorgan) The following is provable:

∀A B : prop, ¬ (A ∨ B) → ¬ A ∧ ¬ B

Proof:

Let A and B be given.

Assume u: ¬ (A ∨ B).

Apply andI to the current goal.

We will prove ¬ A.

Assume a: A.

An exact proof term for the current goal is (u (orIL A B a)).

We will prove ¬ B.

Assume b: B.

An exact proof term for the current goal is (u (orIR A B b)).

∎

Try to prove it yourself. Main Goal

Theorem. (not_ex_all_demorgan_i) The following is provable:

∀P : set → prop, (¬ ∃x, P x) → ∀x, ¬ P x

Proof:

Let P be given.

Assume H1.

Let x be given.

Assume H2.

Apply H1 to the current goal.

We use x to witness the existential quantifier.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (iffI) The following is provable:

∀A B : prop, (A → B) → (B → A) → (A ↔ B)

Proof:

An exact proof term for the current goal is (λA B ⇒ andI (A → B) (B → A)).

∎

Try to prove it yourself. Main Goal

Theorem. (iffEL) The following is provable:

∀A B : prop, (A ↔ B) → A → B

Proof:

An exact proof term for the current goal is (λA B ⇒ andEL (A → B) (B → A)).

∎

Try to prove it yourself. Main Goal

Theorem. (iffER) The following is provable:

∀A B : prop, (A ↔ B) → B → A

Proof:

An exact proof term for the current goal is (λA B ⇒ andER (A → B) (B → A)).

∎

Try to prove it yourself. Main Goal

Theorem. (iff_refl) The following is provable:

∀A : prop, A ↔ A

Proof:

An exact proof term for the current goal is (λA : prop ⇒ andI (A → A) (A → A) (λH : A ⇒ H) (λH : A ⇒ H)).

∎

Try to prove it yourself. Main Goal

Theorem. (iff_sym) The following is provable:

∀A B : prop, (A ↔ B) → (B ↔ A)

Proof:

Let A and B be given.

Assume H1: (A → B) ∧ (B → A).

Apply H1 to the current goal.

Assume H2: A → B.

Assume H3: B → A.

An exact proof term for the current goal is iffI B A H3 H2.

∎

Try to prove it yourself. Main Goal

Theorem. (iff_trans) The following is provable:

∀A B C : prop, (A ↔ B) → (B ↔ C) → (A ↔ C)

Proof:

Let A, B and C be given.

Assume H1: A ↔ B.

Assume H2: B ↔ C.

Apply H1 to the current goal.

Assume H3: A → B.

Assume H4: B → A.

Apply H2 to the current goal.

Assume H5: B → C.

Assume H6: C → B.

An exact proof term for the current goal is (iffI A C (λH ⇒ H5 (H3 H)) (λH ⇒ H4 (H6 H))).

∎

Try to prove it yourself. Main Goal

Theorem. (eq_i_tra) The following is provable:

∀x y z, x = y → y = z → x = z

Proof:

Let x, y and z be given.

Assume H1 H2.

rewrite the current goal using H2 (from right to left).

An exact proof term for the current goal is H1.

∎

Try to prove it yourself. Main Goal

Theorem. (f_eq_i) The following is provable:

∀f : set → set, ∀x y, x = y → f x = f y

Proof:

Let f, x and y be given.

Assume H1.

rewrite the current goal using H1 (from left to right).

Use reflexivity.

∎

Try to prove it yourself. Main Goal

Theorem. (neq_i_sym) The following is provable:

∀x y, x ≠ y → y ≠ x

Proof:

Let x and y be given.

Assume H1 H2.

Apply H1 to the current goal.

Use symmetry.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Definition. We define nIn to be λx X ⇒ ¬ In x X of type set → set → prop.

Notation. We use ∉ as an infix operator with priority 502 and no associativity corresponding to applying term nIn.

Theorem. (Eps_i_ex) The following is provable:

∀P : set → prop, (∃x, P x) → P (Eps_i P)

Proof:

Let P be given.

Assume H1.

Apply H1 to the current goal.

Let x be given.

Assume H2.

An exact proof term for the current goal is Eps_i_ax P x H2.

∎

Try to prove it yourself. Main Goal

Theorem. (pred_ext) The following is provable:

∀P Q : set → prop, (∀x, P x ↔ Q x) → P = Q

Proof:

Let P and Q be given.

Assume H1.

Apply func_ext set prop to the current goal.

Let x be given.

Apply prop_ext to the current goal.

We will prove P x ↔ Q x.

An exact proof term for the current goal is H1 x.

∎

Try to prove it yourself. Main Goal

Theorem. (prop_ext_2) The following is provable:

∀p q : prop, (p → q) → (q → p) → p = q

Proof:

Let p and q be given.

Assume H1 H2.

Apply prop_ext to the current goal.

Apply iffI to the current goal.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (Subq_ref) The following is provable:

∀X : set, X ⊆ X

Proof:

An exact proof term for the current goal is (λ(X x : set)(H : x ∈ X) ⇒ H).

∎

Try to prove it yourself. Main Goal

Theorem. (Subq_tra) The following is provable:

∀X Y Z : set, X ⊆ Y → Y ⊆ Z → X ⊆ Z

Proof:

An exact proof term for the current goal is (λ(X Y Z : set)(H1 : X ⊆ Y)(H2 : Y ⊆ Z)(x : set)(H : x ∈ X) ⇒ (H2 x (H1 x H))).

∎

Try to prove it yourself. Main Goal

Theorem. (Subq_contra) The following is provable:

∀X Y z : set, X ⊆ Y → z ∉ Y → z ∉ X

Proof:

An exact proof term for the current goal is (λX Y z H1 H2 H3 ⇒ H2 (H1 z H3)).

∎

Try to prove it yourself. Main Goal

Theorem. (EmptyE) The following is provable:

∀x : set, x ∉ Empty

Proof:

Let x be given.

Assume H.

Apply EmptyAx to the current goal.

We use x to witness the existential quantifier.

An exact proof term for the current goal is H.

∎

Try to prove it yourself. Main Goal

Theorem. (Subq_Empty) The following is provable:

∀X : set, Empty ⊆ X

Proof:

An exact proof term for the current goal is (λ(X x : set)(H : x ∈ Empty) ⇒ EmptyE x H (x ∈ X)).

∎

Try to prove it yourself. Main Goal

Theorem. (Empty_Subq_eq) The following is provable:

∀X : set, X ⊆ Empty → X = Empty

Proof:

Let X be given.

Assume H1: X ⊆ Empty.

Apply set_ext to the current goal.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is (Subq_Empty X).

∎

Try to prove it yourself. Main Goal

Theorem. (Empty_eq) The following is provable:

∀X : set, (∀x, x ∉ X) → X = Empty

Proof:

Let X be given.

Assume H1: ∀x, x ∉ X.

Apply Empty_Subq_eq to the current goal.

Let x be given.

Assume H2: x ∈ X.

We will prove False.

An exact proof term for the current goal is (H1 x H2).

∎

Try to prove it yourself. Main Goal

Theorem. (UnionI) The following is provable:

∀X x Y : set, x ∈ Y → Y ∈ X → x ∈ ⋃ X

Proof:

Let X, x and Y be given.

Assume H1: x ∈ Y.

Assume H2: Y ∈ X.

Apply UnionEq X x to the current goal.

Assume _ H3.

Apply H3 to the current goal.

We will prove ∃Y : set, x ∈ Y ∧ Y ∈ X.

We use Y to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (UnionE) The following is provable:

∀X x : set, x ∈ ⋃ X → ∃Y : set, x ∈ Y ∧ Y ∈ X

Proof:

An exact proof term for the current goal is (λX x : set ⇒ iffEL (x ∈ ⋃ X) (∃Y : set, x ∈ Y ∧ Y ∈ X) (UnionEq X x)).

∎

Try to prove it yourself. Main Goal

Theorem. (UnionE_impred) The following is provable:

∀X x : set, x ∈ ⋃ X → ∀p : prop, (∀Y : set, x ∈ Y → Y ∈ X → p) → p

Proof:

Let X and x be given.

Assume H1.

Let p be given.

Assume Hp.

Apply UnionE X x H1 to the current goal.

Let x be given.

Assume H2.

Apply H2 to the current goal.

An exact proof term for the current goal is Hp x.

∎

Try to prove it yourself. Main Goal

Theorem. (PowerI) The following is provable:

∀X Y : set, Y ⊆ X → Y ∈ 𝒫 X

Proof:

Let X and Y be given.

Apply PowerEq X Y to the current goal.

An exact proof term for the current goal is (λ_ H ⇒ H).

∎

Try to prove it yourself. Main Goal

Theorem. (PowerE) The following is provable:

∀X Y : set, Y ∈ 𝒫 X → Y ⊆ X

Proof:

Let X and Y be given.

Apply PowerEq X Y to the current goal.

An exact proof term for the current goal is (λH _ ⇒ H).

∎

Try to prove it yourself. Main Goal

Theorem. (Empty_In_Power) The following is provable:

∀X : set, Empty ∈ 𝒫 X

Proof:

An exact proof term for the current goal is (λX : set ⇒ PowerI X Empty (Subq_Empty X)).

∎

Try to prove it yourself. Main Goal

Theorem. (Self_In_Power) The following is provable:

∀X : set, X ∈ 𝒫 X

Proof:

An exact proof term for the current goal is (λX : set ⇒ PowerI X X (Subq_ref X)).

∎

Try to prove it yourself. Main Goal

Theorem. (xm) The following is provable:

∀P : prop, P ∨ ¬ P

Proof:

Let P of type prop be given.

Set p1 to be the term λx : set ⇒ x = Empty ∨ P.

Set p2 to be the term λx : set ⇒ x ≠ Empty ∨ P.

We prove the intermediate claim L1: p1 Empty.

We will prove (Empty = Empty ∨ P).

Apply orIL to the current goal.

An exact proof term for the current goal is (λq H ⇒ H).

We prove the intermediate claim L2: (Eps_i p1) = Empty ∨ P.

An exact proof term for the current goal is (Eps_i_ax p1 Empty L1).

We prove the intermediate claim L3: p2 (𝒫 Empty).

We will prove ¬ (𝒫 Empty = Empty) ∨ P.

Apply orIL to the current goal.

Assume H1: 𝒫 Empty = Empty.

Apply EmptyE Empty to the current goal.

We will prove Empty ∈ Empty.

rewrite the current goal using H1 (from right to left) at position 2.

Apply Empty_In_Power to the current goal.

We prove the intermediate claim L4: Eps_i p2 ≠ Empty ∨ P.

An exact proof term for the current goal is (Eps_i_ax p2 (𝒫 Empty) L3).

Apply L2 to the current goal.

Assume H1: Eps_i p1 = Empty.

Apply L4 to the current goal.

Assume H2: Eps_i p2 ≠ Empty.

We will prove P ∨ ¬ P.

Apply orIR to the current goal.

We will prove ¬ P.

Assume H3: P.

We prove the intermediate claim L5: p1 = p2.

Apply pred_ext to the current goal.

Let x be given.

Apply iffI to the current goal.

Assume H4.

We will prove (¬ (x = Empty) ∨ P).

Apply orIR to the current goal.

We will prove P.

An exact proof term for the current goal is H3.

Assume H4.

We will prove (x = Empty ∨ P).

Apply orIR to the current goal.

We will prove P.

An exact proof term for the current goal is H3.

Apply H2 to the current goal.

rewrite the current goal using L5 (from right to left).

An exact proof term for the current goal is H1.

Assume H2: P.

We will prove P ∨ ¬ P.

Apply orIL to the current goal.

We will prove P.

An exact proof term for the current goal is H2.

Assume H1: P.

We will prove P ∨ ¬ P.

Apply orIL to the current goal.

We will prove P.

An exact proof term for the current goal is H1.

∎

Theorem. (dneg) The following is provable:

∀P : prop, ¬ ¬ P → P

Proof:

Let P be given.

Assume H1.

Apply xm P to the current goal.

An exact proof term for the current goal is (λH ⇒ H).

Assume H2: ¬ P.

We will prove False.

An exact proof term for the current goal is H1 H2.

∎

Theorem. (not_all_ex_demorgan_i) The following is provable:

∀P : set → prop, ¬ (∀x, P x) → ∃x, ¬ P x

Proof:

Let P be given.

Assume u: ¬ ∀x, P x.

Apply dneg to the current goal.

Assume v: ¬ ∃x, ¬ P x.

Apply u to the current goal.

Let x be given.

Apply dneg to the current goal.

Assume w: ¬ P x.

An exact proof term for the current goal is (not_ex_all_demorgan_i (λx ⇒ ¬ P x) v x w).

∎

Try to prove it yourself. Main Goal

Theorem. (eq_or_nand) The following is provable:

or = (λx y : prop ⇒ ¬ (¬ x ∧ ¬ y))

Proof:

Apply func_ext prop (prop → prop) to the current goal.

Let x be given.

Apply func_ext prop prop to the current goal.

Let y be given.

Apply prop_ext_2 to the current goal.

Assume H1: x ∨ y.

Assume H2: ¬ x ∧ ¬ y.

Apply H2 to the current goal.

Assume H3 H4.

An exact proof term for the current goal is (H1 False H3 H4).

Assume H1: ¬ (¬ x ∧ ¬ y).

Apply (xm x) to the current goal.

Assume H2: x.

Apply orIL to the current goal.

An exact proof term for the current goal is H2.

Assume H2: ¬ x.

Apply (xm y) to the current goal.

Assume H3: y.

Apply orIR to the current goal.

An exact proof term for the current goal is H3.

Assume H3: ¬ y.

Apply H1 to the current goal.

An exact proof term for the current goal is (andI (¬ x) (¬ y) H2 H3).

∎

Try to prove it yourself. Main Goal

Definition. We define exactly1of2 to be λA B : prop ⇒ A ∧ ¬ B ∨ ¬ A ∧ B of type prop → prop → prop.

Theorem. (exactly1of2_I1) The following is provable:

∀A B : prop, A → ¬ B → exactly1of2 A B

Proof:

Let A and B be given.

Assume HA: A.

Assume HB: ¬ B.

We will prove A ∧ ¬ B ∨ ¬ A ∧ B.

Apply orIL to the current goal.

We will prove A ∧ ¬ B.

An exact proof term for the current goal is (andI A (¬ B) HA HB).

∎

Try to prove it yourself. Main Goal

Theorem. (exactly1of2_I2) The following is provable:

∀A B : prop, ¬ A → B → exactly1of2 A B

Proof:

Let A and B be given.

Assume HA: ¬ A.

Assume HB: B.

We will prove A ∧ ¬ B ∨ ¬ A ∧ B.

Apply orIR to the current goal.

We will prove ¬ A ∧ B.

An exact proof term for the current goal is (andI (¬ A) B HA HB).

∎

Try to prove it yourself. Main Goal

Theorem. (exactly1of2_E) The following is provable:

∀A B : prop, exactly1of2 A B → ∀p : prop, (A → ¬ B → p) → (¬ A → B → p) → p

Proof:

Let A and B be given.

Assume H1: exactly1of2 A B.

Let p be given.

Assume H2: A → ¬ B → p.

Assume H3: ¬ A → B → p.

Apply (H1 p) to the current goal.

An exact proof term for the current goal is (λH4 : A ∧ ¬ B ⇒ H4 p H2).

An exact proof term for the current goal is (λH4 : ¬ A ∧ B ⇒ H4 p H3).

∎

Try to prove it yourself. Main Goal

Theorem. (exactly1of2_or) The following is provable:

∀A B : prop, exactly1of2 A B → A ∨ B

Proof:

Let A and B be given.

Assume H1: exactly1of2 A B.

Apply (exactly1of2_E A B H1 (A ∨ B)) to the current goal.

An exact proof term for the current goal is (λ(HA : A)(_ : ¬ B) ⇒ orIL A B HA).

An exact proof term for the current goal is (λ(_ : ¬ A)(HB : B) ⇒ orIR A B HB).

∎

Try to prove it yourself. Main Goal

Theorem. (ReplI) The following is provable:

∀A : set, ∀F : set → set, ∀x : set, x ∈ A → F x ∈ {F x|x ∈ A}

Proof:

Let A, F and x be given.

Assume H1.

Apply ReplEq A F (F x) to the current goal.

Assume _ H2.

Apply H2 to the current goal.

We will prove ∃x' ∈ A, F x = F x'.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is (λq H ⇒ H).

∎

Try to prove it yourself. Main Goal

Theorem. (ReplE) The following is provable:

∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} → ∃x ∈ A, y = F x

Proof:

Let A, F and y be given.

Apply ReplEq A F y to the current goal.

An exact proof term for the current goal is (λH _ ⇒ H).

∎

Try to prove it yourself. Main Goal

Theorem. (ReplE_impred) The following is provable:

∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} → ∀p : prop, (∀x : set, x ∈ A → y = F x → p) → p

Proof:

Let A, F and y be given.

Assume H1.

Apply ReplE A F y H1 to the current goal.

Let x be given.

Assume H2.

Apply H2 to the current goal.

Assume H3 H4.

Let p be given.

Assume Hp.

An exact proof term for the current goal is Hp x H3 H4.

∎

Try to prove it yourself. Main Goal

Theorem. (ReplE') The following is provable:

∀X, ∀f : set → set, ∀p : set → prop, (∀x ∈ X, p (f x)) → ∀y ∈ {f x|x ∈ X}, p y

Proof:

Let X, f and p be given.

Assume H1.

Let y be given.

Assume Hy.

Apply ReplE_impred X f y Hy to the current goal.

Let x be given.

Assume Hx: x ∈ X.

Assume Hx2: y = f x.

We will prove p y.

rewrite the current goal using Hx2 (from left to right).

An exact proof term for the current goal is H1 x Hx.

∎

Try to prove it yourself. Main Goal

Theorem. (Repl_Empty) The following is provable:

∀F : set → set, {F x|x ∈ Empty} = Empty

Proof:

Let F be given.

Apply (Empty_eq {F x|x ∈ Empty}) to the current goal.

Let y be given.

Assume H1: y ∈ {F x|x ∈ Empty}.

Apply (ReplE_impred Empty F y H1) to the current goal.

Let x be given.

Assume H2: x ∈ Empty.

Assume _.

An exact proof term for the current goal is (EmptyE x H2).

∎

Try to prove it yourself. Main Goal

Theorem. (ReplEq_ext_sub) The following is provable:

∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → {F x|x ∈ X} ⊆ {G x|x ∈ X}

Proof:

Let X, F and G be given.

Assume H1: ∀x ∈ X, F x = G x.

Let y be given.

Assume Hy: y ∈ {F x|x ∈ X}.

Apply ReplE_impred X F y Hy to the current goal.

Let x be given.

Assume Hx: x ∈ X.

Assume H2: y = F x.

We will prove y ∈ {G x|x ∈ X}.

rewrite the current goal using H2 (from left to right).

We will prove F x ∈ {G x|x ∈ X}.

rewrite the current goal using H1 x Hx (from left to right).

We will prove G x ∈ {G x|x ∈ X}.

Apply ReplI to the current goal.

An exact proof term for the current goal is Hx.

∎

Try to prove it yourself. Main Goal

Theorem. (ReplEq_ext) The following is provable:

∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → {F x|x ∈ X} = {G x|x ∈ X}

Proof:

Let X, F and G be given.

Assume H1: ∀x ∈ X, F x = G x.

Apply set_ext to the current goal.

An exact proof term for the current goal is ReplEq_ext_sub X F G H1.

Apply ReplEq_ext_sub X G F to the current goal.

Let x be given.

Assume Hx.

Use symmetry.

An exact proof term for the current goal is H1 x Hx.

∎

Try to prove it yourself. Main Goal

Theorem. (Repl_inv_eq) The following is provable:

∀P : set → prop, ∀f g : set → set, (∀x, P x → g (f x) = x) → ∀X, (∀x ∈ X, P x) → {g y|y ∈ {f x|x ∈ X}} = X

Proof:

Let P, f and g be given.

Assume H1.

Let X be given.

Assume HX.

Apply set_ext to the current goal.

Let w be given.

Assume Hw: w ∈ {g y|y ∈ {f x|x ∈ X}}.

Apply ReplE_impred {f x|x ∈ X} g w Hw to the current goal.

Let y be given.

Assume Hy: y ∈ {f x|x ∈ X}.

Assume Hwy: w = g y.

Apply ReplE_impred X f y Hy to the current goal.

Let x be given.

Assume Hx: x ∈ X.

Assume Hyx: y = f x.

We will prove w ∈ X.

rewrite the current goal using Hwy (from left to right).

rewrite the current goal using Hyx (from left to right).

We will prove g (f x) ∈ X.

rewrite the current goal using H1 x (HX x Hx) (from left to right).

An exact proof term for the current goal is Hx.

Let x be given.

Assume Hx: x ∈ X.

rewrite the current goal using H1 x (HX x Hx) (from right to left).

We will prove g (f x) ∈ {g y|y ∈ {f x|x ∈ X}}.

Apply ReplI to the current goal.

We will prove f x ∈ {f x|x ∈ X}.

Apply ReplI to the current goal.

An exact proof term for the current goal is Hx.

∎

Try to prove it yourself. Main Goal

Theorem. (Repl_invol_eq) The following is provable:

∀P : set → prop, ∀f : set → set, (∀x, P x → f (f x) = x) → ∀X, (∀x ∈ X, P x) → {f y|y ∈ {f x|x ∈ X}} = X

Proof:

Let P and f be given.

Assume H1.

An exact proof term for the current goal is Repl_inv_eq P f f H1.

∎

Try to prove it yourself. Main Goal

Definition. We define If_i to be (λp x y ⇒ Eps_i (λz : set ⇒ p ∧ z = x ∨ ¬ p ∧ z = y)) of type prop → set → set → set.

Notation. if cond then T else E is notation corresponding to If_i type cond T E where type is the inferred type of T.

Theorem. (If_i_correct) The following is provable:

∀p : prop, ∀x y : set, p ∧ (if p then x else y) = x ∨ ¬ p ∧ (if p then x else y) = y

Proof:

Let p, x and y be given.

Apply (xm p) to the current goal.

Assume H1: p.

We prove the intermediate claim L1: p ∧ x = x ∨ ¬ p ∧ x = y.

Apply orIL to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is H1.

Use reflexivity.

An exact proof term for the current goal is (Eps_i_ax (λz : set ⇒ p ∧ z = x ∨ ¬ p ∧ z = y) x L1).

Assume H1: ¬ p.

We prove the intermediate claim L1: p ∧ y = x ∨ ¬ p ∧ y = y.

Apply orIR to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is H1.

Use reflexivity.

An exact proof term for the current goal is (Eps_i_ax (λz : set ⇒ p ∧ z = x ∨ ¬ p ∧ z = y) y L1).

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Theorem. (If_i_0) The following is provable:

∀p : prop, ∀x y : set, ¬ p → (if p then x else y) = y

Proof:

Let p, x and y be given.

Assume H1: ¬ p.

Apply (If_i_correct p x y) to the current goal.

Assume H2: p ∧ (if p then x else y) = x.

An exact proof term for the current goal is (H1 (andEL p ((if p then x else y) = x) H2) ((if p then x else y) = y)).

Assume H2: ¬ p ∧ (if p then x else y) = y.

An exact proof term for the current goal is (andER (¬ p) ((if p then x else y) = y) H2).

∎

Try to prove it yourself. Main Goal

Theorem. (If_i_1) The following is provable:

∀p : prop, ∀x y : set, p → (if p then x else y) = x

Proof:

Let p, x and y be given.

Assume H1: p.

Apply (If_i_correct p x y) to the current goal.

Assume H2: p ∧ (if p then x else y) = x.

An exact proof term for the current goal is (andER p ((if p then x else y) = x) H2).

Assume H2: ¬ p ∧ (if p then x else y) = y.

An exact proof term for the current goal is (andEL (¬ p) ((if p then x else y) = y) H2 H1 ((if p then x else y) = x)).

∎

Try to prove it yourself. Main Goal

Theorem. (If_i_or) The following is provable:

∀p : prop, ∀x y : set, (if p then x else y) = x ∨ (if p then x else y) = y

Proof:

Let p, x and y be given.

Apply (xm p) to the current goal.

Assume H1: p.

Apply orIL to the current goal.

An exact proof term for the current goal is (If_i_1 p x y H1).

Assume H1: ¬ p.

Apply orIR to the current goal.

An exact proof term for the current goal is (If_i_0 p x y H1).

∎

Try to prove it yourself. Main Goal

Definition. We define UPair to be λy z ⇒ {if Empty ∈ X then y else z|X ∈ 𝒫 (𝒫 Empty)} of type set → set → set.

Notation. {x,y} is notation for UPair x y.

Theorem. (UPairE) The following is provable:

∀x y z : set, x ∈ {y,z} → x = y ∨ x = z

Proof:

Let x, y and z be given.

Assume H1: x ∈ {y,z}.

Apply (ReplE (𝒫 (𝒫 Empty)) (λX ⇒ if Empty ∈ X then y else z) x H1) to the current goal.

Let X be given.

Assume H2: X ∈ 𝒫 (𝒫 Empty) ∧ x = if Empty ∈ X then y else z.

We prove the intermediate claim L1: x = if Empty ∈ X then y else z.

An exact proof term for the current goal is (andER (X ∈ 𝒫 (𝒫 Empty)) (x = if Empty ∈ X then y else z) H2).

Apply (If_i_or (Empty ∈ X) y z) to the current goal.

Assume H3: (if Empty ∈ X then y else z) = y.

Apply orIL to the current goal.

We will prove x = y.

rewrite the current goal using H3 (from right to left).

An exact proof term for the current goal is L1.

Assume H3: (if Empty ∈ X then y else z) = z.

Apply orIR to the current goal.

We will prove x = z.

rewrite the current goal using H3 (from right to left).

An exact proof term for the current goal is L1.

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (UPairI1) The following is provable:

∀y z : set, y ∈ {y,z}

Proof:

Let y and z be given.

We will prove y ∈ {y,z}.

rewrite the current goal using (If_i_1 (Empty ∈ 𝒫 Empty) y z (Empty_In_Power Empty)) (from right to left) at position 1.

We will prove (if Empty ∈ 𝒫 Empty then y else z) ∈ {y,z}.

We will prove (if Empty ∈ 𝒫 Empty then y else z) ∈ {if Empty ∈ X then y else z|X ∈ 𝒫 (𝒫 Empty)}.

Apply (ReplI (𝒫 (𝒫 Empty)) (λX : set ⇒ if (Empty ∈ X) then y else z) (𝒫 Empty)) to the current goal.

We will prove 𝒫 Empty ∈ 𝒫 (𝒫 Empty).

An exact proof term for the current goal is (Self_In_Power (𝒫 Empty)).

∎

Try to prove it yourself. Main Goal

Theorem. (UPairI2) The following is provable:

∀y z : set, z ∈ {y,z}

Proof:

Let y and z be given.

We will prove z ∈ {y,z}.

rewrite the current goal using (If_i_0 (Empty ∈ Empty) y z (EmptyE Empty)) (from right to left) at position 1.

We will prove (if Empty ∈ Empty then y else z) ∈ {y,z}.

We will prove (if Empty ∈ Empty then y else z) ∈ {if Empty ∈ X then y else z|X ∈ 𝒫 (𝒫 Empty)}.

Apply (ReplI (𝒫 (𝒫 Empty)) (λX : set ⇒ if (Empty ∈ X) then y else z) Empty) to the current goal.

We will prove Empty ∈ 𝒫 (𝒫 Empty).

An exact proof term for the current goal is (Empty_In_Power (𝒫 Empty)).

∎

Try to prove it yourself. Main Goal

Definition. We define Sing to be λx ⇒ {x,x} of type set → set.

Notation. {x} is notation for Sing x.

Theorem. (SingI) The following is provable:

∀x : set, x ∈ {x}

Proof:

An exact proof term for the current goal is (λx : set ⇒ UPairI1 x x).

∎

Try to prove it yourself. Main Goal

Theorem. (SingE) The following is provable:

∀x y : set, y ∈ {x} → y = x

Proof:

An exact proof term for the current goal is (λx y H ⇒ UPairE y x x H (y = x) (λH ⇒ H) (λH ⇒ H)).

∎

Try to prove it yourself. Main Goal

Definition. We define binunion to be λX Y ⇒ ⋃ {X,Y} of type set → set → set.

Notation. We use ∪ as an infix operator with priority 345 and which associates to the left corresponding to applying term binunion.

Theorem. (binunionI1) The following is provable:

∀X Y z : set, z ∈ X → z ∈ X ∪ Y

Proof:

Let X, Y and z be given.

Assume H1: z ∈ X.

We will prove z ∈ X ∪ Y.

We will prove z ∈ ⋃ {X,Y}.

Apply (UnionI {X,Y} z X) to the current goal.

We will prove z ∈ X.

An exact proof term for the current goal is H1.

We will prove X ∈ {X,Y}.

An exact proof term for the current goal is (UPairI1 X Y).

∎

Try to prove it yourself. Main Goal

Theorem. (binunionI2) The following is provable:

∀X Y z : set, z ∈ Y → z ∈ X ∪ Y

Proof:

Let X, Y and z be given.

Assume H1: z ∈ Y.

We will prove z ∈ X ∪ Y.

We will prove z ∈ ⋃ {X,Y}.

Apply (UnionI {X,Y} z Y) to the current goal.

We will prove z ∈ Y.

An exact proof term for the current goal is H1.

We will prove Y ∈ {X,Y}.

An exact proof term for the current goal is (UPairI2 X Y).

∎

Try to prove it yourself. Main Goal

Theorem. (binunionE) The following is provable:

∀X Y z : set, z ∈ X ∪ Y → z ∈ X ∨ z ∈ Y

Proof:

Let X, Y and z be given.

Assume H1: z ∈ X ∪ Y.

We will prove z ∈ X ∨ z ∈ Y.

Apply (UnionE_impred {X,Y} z H1) to the current goal.

Let Z be given.

Assume H2: z ∈ Z.

Assume H3: Z ∈ {X,Y}.

Apply (UPairE Z X Y H3) to the current goal.

Assume H4: Z = X.

Apply orIL to the current goal.

We will prove z ∈ X.

rewrite the current goal using H4 (from right to left).

We will prove z ∈ Z.

An exact proof term for the current goal is H2.

Assume H4: Z = Y.

Apply orIR to the current goal.

We will prove z ∈ Y.

rewrite the current goal using H4 (from right to left).

We will prove z ∈ Z.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (binunionE') The following is provable:

∀X Y z, ∀p : prop, (z ∈ X → p) → (z ∈ Y → p) → (z ∈ X ∪ Y → p)

Proof:

Let X, Y, z and p be given.

Assume H1 H2 Hz.

Apply binunionE X Y z Hz to the current goal.

Assume H3: z ∈ X.

An exact proof term for the current goal is H1 H3.

Assume H3: z ∈ Y.

An exact proof term for the current goal is H2 H3.

∎

Try to prove it yourself. Main Goal

Theorem. (binunion_asso) The following is provable:

∀X Y Z : set, X ∪ (Y ∪ Z) = (X ∪ Y) ∪ Z

Proof:

Let X, Y and Z be given.

Apply set_ext to the current goal.

Let w be given.

Assume H1: w ∈ X ∪ (Y ∪ Z).

We will prove w ∈ (X ∪ Y) ∪ Z.

Apply (binunionE X (Y ∪ Z) w H1) to the current goal.

Assume H2: w ∈ X.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is H2.

Assume H2: w ∈ Y ∪ Z.

Apply (binunionE Y Z w H2) to the current goal.

Assume H3: w ∈ Y.

Apply binunionI1 to the current goal.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is H3.

Assume H3: w ∈ Z.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is H3.

Let w be given.

Assume H1: w ∈ (X ∪ Y) ∪ Z.

We will prove w ∈ X ∪ (Y ∪ Z).

Apply (binunionE (X ∪ Y) Z w H1) to the current goal.

Assume H2: w ∈ X ∪ Y.

Apply (binunionE X Y w H2) to the current goal.

Assume H3: w ∈ X.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is H3.

Assume H3: w ∈ Y.

Apply binunionI2 to the current goal.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is H3.

Assume H2: w ∈ Z.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (binunion_com_Subq) The following is provable:

∀X Y : set, X ∪ Y ⊆ Y ∪ X

Proof:

Let X, Y and w be given.

Assume H1: w ∈ X ∪ Y.

We will prove w ∈ Y ∪ X.

Apply (binunionE X Y w H1) to the current goal.

Assume H2: w ∈ X.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is H2.

Assume H2: w ∈ Y.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (binunion_com) The following is provable:

∀X Y : set, X ∪ Y = Y ∪ X

Proof:

Let X and Y be given.

Apply set_ext to the current goal.

An exact proof term for the current goal is (binunion_com_Subq X Y).

An exact proof term for the current goal is (binunion_com_Subq Y X).

∎

Try to prove it yourself. Main Goal

Theorem. (binunion_idl) The following is provable:

∀X : set, Empty ∪ X = X

Proof:

Let X be given.

Apply set_ext to the current goal.

Let x be given.

Assume H1: x ∈ Empty ∪ X.

Apply (binunionE Empty X x H1) to the current goal.

Assume H2: x ∈ Empty.

We will prove False.

An exact proof term for the current goal is (EmptyE x H2).

Assume H2: x ∈ X.

An exact proof term for the current goal is H2.

Let x be given.

Assume H2: x ∈ X.

We will prove x ∈ Empty ∪ X.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (binunion_idr) The following is provable:

∀X : set, X ∪ Empty = X

Proof:

Let X be given.

rewrite the current goal using (binunion_com X Empty) (from left to right).

An exact proof term for the current goal is (binunion_idl X).

∎

Try to prove it yourself. Main Goal

Theorem. (binunion_Subq_1) The following is provable:

∀X Y : set, X ⊆ X ∪ Y

Proof:

An exact proof term for the current goal is binunionI1.

∎

Try to prove it yourself. Main Goal

Theorem. (binunion_Subq_2) The following is provable:

∀X Y : set, Y ⊆ X ∪ Y

Proof:

An exact proof term for the current goal is binunionI2.

∎

Try to prove it yourself. Main Goal

Theorem. (binunion_Subq_min) The following is provable:

∀X Y Z : set, X ⊆ Z → Y ⊆ Z → X ∪ Y ⊆ Z

Proof:

Let X, Y and Z be given.

Assume H1: X ⊆ Z.

Assume H2: Y ⊆ Z.

Let w be given.

Assume H3: w ∈ X ∪ Y.

Apply (binunionE X Y w H3) to the current goal.

Assume H4: w ∈ X.

An exact proof term for the current goal is (H1 w H4).

Assume H4: w ∈ Y.

An exact proof term for the current goal is (H2 w H4).

∎

Try to prove it yourself. Main Goal

Theorem. (Subq_binunion_eq) The following is provable:

∀X Y, (X ⊆ Y) = (X ∪ Y = Y)

Proof:

Let X and Y be given.

Apply prop_ext_2 to the current goal.

Assume H1: X ⊆ Y.

We will prove X ∪ Y = Y.

Apply set_ext to the current goal.

We will prove X ∪ Y ⊆ Y.

Apply (binunion_Subq_min X Y Y) to the current goal.

We will prove X ⊆ Y.

An exact proof term for the current goal is H1.

We will prove Y ⊆ Y.

An exact proof term for the current goal is (Subq_ref Y).

We will prove Y ⊆ X ∪ Y.

An exact proof term for the current goal is (binunion_Subq_2 X Y).

Assume H1: X ∪ Y = Y.

We will prove X ⊆ Y.

rewrite the current goal using H1 (from right to left).

We will prove X ⊆ X ∪ Y.

An exact proof term for the current goal is (binunion_Subq_1 X Y).

∎

Try to prove it yourself. Main Goal

Definition. We define SetAdjoin to be λX y ⇒ X ∪ {y} of type set → set → set.

Notation. We now use the set enumeration notation {...,...,...} in general. If 0 elements are given, then Empty is used to form the corresponding term. If 1 element is given, then Sing is used to form the corresponding term. If 2 elements are given, then UPair is used to form the corresponding term. If more than elements are given, then SetAdjoin is used to reduce to the case with one fewer elements.

Definition. We define famunion to be λX F ⇒ ⋃ {F x|x ∈ X} of type set → (set → set) → set.

Notation. We use ⋃ x [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using famunion.

Theorem. (famunionI) The following is provable:

∀X : set, ∀F : (set → set), ∀x y : set, x ∈ X → y ∈ F x → y ∈ ⋃_{x ∈ X}F x

Proof:

An exact proof term for the current goal is (λX F x y H1 H2 ⇒ UnionI (Repl X F) y (F x) H2 (ReplI X F x H1)).

∎

Try to prove it yourself. Main Goal

Theorem. (famunionE) The following is provable:

∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃_{x ∈ X}F x) → ∃x ∈ X, y ∈ F x

Proof:

Let X, F and y be given.

Assume H1: y ∈ (⋃_{x ∈ X}F x).

We will prove ∃x ∈ X, y ∈ F x.

Apply (UnionE_impred {F x|x ∈ X} y H1) to the current goal.

Let Y be given.

Assume H2: y ∈ Y.

Assume H3: Y ∈ {F x|x ∈ X}.

Apply (ReplE_impred X F Y H3) to the current goal.

Let x be given.

Assume H4: x ∈ X.

Assume H5: Y = F x.

We use x to witness the existential quantifier.

We will prove x ∈ X ∧ y ∈ F x.

Apply andI to the current goal.

An exact proof term for the current goal is H4.

We will prove y ∈ F x.

rewrite the current goal using H5 (from right to left).

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (famunionE_impred) The following is provable:

∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃_{x ∈ X}F x) → ∀p : prop, (∀x, x ∈ X → y ∈ F x → p) → p

Proof:

Let X, F and y be given.

Assume Hy.

Let p be given.

Assume Hp.

Apply famunionE X F y Hy to the current goal.

Let x be given.

Assume H1.

Apply H1 to the current goal.

An exact proof term for the current goal is Hp x.

∎

Try to prove it yourself. Main Goal

Theorem. (famunion_Empty) The following is provable:

∀F : set → set, (⋃_{x ∈ Empty}F x) = Empty

Proof:

Let F be given.

Apply Empty_Subq_eq to the current goal.

Let y be given.

Assume Hy: y ∈ ⋃_{x ∈ Empty}F x.

Apply famunionE_impred Empty F y Hy to the current goal.

Let x be given.

Assume Hx: x ∈ Empty.

We will prove False.

An exact proof term for the current goal is EmptyE x Hx.

∎

Try to prove it yourself. Main Goal

Beginning of Section SepSec

Variable X : set

Variable P : set → prop

Let z : set ≝ Eps_i (λz ⇒ z ∈ X ∧ P z)

Let F : set → set ≝ λx ⇒ if P x then x else z

Definition. We define Sep to be if (∃z ∈ X, P z) then {F x|x ∈ X} else Empty of type set.

End of Section SepSec

Notation. {x ∈ A | B} is notation for Sep A (λ x . B).

Theorem. (SepI) The following is provable:

∀X : set, ∀P : (set → prop), ∀x : set, x ∈ X → P x → x ∈ {x ∈ X|P x}

Proof:

Let X, P and x be given.

Set z to be the term Eps_i (λz ⇒ z ∈ X ∧ P z) of type set.

Set F to be the term λx ⇒ if P x then x else z of type set → set.

Assume H1: x ∈ X.

Assume H2: P x.

We prove the intermediate claim L1: ∃z ∈ X, P z.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is H2.

We will prove x ∈ {x ∈ X|P x}.

We will prove x ∈ if (∃z ∈ X, P z) then {F x|x ∈ X} else Empty.

We prove the intermediate claim L2: (if (∃z ∈ X, P z) then {F x|x ∈ X} else Empty) = {F x|x ∈ X}.

An exact proof term for the current goal is (If_i_1 (∃z ∈ X, P z) {F x|x ∈ X} Empty L1).

rewrite the current goal using L2 (from left to right).

We will prove x ∈ {F x|x ∈ X}.

We prove the intermediate claim L3: F x = x.

We will prove (if P x then x else z) = x.

An exact proof term for the current goal is (If_i_1 (P x) x z H2).

rewrite the current goal using L3 (from right to left).

We will prove F x ∈ {F x|x ∈ X}.

An exact proof term for the current goal is (ReplI X F x H1).

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Main Goal

Theorem. (SepE) The following is provable:

∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X ∧ P x

Proof:

Let X, P and x be given.

Set z to be the term Eps_i (λz ⇒ z ∈ X ∧ P z) of type set.

Set F to be the term λx ⇒ if P x then x else z of type set → set.

Apply (xm (∃z ∈ X, P z)) to the current goal.

Assume H1: ∃z ∈ X, P z.

We will prove (x ∈ (if (∃z ∈ X, P z) then {F x|x ∈ X} else Empty) → x ∈ X ∧ P x).

We prove the intermediate claim L1: (if (∃z ∈ X, P z) then {F x|x ∈ X} else Empty) = {F x|x ∈ X}.

An exact proof term for the current goal is (If_i_1 (∃z ∈ X, P z) {F x|x ∈ X} Empty H1).

rewrite the current goal using L1 (from left to right).

We will prove x ∈ {F x|x ∈ X} → x ∈ X ∧ P x.

Assume H2: x ∈ {F x|x ∈ X}.

Apply (ReplE_impred X F x H2) to the current goal.

Let y be given.

Assume H3: y ∈ X.

Assume H4: x = F y.

We will prove x ∈ X ∧ P x.

Apply (xm (P y)) to the current goal.

Assume H5: P y.

We prove the intermediate claim L2: x = y.

rewrite the current goal using (If_i_1 (P y) y z H5) (from right to left).

An exact proof term for the current goal is H4.

rewrite the current goal using L2 (from left to right).

We will prove y ∈ X ∧ P y.

Apply andI to the current goal.

An exact proof term for the current goal is H3.

An exact proof term for the current goal is H5.

Assume H5: ¬ P y.

We prove the intermediate claim L2: x = z.

rewrite the current goal using (If_i_0 (P y) y z H5) (from right to left).

An exact proof term for the current goal is H4.

rewrite the current goal using L2 (from left to right).

We will prove z ∈ X ∧ P z.

An exact proof term for the current goal is (Eps_i_ex (λz ⇒ z ∈ X ∧ P z) H1).

Assume H1: ¬ ∃z ∈ X, P z.

We will prove (x ∈ (if (∃z ∈ X, P z) then {F x|x ∈ X} else Empty) → x ∈ X ∧ P x).

We prove the intermediate claim L1: (if (∃z ∈ X, P z) then {F x|x ∈ X} else Empty) = Empty.

An exact proof term for the current goal is (If_i_0 (∃z ∈ X, P z) {F x|x ∈ X} Empty H1).

rewrite the current goal using L1 (from left to right).

We will prove x ∈ Empty → x ∈ X ∧ P x.

Assume H2: x ∈ Empty.

We will prove False.

An exact proof term for the current goal is (EmptyE x H2).

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Main Goal

Theorem. (SepE1) The following is provable:

∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X

Proof:

An exact proof term for the current goal is (λX P x H ⇒ SepE X P x H (x ∈ X) (λH _ ⇒ H)).

∎

Try to prove it yourself. Main Goal

Theorem. (SepE2) The following is provable:

∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → P x

Proof:

An exact proof term for the current goal is (λX P x H ⇒ SepE X P x H (P x) (λ_ H ⇒ H)).

∎

Try to prove it yourself. Main Goal

Theorem. (Sep_Subq) The following is provable:

∀X : set, ∀P : set → prop, {x ∈ X|P x} ⊆ X

Proof:

An exact proof term for the current goal is SepE1.

∎

Try to prove it yourself. Main Goal

Theorem. (Sep_In_Power) The following is provable:

∀X : set, ∀P : set → prop, {x ∈ X|P x} ∈ 𝒫 X

Proof:

An exact proof term for the current goal is (λX P ⇒ PowerI X (Sep X P) (Sep_Subq X P)).

∎

Try to prove it yourself. Main Goal

Definition. We define ReplSep to be λX P F ⇒ {F x|x ∈ {z ∈ X|P z}} of type set → (set → prop) → (set → set) → set.

Notation. {B| x ∈ A, C} is notation for ReplSep A (λ x . C) (λ x . B).

Theorem. (ReplSepI) The following is provable:

∀X : set, ∀P : set → prop, ∀F : set → set, ∀x : set, x ∈ X → P x → F x ∈ {F x|x ∈ X, P x}

Proof:

An exact proof term for the current goal is (λX P F x u v ⇒ ReplI (Sep X P) F x (SepI X P x u v)).

∎

Try to prove it yourself. Main Goal

Theorem. (ReplSepE) The following is provable:

∀X : set, ∀P : set → prop, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ X, P x} → ∃x : set, x ∈ X ∧ P x ∧ y = F x

Proof:

Let X, P, F and y be given.

Assume H1: y ∈ {F x|x ∈ {z ∈ X|P z}}.

Apply (ReplE {z ∈ X|P z} F y H1) to the current goal.

Let x be given.

Assume H2: x ∈ {z ∈ X|P z} ∧ y = F x.

Apply H2 to the current goal.

Assume H3: x ∈ {z ∈ X|P z}.

Assume H4: y = F x.

Apply (SepE X P x H3) to the current goal.

Assume H5: x ∈ X.

Assume H6: P x.

We use x to witness the existential quantifier.

Apply and3I to the current goal.

An exact proof term for the current goal is H5.

An exact proof term for the current goal is H6.

An exact proof term for the current goal is H4.

∎

Try to prove it yourself. Main Goal

Theorem. (ReplSepE_impred) The following is provable:

∀X : set, ∀P : set → prop, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ X, P x} → ∀p : prop, (∀x ∈ X, P x → y = F x → p) → p

Proof:

Let X, P, F and y be given.

Assume H1: y ∈ {F x|x ∈ X, P x}.

Let p be given.

Assume H2: ∀x ∈ X, P x → y = F x → p.

We will prove p.

Apply ReplSepE X P F y H1 to the current goal.

Let x be given.

Assume H3.

Apply H3 to the current goal.

Assume H3.

Apply H3 to the current goal.

An exact proof term for the current goal is H2 x.

∎

Try to prove it yourself. Main Goal

Definition. We define binintersect to be λX Y ⇒ {x ∈ X|x ∈ Y} of type set → set → set.

Notation. We use ∩ as an infix operator with priority 340 and which associates to the left corresponding to applying term binintersect.

Theorem. (binintersectI) The following is provable:

∀X Y z, z ∈ X → z ∈ Y → z ∈ X ∩ Y

Proof:

An exact proof term for the current goal is (λX Y z H1 H2 ⇒ SepI X (λx : set ⇒ x ∈ Y) z H1 H2).

∎

Try to prove it yourself. Main Goal

Theorem. (binintersectE) The following is provable:

∀X Y z, z ∈ X ∩ Y → z ∈ X ∧ z ∈ Y

Proof:

An exact proof term for the current goal is (λX Y z H1 ⇒ SepE X (λx : set ⇒ x ∈ Y) z H1).

∎

Try to prove it yourself. Main Goal

Theorem. (binintersectE1) The following is provable:

∀X Y z, z ∈ X ∩ Y → z ∈ X

Proof:

An exact proof term for the current goal is (λX Y z H1 ⇒ SepE1 X (λx : set ⇒ x ∈ Y) z H1).

∎

Try to prove it yourself. Main Goal

Theorem. (binintersectE2) The following is provable:

∀X Y z, z ∈ X ∩ Y → z ∈ Y

Proof:

An exact proof term for the current goal is (λX Y z H1 ⇒ SepE2 X (λx : set ⇒ x ∈ Y) z H1).

∎

Try to prove it yourself. Main Goal

Theorem. (binintersect_Subq_1) The following is provable:

∀X Y : set, X ∩ Y ⊆ X

Proof:

An exact proof term for the current goal is binintersectE1.

∎

Try to prove it yourself. Main Goal

Theorem. (binintersect_Subq_2) The following is provable:

∀X Y : set, X ∩ Y ⊆ Y

Proof:

An exact proof term for the current goal is binintersectE2.

∎

Try to prove it yourself. Main Goal

Theorem. (binintersect_Subq_eq_1) The following is provable:

∀X Y, X ⊆ Y → X ∩ Y = X

Proof:

Let X and Y be given.

Assume H1: X ⊆ Y.

Apply set_ext to the current goal.

Apply binintersect_Subq_1 to the current goal.

Let x be given.

Assume H2: x ∈ X.

Apply binintersectI to the current goal.

An exact proof term for the current goal is H2.

Apply H1 to the current goal.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (binintersect_Subq_max) The following is provable:

∀X Y Z : set, Z ⊆ X → Z ⊆ Y → Z ⊆ X ∩ Y

Proof:

Let X, Y and Z be given.

Assume H1: Z ⊆ X.

Assume H2: Z ⊆ Y.

Let w be given.

Assume H3: w ∈ Z.

Apply (binintersectI X Y w) to the current goal.

We will prove w ∈ X.

An exact proof term for the current goal is (H1 w H3).

We will prove w ∈ Y.

An exact proof term for the current goal is (H2 w H3).

∎

Try to prove it yourself. Main Goal

Theorem. (binintersect_com_Subq) The following is provable:

∀X Y : set, X ∩ Y ⊆ Y ∩ X

Proof:

Let X and Y be given.

Apply (binintersect_Subq_max Y X (X ∩ Y)) to the current goal.

We will prove X ∩ Y ⊆ Y.

Apply binintersect_Subq_2 to the current goal.

We will prove X ∩ Y ⊆ X.

Apply binintersect_Subq_1 to the current goal.

∎

Try to prove it yourself. Main Goal

Theorem. (binintersect_com) The following is provable:

∀X Y : set, X ∩ Y = Y ∩ X

Proof:

Let X and Y be given.

Apply set_ext to the current goal.

An exact proof term for the current goal is (binintersect_com_Subq X Y).

An exact proof term for the current goal is (binintersect_com_Subq Y X).

∎

Try to prove it yourself. Main Goal

Definition. We define setminus to be λX Y ⇒ Sep X (λx ⇒ x ∉ Y) of type set → set → set.

Notation. We use ∖ as an infix operator with priority 350 and no associativity corresponding to applying term setminus.

Theorem. (setminusI) The following is provable:

∀X Y z, (z ∈ X) → (z ∉ Y) → z ∈ X ∖ Y

Proof:

An exact proof term for the current goal is (λX Y z H1 H2 ⇒ SepI X (λx : set ⇒ x ∉ Y) z H1 H2).

∎

Try to prove it yourself. Main Goal

Theorem. (setminusE) The following is provable:

∀X Y z, (z ∈ X ∖ Y) → z ∈ X ∧ z ∉ Y

Proof:

An exact proof term for the current goal is (λX Y z H ⇒ SepE X (λx : set ⇒ x ∉ Y) z H).

∎

Try to prove it yourself. Main Goal

Theorem. (setminusE1) The following is provable:

∀X Y z, (z ∈ X ∖ Y) → z ∈ X

Proof:

An exact proof term for the current goal is (λX Y z H ⇒ SepE1 X (λx : set ⇒ x ∉ Y) z H).

∎

Try to prove it yourself. Main Goal

Theorem. (setminus_Subq) The following is provable:

∀X Y : set, X ∖ Y ⊆ X

Proof:

An exact proof term for the current goal is setminusE1.

∎

Try to prove it yourself. Main Goal

Theorem. (setminus_Subq_contra) The following is provable:

∀X Y Z : set, Z ⊆ Y → X ∖ Y ⊆ X ∖ Z

Proof:

Let X, Y and Z be given.

Assume H1: Z ⊆ Y.

Let x be given.

Assume H2: x ∈ X ∖ Y.

Apply (setminusE X Y x H2) to the current goal.

Assume H3: x ∈ X.

Assume H4: x ∉ Y.

We will prove x ∈ X ∖ Z.

Apply setminusI to the current goal.

An exact proof term for the current goal is H3.

We will prove x ∉ Z.

An exact proof term for the current goal is (Subq_contra Z Y x H1 H4).

∎

Try to prove it yourself. Main Goal

Theorem. (setminus_In_Power) The following is provable:

∀A U, A ∖ U ∈ 𝒫 A

Proof:

Let A and U be given.

Apply PowerI to the current goal.

Apply setminus_Subq to the current goal.

∎

Try to prove it yourself. Main Goal

Theorem. (In_irref) The following is provable:

∀x, x ∉ x

Proof:

Apply In_ind to the current goal.

We will prove (∀X : set, (∀x : set, x ∈ X → x ∉ x) → X ∉ X).

Let X be given.

Assume IH: ∀x : set, x ∈ X → x ∉ x.

Assume H: X ∈ X.

An exact proof term for the current goal is IH X H H.

∎

Try to prove it yourself. Main Goal

Theorem. (In_no2cycle) The following is provable:

∀x y, x ∈ y → y ∈ x → False

Proof:

Apply In_ind to the current goal.

Let x be given.

Assume IH: ∀z, z ∈ x → ∀y, z ∈ y → y ∈ z → False.

Let y be given.

Assume H1: x ∈ y.

Assume H2: y ∈ x.

An exact proof term for the current goal is IH y H2 x H2 H1.

∎

Try to prove it yourself. Main Goal

Ordinals and Natural Numbers

Definition. We define ordsucc to be λx : set ⇒ x ∪ {x} of type set → set.

Theorem. (ordsuccI1) The following is provable:

∀x : set, x ⊆ ordsucc x

Proof:

Let x be given.

An exact proof term for the current goal is (λ(y : set)(H1 : y ∈ x) ⇒ binunionI1 x {x} y H1).

∎

Try to prove it yourself. Main Goal

Theorem. (ordsuccI2) The following is provable:

∀x : set, x ∈ ordsucc x

Proof:

An exact proof term for the current goal is (λx : set ⇒ binunionI2 x {x} x (SingI x)).

∎

Try to prove it yourself. Main Goal

Theorem. (ordsuccE) The following is provable:

∀x y : set, y ∈ ordsucc x → y ∈ x ∨ y = x

Proof:

Let x and y be given.

Assume H1: y ∈ x ∪ {x}.

Apply (binunionE x {x} y H1) to the current goal.

Assume H2: y ∈ x.

Apply orIL to the current goal.

An exact proof term for the current goal is H2.

Assume H2: y ∈ {x}.

Apply orIR to the current goal.

An exact proof term for the current goal is (SingE x y H2).

∎

Try to prove it yourself. Main Goal

Notation. Natural numbers 0,1,2,... are notation for the terms formed using Empty as 0 and forming successors with ordsucc.

Theorem. (neq_0_ordsucc) The following is provable:

∀a : set, 0 ≠ ordsucc a

Proof:

Let a be given.

We will prove ¬ (0 = ordsucc a).

Assume H1: 0 = ordsucc a.

We prove the intermediate claim L1: a ∈ ordsucc a → False.

rewrite the current goal using H1 (from right to left).

An exact proof term for the current goal is (EmptyE a).

An exact proof term for the current goal is (L1 (ordsuccI2 a)).

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (neq_ordsucc_0) The following is provable:

∀a : set, ordsucc a ≠ 0

Proof:

Let a be given.

An exact proof term for the current goal is neq_i_sym 0 (ordsucc a) (neq_0_ordsucc a).

∎

Try to prove it yourself. Main Goal

Theorem. (ordsucc_inj) The following is provable:

∀a b : set, ordsucc a = ordsucc b → a = b

Proof:

Let a and b be given.

Assume H1: ordsucc a = ordsucc b.

We prove the intermediate claim L1: a ∈ ordsucc b.

rewrite the current goal using H1 (from right to left).

An exact proof term for the current goal is (ordsuccI2 a).

Apply (ordsuccE b a L1) to the current goal.

Assume H2: a ∈ b.

We prove the intermediate claim L2: b ∈ ordsucc a.

rewrite the current goal using H1 (from left to right).

An exact proof term for the current goal is (ordsuccI2 b).

Apply (ordsuccE a b L2) to the current goal.

Assume H3: b ∈ a.

We will prove False.

An exact proof term for the current goal is (In_no2cycle a b H2 H3).

Assume H3: b = a.

Use symmetry.

An exact proof term for the current goal is H3.

Assume H2: a = b.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Theorem. (ordsucc_inj_contra) The following is provable:

∀a b : set, a ≠ b → ordsucc a ≠ ordsucc b

Proof:

Let a and b be given.

Assume H1.

We will prove ¬ (ordsucc a = ordsucc b).

Assume H2: ordsucc a = ordsucc b.

An exact proof term for the current goal is H1 (ordsucc_inj a b H2).

∎

Try to prove it yourself. Main Goal

Theorem. (In_0_1) The following is provable:

0 ∈ 1

Proof:

An exact proof term for the current goal is (ordsuccI2 0).

∎

Try to prove it yourself. Main Goal

Theorem. (In_0_2) The following is provable:

0 ∈ 2

Proof:

An exact proof term for the current goal is (ordsuccI1 1 0 In_0_1).

∎

Try to prove it yourself. Main Goal

Theorem. (In_1_2) The following is provable:

1 ∈ 2

Proof:

An exact proof term for the current goal is (ordsuccI2 1).

∎

Try to prove it yourself. Main Goal

Definition. We define nat_p to be λn : set ⇒ ∀p : set → prop, p 0 → (∀x : set, p x → p (ordsucc x)) → p n of type set → prop.

Theorem. (nat_0) The following is provable:

nat_p 0

Proof:

An exact proof term for the current goal is (λp H _ ⇒ H).

∎

Try to prove it yourself. Main Goal

Theorem. (nat_ordsucc) The following is provable:

∀n : set, nat_p n → nat_p (ordsucc n)

Proof:

An exact proof term for the current goal is (λn H1 p H2 H3 ⇒ H3 n (H1 p H2 H3)).

∎

Try to prove it yourself. Main Goal

Theorem. (nat_1) The following is provable:

nat_p 1

Proof:

An exact proof term for the current goal is (nat_ordsucc 0 nat_0).

∎

Try to prove it yourself. Main Goal

Theorem. (nat_2) The following is provable:

nat_p 2

Proof:

An exact proof term for the current goal is (nat_ordsucc 1 nat_1).

∎

Try to prove it yourself. Main Goal

Theorem. (nat_0_in_ordsucc) The following is provable:

∀n, nat_p n → 0 ∈ ordsucc n

Proof:

Let n be given.

Assume H1.

Apply H1 (λn ⇒ 0 ∈ ordsucc n) to the current goal.

We will prove 0 ∈ ordsucc 0.

An exact proof term for the current goal is In_0_1.

Let n be given.

Assume IH: 0 ∈ ordsucc n.

We will prove 0 ∈ ordsucc (ordsucc n).

An exact proof term for the current goal is (ordsuccI1 (ordsucc n) 0 IH).

∎

Try to prove it yourself. Main Goal

Theorem. (nat_ordsucc_in_ordsucc) The following is provable:

∀n, nat_p n → ∀m ∈ n, ordsucc m ∈ ordsucc n

Proof:

Let n be given.

Assume H1.

Apply (H1 (λn ⇒ ∀m ∈ n, ordsucc m ∈ ordsucc n)) to the current goal.

We will prove ∀m ∈ 0, ordsucc m ∈ ordsucc 0.

Let m be given.

Assume Hm: m ∈ 0.

We will prove False.

An exact proof term for the current goal is (EmptyE m Hm).

Let n be given.

Assume IH: ∀m ∈ n, ordsucc m ∈ ordsucc n.

We will prove ∀m ∈ ordsucc n, ordsucc m ∈ ordsucc (ordsucc n).

Let m be given.

Assume H2: m ∈ ordsucc n.

We will prove ordsucc m ∈ ordsucc (ordsucc n).

Apply (ordsuccE n m H2) to the current goal.

Assume H3: m ∈ n.

We prove the intermediate claim L1: ordsucc m ∈ ordsucc n.

An exact proof term for the current goal is (IH m H3).

An exact proof term for the current goal is (ordsuccI1 (ordsucc n) (ordsucc m) L1).

Assume H3: m = n.

rewrite the current goal using H3 (from left to right).

We will prove ordsucc n ∈ ordsucc (ordsucc n).

An exact proof term for the current goal is (ordsuccI2 (ordsucc n)).

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (nat_ind) The following is provable:

∀p : set → prop, p 0 → (∀n, nat_p n → p n → p (ordsucc n)) → ∀n, nat_p n → p n

Proof:

Let p be given.

Assume H1: p 0.

Assume H2: ∀n, nat_p n → p n → p (ordsucc n).

We prove the intermediate claim L1: nat_p 0 ∧ p 0.

An exact proof term for the current goal is (andI (nat_p 0) (p 0) nat_0 H1).

We prove the intermediate claim L2: ∀n, nat_p n ∧ p n → nat_p (ordsucc n) ∧ p (ordsucc n).

Let n be given.

Assume H3: nat_p n ∧ p n.

Apply H3 to the current goal.

Assume H4: nat_p n.

Assume H5: p n.

Apply andI to the current goal.

We will prove nat_p (ordsucc n).

An exact proof term for the current goal is (nat_ordsucc n H4).

We will prove p (ordsucc n).

An exact proof term for the current goal is (H2 n H4 H5).

Let n be given.

Assume H3.

We prove the intermediate claim L3: nat_p n ∧ p n.

An exact proof term for the current goal is (H3 (λn ⇒ nat_p n ∧ p n) L1 L2).

An exact proof term for the current goal is (andER (nat_p n) (p n) L3).

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Main Goal

Theorem. (nat_inv_impred) The following is provable:

∀p : set → prop, p 0 → (∀n, nat_p n → p (ordsucc n)) → ∀n, nat_p n → p n

Proof:

Let p be given.

Assume H1 H2.

An exact proof term for the current goal is nat_ind p H1 (λn H _ ⇒ H2 n H).

∎

Try to prove it yourself. Main Goal

Theorem. (nat_inv) The following is provable:

∀n, nat_p n → n = 0 ∨ ∃x, nat_p x ∧ n = ordsucc x

Proof:

Apply nat_inv_impred to the current goal.

Apply orIL to the current goal.

Use reflexivity.

Let n be given.

Assume Hn.

Apply orIR to the current goal.

We use n to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hn.

Use reflexivity.

∎

Try to prove it yourself. Main Goal

Theorem. (nat_complete_ind) The following is provable:

∀p : set → prop, (∀n, nat_p n → (∀m ∈ n, p m) → p n) → ∀n, nat_p n → p n

Proof:

Let p be given.

Assume H1: ∀n, nat_p n → (∀m ∈ n, p m) → p n.

We prove the intermediate claim L1: ∀n : set, nat_p n → ∀m ∈ n, p m.

Apply nat_ind to the current goal.

We will prove ∀m ∈ 0, p m.

Let m be given.

Assume Hm: m ∈ 0.

We will prove False.

An exact proof term for the current goal is (EmptyE m Hm).

Let n be given.

Assume Hn: nat_p n.

Assume IHn: ∀m ∈ n, p m.

We will prove ∀m ∈ ordsucc n, p m.

Let m be given.

Assume Hm: m ∈ ordsucc n.

We will prove p m.

Apply (ordsuccE n m Hm) to the current goal.

Assume H2: m ∈ n.

An exact proof term for the current goal is (IHn m H2).

Assume H2: m = n.

We will prove p m.

rewrite the current goal using H2 (from left to right).

We will prove p n.

An exact proof term for the current goal is (H1 n Hn IHn).

We will prove ∀n, nat_p n → p n.

An exact proof term for the current goal is (λn Hn ⇒ H1 n Hn (L1 n Hn)).

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (nat_p_trans) The following is provable:

∀n, nat_p n → ∀m ∈ n, nat_p m

Proof:

Apply nat_ind to the current goal.

We will prove ∀m ∈ 0, nat_p m.

Let m be given.

Assume Hm: m ∈ 0.

We will prove False.

An exact proof term for the current goal is (EmptyE m Hm).

Let n be given.

Assume Hn: nat_p n.

Assume IHn: ∀m ∈ n, nat_p m.

We will prove ∀m ∈ ordsucc n, nat_p m.

Let m be given.

Assume Hm: m ∈ ordsucc n.

Apply (ordsuccE n m Hm) to the current goal.

Assume H1: m ∈ n.

An exact proof term for the current goal is (IHn m H1).

Assume H1: m = n.

rewrite the current goal using H1 (from left to right).

An exact proof term for the current goal is Hn.

∎

Try to prove it yourself. Main Goal

Theorem. (nat_trans) The following is provable:

∀n, nat_p n → ∀m ∈ n, m ⊆ n

Proof:

Apply nat_ind to the current goal.

We will prove ∀m ∈ 0, m ⊆ 0.

Let m be given.

Assume Hm: m ∈ 0.

We will prove False.

An exact proof term for the current goal is (EmptyE m Hm).

Let n be given.

Assume Hn: nat_p n.

Assume IHn: ∀m ∈ n, m ⊆ n.

We will prove ∀m ∈ ordsucc n, m ⊆ ordsucc n.

Let m be given.

Assume Hm: m ∈ ordsucc n.

Apply (ordsuccE n m Hm) to the current goal.

Assume H1: m ∈ n.

We will prove m ⊆ ordsucc n.

Apply (Subq_tra m n (ordsucc n)) to the current goal.

An exact proof term for the current goal is (IHn m H1).

An exact proof term for the current goal is (ordsuccI1 n).

Assume H1: m = n.

We will prove m ⊆ ordsucc n.

rewrite the current goal using H1 (from left to right).

We will prove n ⊆ ordsucc n.

An exact proof term for the current goal is (ordsuccI1 n).

∎

Try to prove it yourself. Main Goal

Theorem. (nat_ordsucc_trans) The following is provable:

∀n, nat_p n → ∀m ∈ ordsucc n, m ⊆ n

Proof:

Let n be given.

Assume Hn: nat_p n.

Let m be given.

Assume Hm: m ∈ ordsucc n.

Let k be given.

Assume Hk: k ∈ m.

We will prove k ∈ n.

Apply (ordsuccE n m Hm) to the current goal.

Assume H1: m ∈ n.

An exact proof term for the current goal is nat_trans n Hn m H1 k Hk.

Assume H1: m = n.

rewrite the current goal using H1 (from right to left).

An exact proof term for the current goal is Hk.

∎

Try to prove it yourself. Main Goal

Theorem. (Union_ordsucc_eq) The following is provable:

∀n, nat_p n → ⋃ (ordsucc n) = n

Proof:

Apply nat_complete_ind to the current goal.

Let n be given.

Assume Hn: nat_p n.

Assume IHn: ∀m ∈ n, ⋃ (ordsucc m) = m.

We will prove ⋃ (ordsucc n) = n.

Apply set_ext to the current goal.

Let m be given.

Assume Hm: m ∈ ⋃ (ordsucc n).

Apply (UnionE_impred (ordsucc n) m Hm) to the current goal.

Let k be given.

Assume H1: m ∈ k.

Assume H2: k ∈ ordsucc n.

We will prove m ∈ n.

An exact proof term for the current goal is nat_ordsucc_trans n Hn k H2 m H1.

Let m be given.

Assume Hm: m ∈ n.

We will prove m ∈ ⋃ (ordsucc n).

Apply (UnionI (ordsucc n) m n) to the current goal.

An exact proof term for the current goal is Hm.

An exact proof term for the current goal is (ordsuccI2 n).

∎

Try to prove it yourself. Main Goal

Theorem. (cases_1) The following is provable:

∀i ∈ 1, ∀p : set → prop, p 0 → p i

Proof:

Let i be given.

Assume Hi.

Let p be given.

Assume Hp0.

Apply ordsuccE 0 i Hi to the current goal.

Assume Hil: i ∈ 0.

Apply EmptyE i Hil to the current goal.

Assume Hie: i = 0.

rewrite the current goal using Hie (from left to right).

An exact proof term for the current goal is Hp0.

∎

Try to prove it yourself. Main Goal

Theorem. (cases_2) The following is provable:

∀i ∈ 2, ∀p : set → prop, p 0 → p 1 → p i

Proof:

Let i be given.

Assume Hi.

Let p be given.

Assume Hp0 Hp1.

Apply ordsuccE 1 i Hi to the current goal.

Assume Hil: i ∈ 1.

An exact proof term for the current goal is cases_1 i Hil p Hp0.

Assume Hie: i = 1.

rewrite the current goal using Hie (from left to right).

An exact proof term for the current goal is Hp1.

∎

Try to prove it yourself. Main Goal

Theorem. (cases_3) The following is provable:

∀i ∈ 3, ∀p : set → prop, p 0 → p 1 → p 2 → p i

Proof:

Let i be given.

Assume Hi.

Let p be given.

Assume Hp0 Hp1 Hp2.

Apply ordsuccE 2 i Hi to the current goal.

Assume Hil: i ∈ 2.

An exact proof term for the current goal is cases_2 i Hil p Hp0 Hp1.

Assume Hie: i = 2.

rewrite the current goal using Hie (from left to right).

An exact proof term for the current goal is Hp2.

∎

Try to prove it yourself. Main Goal

Theorem. (neq_0_1) The following is provable:

0 ≠ 1

Proof:

An exact proof term for the current goal is (neq_0_ordsucc 0).

∎

Try to prove it yourself. Main Goal

Theorem. (neq_1_0) The following is provable:

1 ≠ 0

Proof:

An exact proof term for the current goal is (neq_ordsucc_0 0).

∎

Try to prove it yourself. Main Goal

Theorem. (neq_0_2) The following is provable:

0 ≠ 2

Proof:

An exact proof term for the current goal is (neq_0_ordsucc 1).

∎

Try to prove it yourself. Main Goal

Theorem. (neq_2_0) The following is provable:

2 ≠ 0

Proof:

An exact proof term for the current goal is (neq_ordsucc_0 1).

∎

Try to prove it yourself. Main Goal

Theorem. (neq_1_2) The following is provable:

1 ≠ 2

Proof:

An exact proof term for the current goal is (ordsucc_inj_contra 0 1 neq_0_1).

∎

Try to prove it yourself. Main Goal

Theorem. (ZF_closed_E) The following is provable:

∀U, ZF_closed U → ∀p : prop, (Union_closed U → Power_closed U → Repl_closed U → p) → p

Proof:

An exact proof term for the current goal is (λU C p v ⇒ C p (λC H3 ⇒ C p (λH1 H2 ⇒ v H1 H2 H3))).

∎

Try to prove it yourself. Main Goal

Theorem. (ZF_Union_closed) The following is provable:

∀U, ZF_closed U → ∀X ∈ U, ⋃ X ∈ U

Proof:

An exact proof term for the current goal is (λU C ⇒ ZF_closed_E U C (∀X ∈ U, ⋃ X ∈ U) (λH _ _ ⇒ H)).

∎

Try to prove it yourself. Main Goal

Theorem. (ZF_Power_closed) The following is provable:

∀U, ZF_closed U → ∀X ∈ U, 𝒫 X ∈ U

Proof:

An exact proof term for the current goal is (λU C ⇒ ZF_closed_E U C (∀X ∈ U, 𝒫 X ∈ U) (λ_ H _ ⇒ H)).

∎

Try to prove it yourself. Main Goal

Theorem. (ZF_Repl_closed) The following is provable:

∀U, ZF_closed U → ∀X ∈ U, ∀F : set → set, (∀x ∈ X, F x ∈ U) → {F x|x ∈ X} ∈ U

Proof:

An exact proof term for the current goal is (λU C ⇒ ZF_closed_E U C (∀X ∈ U, ∀F : set → set, (∀x ∈ X, F x ∈ U) → {F x|x ∈ X} ∈ U) (λ_ _ H ⇒ H)).

∎

Try to prove it yourself. Main Goal

Theorem. (ZF_UPair_closed) The following is provable:

∀U, ZF_closed U → ∀x y ∈ U, {x,y} ∈ U

Proof:

Let U be given.

Assume C: ZF_closed U.

Let x be given.

Assume Hx: x ∈ U.

Let y be given.

Assume Hy: y ∈ U.

We will prove {x,y} ∈ U.

We prove the intermediate claim L1: {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)} = {x,y}.

Apply set_ext to the current goal.

We will prove {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)} ⊆ {x,y}.

Let z be given.

Assume Hz: z ∈ {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)}.

We will prove z ∈ {x,y}.

Apply (ReplE_impred (𝒫 (𝒫 x)) (λX ⇒ if x ∈ X then x else y) z Hz) to the current goal.

Let X be given.

Assume _.

We will prove z = (if x ∈ X then x else y) → z ∈ {x,y}.

Apply (xm (x ∈ X)) to the current goal.

Assume H2: x ∈ X.

rewrite the current goal using (If_i_1 (x ∈ X) x y H2) (from left to right).

We will prove (z = x → z ∈ {x,y}).

Assume H3: z = x.

rewrite the current goal using H3 (from left to right).

An exact proof term for the current goal is (UPairI1 x y).

Assume H2: x ∉ X.

rewrite the current goal using (If_i_0 (x ∈ X) x y H2) (from left to right).

We will prove (z = y → z ∈ {x,y}).

Assume H3: z = y.

rewrite the current goal using H3 (from left to right).

An exact proof term for the current goal is (UPairI2 x y).

We will prove {x,y} ⊆ {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)}.

Let z be given.

Assume Hz: z ∈ {x,y}.

We will prove z ∈ {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)}.

We prove the intermediate claim L1a: (if x ∈ (𝒫 x) then x else y) ∈ {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)}.

Apply (ReplI (𝒫 (𝒫 x)) (λX ⇒ if x ∈ X then x else y) (𝒫 x)) to the current goal.

We will prove 𝒫 x ∈ 𝒫 (𝒫 x).

An exact proof term for the current goal is (Self_In_Power (𝒫 x)).

We prove the intermediate claim L1b: (if x ∈ Empty then x else y) ∈ {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)}.

Apply (ReplI (𝒫 (𝒫 x)) (λX ⇒ if x ∈ X then x else y) Empty) to the current goal.

We will prove Empty ∈ 𝒫 (𝒫 x).

An exact proof term for the current goal is (Empty_In_Power (𝒫 x)).

Apply (UPairE z x y Hz) to the current goal.

Assume H1: z = x.

rewrite the current goal using H1 (from left to right).

We will prove x ∈ {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)}.

rewrite the current goal using (If_i_1 (x ∈ (𝒫 x)) x y (Self_In_Power x)) (from right to left) at position 1.

An exact proof term for the current goal is L1a.

Assume H1: z = y.

rewrite the current goal using H1 (from left to right).

We will prove y ∈ {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)}.

rewrite the current goal using (If_i_0 (x ∈ Empty) x y (EmptyE x)) (from right to left) at position 1.

An exact proof term for the current goal is L1b.

We will prove {x,y} ∈ U.

rewrite the current goal using L1 (from right to left).

We will prove {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)} ∈ U.

We prove the intermediate claim L2: 𝒫 (𝒫 x) ∈ U.

An exact proof term for the current goal is (ZF_Power_closed U C (𝒫 x) (ZF_Power_closed U C x Hx)).

We prove the intermediate claim L3: ∀X ∈ 𝒫 (𝒫 x), (if x ∈ X then x else y) ∈ U.

Let X be given.

Assume _.

We will prove (if x ∈ X then x else y) ∈ U.

Apply (xm (x ∈ X)) to the current goal.

Assume H1: x ∈ X.

rewrite the current goal using (If_i_1 (x ∈ X) x y H1) (from left to right).

We will prove x ∈ U.

An exact proof term for the current goal is Hx.

Assume H1: x ∉ X.

rewrite the current goal using (If_i_0 (x ∈ X) x y H1) (from left to right).

We will prove y ∈ U.

An exact proof term for the current goal is Hy.

An exact proof term for the current goal is (ZF_Repl_closed U C (𝒫 (𝒫 x)) L2 (λX ⇒ if x ∈ X then x else y) L3).

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Main Goal

Theorem. (ZF_Sing_closed) The following is provable:

∀U, ZF_closed U → ∀x ∈ U, {x} ∈ U

Proof:

An exact proof term for the current goal is (λU C x H ⇒ ZF_UPair_closed U C x H x H).

∎

Try to prove it yourself. Main Goal

Theorem. (ZF_binunion_closed) The following is provable:

∀U, ZF_closed U → ∀X Y ∈ U, (X ∪ Y) ∈ U

Proof:

An exact proof term for the current goal is (λU C X HX Y HY ⇒ ZF_Union_closed U C {X,Y} (ZF_UPair_closed U C X HX Y HY)).

∎

Try to prove it yourself. Main Goal

Theorem. (ZF_ordsucc_closed) The following is provable:

∀U, ZF_closed U → ∀x ∈ U, ordsucc x ∈ U

Proof:

An exact proof term for the current goal is (λU C x H ⇒ ZF_binunion_closed U C x H {x} (ZF_Sing_closed U C x H)).

∎

Try to prove it yourself. Main Goal

Theorem. (nat_p_UnivOf_Empty) The following is provable:

∀n : set, nat_p n → n ∈ UnivOf Empty

Proof:

Apply nat_ind to the current goal.

We will prove 0 ∈ UnivOf Empty.

An exact proof term for the current goal is (UnivOf_In Empty).

Let n be given.

Assume Hn: nat_p n.

Assume IHn: n ∈ UnivOf Empty.

We will prove ordsucc n ∈ UnivOf Empty.

An exact proof term for the current goal is (ZF_ordsucc_closed (UnivOf Empty) (UnivOf_ZF_closed Empty) n IHn).

∎

Try to prove it yourself. Main Goal

Definition. We define ω to be {n ∈ UnivOf Empty|nat_p n} of type set.

Theorem. (omega_nat_p) The following is provable:

∀n ∈ ω, nat_p n

Proof:

An exact proof term for the current goal is (λn H ⇒ SepE2 (UnivOf Empty) nat_p n H).

∎

Try to prove it yourself. Main Goal

Theorem. (nat_p_omega) The following is provable:

∀n : set, nat_p n → n ∈ ω

Proof:

Let n be given.

Assume H: nat_p n.

We will prove n ∈ {n ∈ UnivOf Empty|nat_p n}.

Apply SepI to the current goal.

We will prove n ∈ UnivOf Empty.

An exact proof term for the current goal is (nat_p_UnivOf_Empty n H).

We will prove nat_p n.

An exact proof term for the current goal is H.

∎

Try to prove it yourself. Main Goal

Theorem. (omega_ordsucc) The following is provable:

∀n ∈ ω, ordsucc n ∈ ω

Proof:

Let n be given.

Assume Hn.

Apply nat_p_omega to the current goal.

Apply nat_ordsucc to the current goal.

Apply omega_nat_p to the current goal.

An exact proof term for the current goal is Hn.

∎

Try to prove it yourself. Main Goal

Definition. We define ordinal to be λalpha : set ⇒ TransSet alpha ∧ ∀beta ∈ alpha, TransSet beta of type set → prop.

Theorem. (ordinal_TransSet) The following is provable:

∀alpha : set, ordinal alpha → TransSet alpha

Proof:

An exact proof term for the current goal is (λalpha H ⇒ andEL (TransSet alpha) (∀beta ∈ alpha, TransSet beta) H).

∎

Try to prove it yourself. Main Goal

Theorem. (ordinal_Empty) The following is provable:

ordinal Empty

Proof:

We will prove TransSet Empty ∧ ∀x ∈ Empty, TransSet x.

Apply andI to the current goal.

Let x be given.

Assume Hx: x ∈ Empty.

We will prove False.

An exact proof term for the current goal is (EmptyE x Hx).

Let x be given.

Assume Hx: x ∈ Empty.

We will prove False.

An exact proof term for the current goal is (EmptyE x Hx).

∎

Try to prove it yourself. Main Goal

Theorem. (ordinal_Hered) The following is provable:

∀alpha : set, ordinal alpha → ∀beta ∈ alpha, ordinal beta

Proof:

Let alpha be given.

Assume H1: TransSet alpha ∧ ∀x ∈ alpha, TransSet x.

Let beta be given.

Assume H2: beta ∈ alpha.

We will prove TransSet beta ∧ ∀x ∈ beta, TransSet x.

Apply H1 to the current goal.

Assume H3: TransSet alpha.

Assume H4: ∀x ∈ alpha, TransSet x.

Apply andI to the current goal.

An exact proof term for the current goal is (H4 beta H2).

We will prove ∀x ∈ beta, TransSet x.

Let x be given.

Assume Hx: x ∈ beta.

We prove the intermediate claim L1: x ∈ alpha.

An exact proof term for the current goal is (H3 beta H2 x Hx).

We will prove TransSet x.

An exact proof term for the current goal is (H4 x L1).

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (TransSet_ordsucc) The following is provable:

∀X : set, TransSet X → TransSet (ordsucc X)

Proof:

Let X be given.

Assume H1: TransSet X.

Let x be given.

Assume H2: x ∈ ordsucc X.

Let y be given.

Assume H3: y ∈ x.

We will prove y ∈ ordsucc X.

Apply (ordsuccE X x H2) to the current goal.

Assume H4: x ∈ X.

Apply ordsuccI1 to the current goal.

We will prove y ∈ X.

An exact proof term for the current goal is (H1 x H4 y H3).

Assume H4: x = X.

Apply ordsuccI1 to the current goal.

We will prove y ∈ X.

rewrite the current goal using H4 (from right to left).

We will prove y ∈ x.

An exact proof term for the current goal is H3.

∎

Try to prove it yourself. Main Goal

Theorem. (ordinal_ordsucc) The following is provable:

∀alpha : set, ordinal alpha → ordinal (ordsucc alpha)

Proof:

Let alpha be given.

Assume H1: TransSet alpha ∧ ∀beta ∈ alpha, TransSet beta.

Apply H1 to the current goal.

Assume H2: TransSet alpha.

Assume H3: ∀beta ∈ alpha, TransSet beta.

We will prove TransSet (ordsucc alpha) ∧ ∀beta ∈ ordsucc alpha, TransSet beta.

Apply andI to the current goal.

An exact proof term for the current goal is (TransSet_ordsucc alpha H2).

Let beta be given.

Assume H4: beta ∈ ordsucc alpha.

We will prove TransSet beta.

Apply (ordsuccE alpha beta H4) to the current goal.

Assume H5: beta ∈ alpha.

An exact proof term for the current goal is (H3 beta H5).

Assume H5: beta = alpha.

rewrite the current goal using H5 (from left to right).

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (nat_p_ordinal) The following is provable:

∀n : set, nat_p n → ordinal n

Proof:

Apply nat_ind to the current goal.

We will prove ordinal 0.

An exact proof term for the current goal is ordinal_Empty.

Let n be given.

Assume Hn: nat_p n.

Assume IHn: ordinal n.

We will prove ordinal (ordsucc n).

An exact proof term for the current goal is (ordinal_ordsucc n IHn).

∎

Try to prove it yourself. Main Goal

Theorem. (ordinal_1) The following is provable:

ordinal 1

Proof:

An exact proof term for the current goal is nat_p_ordinal 1 nat_1.

∎

Try to prove it yourself. Main Goal

Theorem. (ordinal_2) The following is provable:

ordinal 2

Proof:

An exact proof term for the current goal is nat_p_ordinal 2 nat_2.

∎

Try to prove it yourself. Main Goal

Theorem. (omega_TransSet) The following is provable:

TransSet ω

Proof:

Let n be given.

Assume Hn: n ∈ ω.

Let m be given.

Assume Hm: m ∈ n.

We will prove m ∈ ω.

Apply nat_p_omega to the current goal.

We will prove nat_p m.

Apply (nat_p_trans n) to the current goal.

We will prove nat_p n.

An exact proof term for the current goal is (omega_nat_p n Hn).

We will prove m ∈ n.

An exact proof term for the current goal is Hm.

∎

Try to prove it yourself. Main Goal

Theorem. (omega_ordinal) The following is provable:

ordinal ω

Proof:

We will prove TransSet ω ∧ ∀n ∈ ω, TransSet n.

Apply andI to the current goal.

An exact proof term for the current goal is omega_TransSet.

Let n be given.

Assume Hn: n ∈ ω.

We will prove TransSet n.

Apply ordinal_TransSet to the current goal.

We will prove ordinal n.

Apply nat_p_ordinal to the current goal.

We will prove nat_p n.

An exact proof term for the current goal is (omega_nat_p n Hn).

∎

Try to prove it yourself. Main Goal

Theorem. (ordsucc_omega_ordinal) The following is provable:

ordinal (ordsucc ω)

Proof:

An exact proof term for the current goal is ordinal_ordsucc ω omega_ordinal.

∎

Try to prove it yourself. Main Goal

Theorem. (TransSet_ordsucc_In_Subq) The following is provable:

∀X : set, TransSet X → ∀x ∈ X, ordsucc x ⊆ X

Proof:

Let X be given.

Assume H1: TransSet X.

Let x be given.

Assume H2: x ∈ X.

Let y be given.

Assume H3: y ∈ ordsucc x.

We will prove y ∈ X.

Apply (ordsuccE x y H3) to the current goal.

Assume H4: y ∈ x.

An exact proof term for the current goal is (H1 x H2 y H4).

Assume H4: y = x.

rewrite the current goal using H4 (from left to right).

We will prove x ∈ X.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (ordinal_ordsucc_In_Subq) The following is provable:

∀alpha, ordinal alpha → ∀beta ∈ alpha, ordsucc beta ⊆ alpha

Proof:

Let alpha be given.

Assume H: ordinal alpha.

An exact proof term for the current goal is (TransSet_ordsucc_In_Subq alpha (ordinal_TransSet alpha H)).

∎

Try to prove it yourself. Main Goal

Theorem. (ordinal_trichotomy_or) The following is provable:

∀alpha beta : set, ordinal alpha → ordinal beta → alpha ∈ beta ∨ alpha = beta ∨ beta ∈ alpha

Proof:

Apply In_ind to the current goal.

Let alpha be given.

Assume IHalpha: ∀gamma ∈ alpha, ∀beta : set, ordinal gamma → ordinal beta → gamma ∈ beta ∨ gamma = beta ∨ beta ∈ gamma.

We will prove ∀beta : set, ordinal alpha → ordinal beta → alpha ∈ beta ∨ alpha = beta ∨ beta ∈ alpha.

Apply In_ind to the current goal.

Let beta be given.

Assume IHbeta: ∀delta ∈ beta, ordinal alpha → ordinal delta → alpha ∈ delta ∨ alpha = delta ∨ delta ∈ alpha.

Assume Halpha: ordinal alpha.

Assume Hbeta: ordinal beta.

We will prove alpha ∈ beta ∨ alpha = beta ∨ beta ∈ alpha.

Apply (xm (alpha ∈ beta)) to the current goal.

Assume H1: alpha ∈ beta.

Apply or3I1 to the current goal.

An exact proof term for the current goal is H1.

Assume H1: alpha ∉ beta.

Apply (xm (beta ∈ alpha)) to the current goal.

Assume H2: beta ∈ alpha.

Apply or3I3 to the current goal.

An exact proof term for the current goal is H2.

Assume H2: beta ∉ alpha.

Apply or3I2 to the current goal.

We will prove alpha = beta.

Apply set_ext to the current goal.

We will prove alpha ⊆ beta.

Let gamma be given.

Assume H3: gamma ∈ alpha.

We will prove gamma ∈ beta.

We prove the intermediate claim Lgamma: ordinal gamma.

An exact proof term for the current goal is (ordinal_Hered alpha Halpha gamma H3).

Apply (or3E (gamma ∈ beta) (gamma = beta) (beta ∈ gamma) (IHalpha gamma H3 beta Lgamma Hbeta)) to the current goal.

Assume H4: gamma ∈ beta.

An exact proof term for the current goal is H4.

Assume H4: gamma = beta.

We will prove False.

Apply H2 to the current goal.

We will prove beta ∈ alpha.

rewrite the current goal using H4 (from right to left).

An exact proof term for the current goal is H3.

Assume H4: beta ∈ gamma.

We will prove False.

Apply H2 to the current goal.

We will prove beta ∈ alpha.

An exact proof term for the current goal is (ordinal_TransSet alpha Halpha gamma H3 beta H4).

We will prove beta ⊆ alpha.

Let delta be given.

Assume H3: delta ∈ beta.

We will prove delta ∈ alpha.

We prove the intermediate claim Ldelta: ordinal delta.

An exact proof term for the current goal is (ordinal_Hered beta Hbeta delta H3).

Apply (or3E (alpha ∈ delta) (alpha = delta) (delta ∈ alpha) (IHbeta delta H3 Halpha Ldelta)) to the current goal.

Assume H4: alpha ∈ delta.

We will prove False.

Apply H1 to the current goal.

We will prove alpha ∈ beta.

An exact proof term for the current goal is (ordinal_TransSet beta Hbeta delta H3 alpha H4).

Assume H4: alpha = delta.

We will prove False.

Apply H1 to the current goal.

We will prove alpha ∈ beta.

rewrite the current goal using H4 (from left to right).

An exact proof term for the current goal is H3.

Assume H4: delta ∈ alpha.

An exact proof term for the current goal is H4.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Theorem. (ordinal_trichotomy_or_impred) The following is provable:

∀alpha beta : set, ordinal alpha → ordinal beta → ∀p : prop, (alpha ∈ beta → p) → (alpha = beta → p) → (beta ∈ alpha → p) → p

Proof:

Let alpha and beta be given.

Assume H1 H2.

An exact proof term for the current goal is (or3E (alpha ∈ beta) (alpha = beta) (beta ∈ alpha) (ordinal_trichotomy_or alpha beta H1 H2)).

∎

Try to prove it yourself. Main Goal

Theorem. (ordinal_In_Or_Subq) The following is provable:

∀alpha beta, ordinal alpha → ordinal beta → alpha ∈ beta ∨ beta ⊆ alpha

Proof:

Let alpha and beta be given.

Assume H1: ordinal alpha.

Assume H2: ordinal beta.

Apply (or3E (alpha ∈ beta) (alpha = beta) (beta ∈ alpha) (ordinal_trichotomy_or alpha beta H1 H2)) to the current goal.

Assume H3: alpha ∈ beta.

Apply orIL to the current goal.

An exact proof term for the current goal is H3.

Assume H3: alpha = beta.

Apply orIR to the current goal.

rewrite the current goal using H3 (from left to right).

Apply Subq_ref to the current goal.

Assume H3: beta ∈ alpha.

Apply orIR to the current goal.

An exact proof term for the current goal is (ordinal_TransSet alpha H1 beta H3).

∎

Try to prove it yourself. Main Goal

Theorem. (ordinal_linear) The following is provable:

∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta ∨ beta ⊆ alpha

Proof:

Let alpha and beta be given.

Assume H1: ordinal alpha.

Assume H2: ordinal beta.

Apply (ordinal_In_Or_Subq alpha beta H1 H2) to the current goal.

Assume H3: alpha ∈ beta.

Apply orIL to the current goal.

An exact proof term for the current goal is (ordinal_TransSet beta H2 alpha H3).

Assume H3: beta ⊆ alpha.

Apply orIR to the current goal.

An exact proof term for the current goal is H3.

∎

Try to prove it yourself. Main Goal

Theorem. (ordinal_ordsucc_In_eq) The following is provable:

∀alpha beta, ordinal alpha → beta ∈ alpha → ordsucc beta ∈ alpha ∨ alpha = ordsucc beta

Proof:

Let alpha and beta be given.

Assume Ha Hb.

We prove the intermediate claim L1: ordinal (ordsucc beta).

An exact proof term for the current goal is ordinal_ordsucc beta (ordinal_Hered alpha Ha beta Hb).

Apply ordinal_trichotomy_or alpha (ordsucc beta) Ha L1 to the current goal.

Assume H1.

Apply H1 to the current goal.

Assume H2: alpha ∈ ordsucc beta.

We will prove False.

Apply ordsuccE beta alpha H2 to the current goal.

Assume H3: alpha ∈ beta.

An exact proof term for the current goal is In_no2cycle alpha beta H3 Hb.

Assume H3: alpha = beta.

Apply In_irref alpha to the current goal.

rewrite the current goal using H3 (from left to right) at position 1.

An exact proof term for the current goal is Hb.

Assume H2: alpha = ordsucc beta.

Apply orIR to the current goal.

An exact proof term for the current goal is H2.

Assume H2: ordsucc beta ∈ alpha.

Apply orIL to the current goal.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (ordinal_lim_or_succ) The following is provable:

∀alpha, ordinal alpha → (∀beta ∈ alpha, ordsucc beta ∈ alpha) ∨ (∃beta ∈ alpha, alpha = ordsucc beta)

Proof:

Let alpha be given.

Assume Ha.

Apply xm (∃beta ∈ alpha, alpha = ordsucc beta) to the current goal.

Assume H1.

Apply orIR to the current goal.

An exact proof term for the current goal is H1.

Assume H1: ¬ ∃beta ∈ alpha, alpha = ordsucc beta.

Apply orIL to the current goal.

Let beta be given.

Assume H2: beta ∈ alpha.

Apply ordinal_ordsucc_In_eq alpha beta Ha H2 to the current goal.

Assume H3: ordsucc beta ∈ alpha.

An exact proof term for the current goal is H3.

Assume H3: alpha = ordsucc beta.

We will prove False.

Apply H1 to the current goal.

We use beta to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H2.

An exact proof term for the current goal is H3.

∎

Try to prove it yourself. Main Goal

Theorem. (ordinal_ordsucc_In) The following is provable:

∀alpha, ordinal alpha → ∀beta ∈ alpha, ordsucc beta ∈ ordsucc alpha

Proof:

Let alpha be given.

Assume Ha.

Let beta be given.

Assume Hb.

We prove the intermediate claim L1: ordsucc beta ⊆ alpha.

An exact proof term for the current goal is ordinal_ordsucc_In_Subq alpha Ha beta Hb.

Apply ordinal_In_Or_Subq (ordsucc beta) alpha (ordinal_ordsucc beta (ordinal_Hered alpha Ha beta Hb)) Ha to the current goal.

Assume H1: ordsucc beta ∈ alpha.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is H1.

Assume H1: alpha ⊆ ordsucc beta.

We prove the intermediate claim L2: ordsucc beta = alpha.

Apply set_ext to the current goal.

An exact proof term for the current goal is L1.

An exact proof term for the current goal is H1.

rewrite the current goal using L2 (from left to right).

Apply ordsuccI2 to the current goal.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Theorem. (ordinal_famunion) The following is provable:

∀X, ∀F : set → set, (∀x ∈ X, ordinal (F x)) → ordinal (⋃_{x ∈ X}F x)

Proof:

Let X and F be given.

Assume HXF.

We will prove TransSet (⋃_{x ∈ X}F x) ∧ ∀y ∈ (⋃_{x ∈ X}F x), TransSet y.

Apply andI to the current goal.

Let y be given.

Assume Hy: y ∈ ⋃_{x ∈ X}F x.

Apply famunionE X F y Hy to the current goal.

Let x be given.

Assume H1.

Apply H1 to the current goal.

Assume Hx: x ∈ X.

Assume Hy: y ∈ F x.

We will prove y ⊆ ⋃_{x ∈ X}F x.

We prove the intermediate claim LFx: ordinal (F x).

An exact proof term for the current goal is HXF x Hx.

Apply LFx to the current goal.

Assume HFx1 _.

Let z be given.

Assume Hz: z ∈ y.

We will prove z ∈ ⋃_{x ∈ X}F x.

We prove the intermediate claim LzFx: z ∈ F x.

An exact proof term for the current goal is HFx1 y Hy z Hz.

An exact proof term for the current goal is famunionI X F x z Hx LzFx.

Let y be given.

Assume Hy: y ∈ ⋃_{x ∈ X}F x.

We will prove TransSet y.

Apply famunionE X F y Hy to the current goal.

Let x be given.

Assume H1.

Apply H1 to the current goal.

Assume Hx: x ∈ X.

Assume Hy: y ∈ F x.

We prove the intermediate claim LFx: ordinal (F x).

An exact proof term for the current goal is HXF x Hx.

We prove the intermediate claim Ly: ordinal y.

An exact proof term for the current goal is ordinal_Hered (F x) LFx y Hy.

Apply Ly to the current goal.

Assume Hy1 _.

An exact proof term for the current goal is Hy1.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Main Goal

Theorem. (ordinal_binintersect) The following is provable:

∀alpha beta, ordinal alpha → ordinal beta → ordinal (alpha ∩ beta)

Proof:

Let alpha and beta be given.

Assume Ha Hb.

Apply Ha to the current goal.

Assume Ha1 _.

Apply Hb to the current goal.

Assume Hb1 _.

Apply ordinal_In_Or_Subq alpha beta Ha Hb to the current goal.

Assume H1: alpha ∈ beta.

rewrite the current goal using binintersect_Subq_eq_1 alpha beta (Hb1 alpha H1) (from left to right).

An exact proof term for the current goal is Ha.

Assume H1: beta ⊆ alpha.

rewrite the current goal using binintersect_com (from left to right).

rewrite the current goal using binintersect_Subq_eq_1 beta alpha H1 (from left to right).

An exact proof term for the current goal is Hb.

∎

Try to prove it yourself. Main Goal

Theorem. (ordinal_binunion) The following is provable:

∀alpha beta, ordinal alpha → ordinal beta → ordinal (alpha ∪ beta)

Proof:

Let alpha and beta be given.

Assume Ha Hb.

Apply Ha to the current goal.

Assume Ha1 _.

Apply Hb to the current goal.

Assume Hb1 _.

Apply ordinal_linear alpha beta Ha Hb to the current goal.

rewrite the current goal using Subq_binunion_eq (from left to right).

Assume H1: alpha ∪ beta = beta.

rewrite the current goal using H1 (from left to right).

An exact proof term for the current goal is Hb.

rewrite the current goal using Subq_binunion_eq (from left to right).

rewrite the current goal using binunion_com (from left to right).

Assume H1: alpha ∪ beta = alpha.

rewrite the current goal using H1 (from left to right).

An exact proof term for the current goal is Ha.

∎

Try to prove it yourself. Main Goal

Theorem. (ordinal_ind) The following is provable:

∀p : set → prop, (∀alpha, ordinal alpha → (∀beta ∈ alpha, p beta) → p alpha) → ∀alpha, ordinal alpha → p alpha

Proof:

Let p be given.

Assume H1: ∀alpha, ordinal alpha → (∀beta ∈ alpha, p beta) → p alpha.

Apply In_ind to the current goal.

Let alpha be given.

Assume IH: ∀beta ∈ alpha, ordinal beta → p beta.

Assume H2: ordinal alpha.

We will prove p alpha.

Apply (H1 alpha H2) to the current goal.

Let beta be given.

Assume H3: beta ∈ alpha.

We will prove p beta.

Apply (IH beta H3) to the current goal.

We will prove ordinal beta.

An exact proof term for the current goal is (ordinal_Hered alpha H2 beta H3).

∎

Try to prove it yourself. Main Goal

Theorem. (least_ordinal_ex) The following is provable:

∀p : set → prop, (∃alpha, ordinal alpha ∧ p alpha) → ∃alpha, ordinal alpha ∧ p alpha ∧ ∀beta ∈ alpha, ¬ p beta

Proof:

Let p be given.

Assume H1.

Apply dneg to the current goal.

Assume H2: ¬ ∃alpha, ordinal alpha ∧ p alpha ∧ ∀beta ∈ alpha, ¬ p beta.

We prove the intermediate claim L1: ∀alpha, ordinal alpha → ¬ p alpha.

Apply ordinal_ind to the current goal.

Let alpha be given.

Assume Ha.

Assume IH: ∀beta ∈ alpha, ¬ p beta.

Assume H3: p alpha.

Apply H2 to the current goal.

We use alpha to witness the existential quantifier.

Apply and3I to the current goal.

An exact proof term for the current goal is Ha.

An exact proof term for the current goal is H3.

An exact proof term for the current goal is IH.

Apply H1 to the current goal.

Let alpha be given.

Assume H1a.

Apply H1a to the current goal.

Assume Ha: ordinal alpha.

Assume Hp: p alpha.

An exact proof term for the current goal is L1 alpha Ha Hp.

∎

Try to prove it yourself. Subgoal 1 Main Goal

Definition. We define inj to be λX Y f ⇒ (∀u ∈ X, f u ∈ Y) ∧ (∀u v ∈ X, f u = f v → u = v) of type set → set → (set → set) → prop.

Definition. We define bij to be λX Y f ⇒ (∀u ∈ X, f u ∈ Y) ∧ (∀u v ∈ X, f u = f v → u = v) ∧ (∀w ∈ Y, ∃u ∈ X, f u = w) of type set → set → (set → set) → prop.

Theorem. (bijI) The following is provable:

∀X Y, ∀f : set → set, (∀u ∈ X, f u ∈ Y) → (∀u v ∈ X, f u = f v → u = v) → (∀w ∈ Y, ∃u ∈ X, f u = w) → bij X Y f

Proof:

Let X, Y and f be given.

Assume Hf1 Hf2 Hf3.

We will prove (∀u ∈ X, f u ∈ Y) ∧ (∀u v ∈ X, f u = f v → u = v) ∧ (∀w ∈ Y, ∃u ∈ X, f u = w).

Apply and3I to the current goal.

An exact proof term for the current goal is Hf1.

An exact proof term for the current goal is Hf2.

An exact proof term for the current goal is Hf3.

∎

Try to prove it yourself. Main Goal

Theorem. (bijE) The following is provable:

∀X Y, ∀f : set → set, bij X Y f → ∀p : prop, ((∀u ∈ X, f u ∈ Y) → (∀u v ∈ X, f u = f v → u = v) → (∀w ∈ Y, ∃u ∈ X, f u = w) → p) → p

Proof:

Let X, Y and f be given.

Assume Hf.

Let p be given.

Assume Hp.

Apply Hf to the current goal.

Assume Hf.

Apply Hf to the current goal.

Assume Hf1 Hf2 Hf3.

An exact proof term for the current goal is Hp Hf1 Hf2 Hf3.

∎

Try to prove it yourself. Main Goal

Definition. We define inv to be λX f ⇒ λy : set ⇒ Eps_i (λx ⇒ x ∈ X ∧ f x = y) of type set → (set → set) → set → set.

Theorem. (surj_rinv) The following is provable:

∀X Y, ∀f : set → set, (∀w ∈ Y, ∃u ∈ X, f u = w) → ∀y ∈ Y, inv X f y ∈ X ∧ f (inv X f y) = y

Proof:

Let X, Y and f be given.

Assume H1.

Let y be given.

Assume Hy: y ∈ Y.

Apply H1 y Hy to the current goal.

Let x be given.

Assume H2.

An exact proof term for the current goal is Eps_i_ax (λx ⇒ x ∈ X ∧ f x = y) x H2.

∎

Try to prove it yourself. Main Goal

Theorem. (inj_linv) The following is provable:

∀X, ∀f : set → set, (∀u v ∈ X, f u = f v → u = v) → ∀x ∈ X, inv X f (f x) = x

Proof:

Let X and f be given.

Assume H1.

Let x be given.

Assume Hx.

We prove the intermediate claim L1: inv X f (f x) ∈ X ∧ f (inv X f (f x)) = f x.

Apply Eps_i_ax (λx' ⇒ x' ∈ X ∧ f x' = f x) x to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is Hx.

Use reflexivity.

Apply L1 to the current goal.

Assume H2 H3.

An exact proof term for the current goal is H1 (inv X f (f x)) H2 x Hx H3.

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (bij_inv) The following is provable:

∀X Y, ∀f : set → set, bij X Y f → bij Y X (inv X f)

Proof:

Let X, Y and f be given.

Assume H1.

Apply H1 to the current goal.

Assume H2.

Apply H2 to the current goal.

Assume H3: ∀u ∈ X, f u ∈ Y.

Assume H4: ∀u v ∈ X, f u = f v → u = v.

Assume H5: ∀w ∈ Y, ∃u ∈ X, f u = w.

Set g to be the term λy ⇒ Eps_i (λx ⇒ x ∈ X ∧ f x = y) of type set → set.

We prove the intermediate claim L1: ∀y ∈ Y, g y ∈ X ∧ f (g y) = y.

An exact proof term for the current goal is surj_rinv X Y f H5.

We will prove (∀u ∈ Y, g u ∈ X) ∧ (∀u v ∈ Y, g u = g v → u = v) ∧ (∀w ∈ X, ∃u ∈ Y, g u = w).

Apply and3I to the current goal.

We will prove ∀u ∈ Y, g u ∈ X.

Let u be given.

Assume Hu.

Apply L1 u Hu to the current goal.

Assume H _.

An exact proof term for the current goal is H.

We will prove ∀u v ∈ Y, g u = g v → u = v.

Let u be given.

Assume Hu.

Let v be given.

Assume Hv H6.

We will prove u = v.

Apply L1 u Hu to the current goal.

Assume H7: g u ∈ X.

Assume H8: f (g u) = u.

Apply L1 v Hv to the current goal.

Assume H9: g v ∈ X.

Assume H10: f (g v) = v.

rewrite the current goal using H8 (from right to left).

rewrite the current goal using H10 (from right to left).

rewrite the current goal using H6 (from right to left).

Use reflexivity.

We will prove ∀w ∈ X, ∃u ∈ Y, g u = w.

Let w be given.

Assume Hw.

We prove the intermediate claim Lfw: f w ∈ Y.

An exact proof term for the current goal is H3 w Hw.

We use f w to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Lfw.

An exact proof term for the current goal is inj_linv X f H4 w Hw.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Theorem. (bij_id) The following is provable:

∀X, bij X X (λx ⇒ x)

Proof:

Let X be given.

We will prove (∀u ∈ X, u ∈ X) ∧ (∀u v ∈ X, u = v → u = v) ∧ (∀w ∈ X, ∃u ∈ X, u = w).

Apply and3I to the current goal.

An exact proof term for the current goal is (λu Hu ⇒ Hu).

An exact proof term for the current goal is (λu Hu v Hv H1 ⇒ H1).

Let w be given.

Assume Hw.

We use w to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hw.

Use reflexivity.

∎

Try to prove it yourself. Main Goal

Theorem. (bij_comp) The following is provable:

∀X Y Z : set, ∀f g : set → set, bij X Y f → bij Y Z g → bij X Z (λx ⇒ g (f x))

Proof:

Let X, Y, Z, f and g be given.

Assume Hf.

Apply Hf to the current goal.

Assume Hf12 Hf3.

Apply Hf12 to the current goal.

Assume Hf1 Hf2.

Assume Hg.

Apply Hg to the current goal.

Assume Hg12 Hg3.

Apply Hg12 to the current goal.

Assume Hg1 Hg2.

We will prove (∀u ∈ X, g (f u) ∈ Z) ∧ (∀u v ∈ X, g (f u) = g (f v) → u = v) ∧ (∀w ∈ Z, ∃u ∈ X, g (f u) = w).

Apply and3I to the current goal.

Let u be given.

Assume Hu: u ∈ X.

An exact proof term for the current goal is (Hg1 (f u) (Hf1 u Hu)).

Let u be given.

Assume Hu: u ∈ X.

Let v be given.

Assume Hv: v ∈ X.

Assume H1: g (f u) = g (f v).

We will prove u = v.

Apply Hf2 u Hu v Hv to the current goal.

We will prove f u = f v.

Apply Hg2 (f u) (Hf1 u Hu) (f v) (Hf1 v Hv) to the current goal.

We will prove g (f u) = g (f v).

An exact proof term for the current goal is H1.

Let w be given.

Assume Hw: w ∈ Z.

Apply Hg3 w Hw to the current goal.

Let y be given.

Assume Hy12.

Apply Hy12 to the current goal.

Assume Hy1: y ∈ Y.

Assume Hy2: g y = w.

Apply Hf3 y Hy1 to the current goal.

Let u be given.

Assume Hu12.

Apply Hu12 to the current goal.

Assume Hu1: u ∈ X.

Assume Hu2: f u = y.

We will prove ∃u ∈ X, g (f u) = w.

We use u to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hu1.

rewrite the current goal using Hu2 (from left to right).

An exact proof term for the current goal is Hy2.

∎

Try to prove it yourself. Main Goal

Definition. We define equip to be λX Y : set ⇒ ∃f : set → set, bij X Y f of type set → set → prop.

Theorem. (equip_ref) The following is provable:

∀X, equip X X

Proof:

Let X be given.

We will prove ∃f : set → set, bij X X f.

We use (λx : set ⇒ x) to witness the existential quantifier.

An exact proof term for the current goal is bij_id X.

∎

Try to prove it yourself. Main Goal

Theorem. (equip_sym) The following is provable:

∀X Y, equip X Y → equip Y X

Proof:

Let X and Y be given.

Assume H1.

Apply H1 to the current goal.

Let f be given.

Assume H2: bij X Y f.

We will prove ∃g : set → set, bij Y X g.

We use (inv X f) to witness the existential quantifier.

We will prove bij Y X (inv X f).

An exact proof term for the current goal is bij_inv X Y f H2.

∎

Try to prove it yourself. Main Goal

Theorem. (equip_tra) The following is provable:

∀X Y Z, equip X Y → equip Y Z → equip X Z

Proof:

Let X, Y and Z be given.

Assume H1 H2.

Apply H1 to the current goal.

Let f be given.

Assume H3: bij X Y f.

Apply H2 to the current goal.

Let g be given.

Assume H4: bij Y Z g.

We will prove ∃h : set → set, bij X Z h.

We use (λx : set ⇒ g (f x)) to witness the existential quantifier.

An exact proof term for the current goal is bij_comp X Y Z f g H3 H4.

∎

Try to prove it yourself. Main Goal

Theorem. (equip_0_Empty) The following is provable:

∀X, equip X 0 → X = 0

Proof:

Let X be given.

Assume H1.

Apply Empty_eq to the current goal.

Let x be given.

Assume Hx.

We will prove False.

Apply H1 to the current goal.

Let f be given.

Assume Hf: bij X 0 f.

Apply bijE X 0 f Hf to the current goal.

Assume Hf1: ∀x ∈ X, f x ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE (f x) (Hf1 x Hx).

∎

Try to prove it yourself. Main Goal

Schroeder Bernstein

Beginning of Section SchroederBernstein

Theorem. (KnasterTarski_set) The following is provable:

∀A, ∀F : set → set, (∀U ∈ 𝒫 A, F U ∈ 𝒫 A) → (∀U V ∈ 𝒫 A, U ⊆ V → F U ⊆ F V) → ∃Y ∈ 𝒫 A, F Y = Y

Proof:

Let A and F be given.

Assume H1 H2.

Set Y to be the term {u ∈ A|∀X ∈ 𝒫 A, F X ⊆ X → u ∈ X} of type set.

We prove the intermediate claim L1: Y ∈ 𝒫 A.

Apply Sep_In_Power to the current goal.

We prove the intermediate claim L2: F Y ∈ 𝒫 A.

An exact proof term for the current goal is H1 Y L1.

We prove the intermediate claim L3: ∀X ∈ 𝒫 A, F X ⊆ X → Y ⊆ X.

Let X be given.

Assume HX: X ∈ 𝒫 A.

Assume H3: F X ⊆ X.

Let y be given.

Assume Hy: y ∈ Y.

An exact proof term for the current goal is SepE2 A (λu ⇒ ∀X ∈ 𝒫 A, F X ⊆ X → u ∈ X) y Hy X HX H3.

We prove the intermediate claim L4: F Y ⊆ Y.

Let u be given.

Assume H3: u ∈ F Y.

We will prove u ∈ Y.

Apply SepI to the current goal.

We will prove u ∈ A.

An exact proof term for the current goal is PowerE A (F Y) L2 u H3.

Let X be given.

Assume HX: X ∈ 𝒫 A.

Assume H4: F X ⊆ X.

We will prove u ∈ X.

We prove the intermediate claim L4a: Y ⊆ X.

An exact proof term for the current goal is L3 X HX H4.

We prove the intermediate claim L4b: F Y ⊆ F X.

An exact proof term for the current goal is H2 Y L1 X HX L4a.

We will prove u ∈ X.

Apply H4 to the current goal.

We will prove u ∈ F X.

Apply L4b to the current goal.

An exact proof term for the current goal is H3.

We prove the intermediate claim L5: F (F Y) ⊆ F Y.

An exact proof term for the current goal is H2 (F Y) L2 Y L1 L4.

We use Y to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is L1.

Apply set_ext to the current goal.

An exact proof term for the current goal is L4.

We will prove Y ⊆ F Y.

Apply L3 to the current goal.

An exact proof term for the current goal is L2.

An exact proof term for the current goal is L5.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Subgoal 7 Main Goal

Theorem. (image_In_Power) The following is provable:

∀A B, ∀f : set → set, (∀x ∈ A, f x ∈ B) → ∀U ∈ 𝒫 A, {f x|x ∈ U} ∈ 𝒫 B

Proof:

Let A, B and f be given.

Assume Hf.

Let U be given.

Assume HU.

Apply PowerI to the current goal.

Let y be given.

Assume Hy: y ∈ {f x|x ∈ U}.

Apply ReplE_impred U f y Hy to the current goal.

Let x be given.

Assume Hx: x ∈ U.

Assume H1: y = f x.

rewrite the current goal using H1 (from left to right).

Apply Hf to the current goal.

We will prove x ∈ A.

Apply PowerE A U HU to the current goal.

An exact proof term for the current goal is Hx.

∎

Try to prove it yourself. Main Goal

Theorem. (image_monotone) The following is provable:

∀f : set → set, ∀U V, U ⊆ V → {f x|x ∈ U} ⊆ {f x|x ∈ V}

Proof:

Let f, U and V be given.

Assume HUV.

Let y be given.

Assume Hy: y ∈ {f x|x ∈ U}.

Apply ReplE_impred U f y Hy to the current goal.

Let x be given.

Assume Hx: x ∈ U.

Assume H1: y = f x.

rewrite the current goal using H1 (from left to right).

We will prove f x ∈ {f x|x ∈ V}.

Apply ReplI to the current goal.

Apply HUV to the current goal.

An exact proof term for the current goal is Hx.

∎

Try to prove it yourself. Main Goal

Theorem. (setminus_antimonotone) The following is provable:

∀A U V, U ⊆ V → A ∖ V ⊆ A ∖ U

Proof:

Let A, U and V be given.

Assume HUV.

Let x be given.

Assume Hx.

Apply setminusE A V x Hx to the current goal.

Assume H1 H2.

Apply setminusI to the current goal.

An exact proof term for the current goal is H1.

Assume H3: x ∈ U.

Apply H2 to the current goal.

We will prove x ∈ V.

An exact proof term for the current goal is HUV x H3.

∎

Try to prove it yourself. Main Goal

Theorem. (SchroederBernstein) The following is provable:

∀A B, ∀f g : set → set, inj A B f → inj B A g → equip A B

Proof:

Let A, B, f and g be given.

Assume Hf Hg.

Apply Hf to the current goal.

Assume Hf1 Hf2.

Apply Hg to the current goal.

Assume Hg1 Hg2.

Set F to be the term λX ⇒ {g y|y ∈ B ∖ {f x|x ∈ A ∖ X}} of type set → set.

We prove the intermediate claim L1: ∀U ∈ 𝒫 A, F U ∈ 𝒫 A.

Let U be given.

Assume HU.

We will prove {g y|y ∈ B ∖ {f x|x ∈ A ∖ U}} ∈ 𝒫 A.

Apply image_In_Power B A g Hg1 to the current goal.

We will prove B ∖ {f x|x ∈ A ∖ U} ∈ 𝒫 B.

Apply setminus_In_Power to the current goal.

We prove the intermediate claim L2: ∀U V ∈ 𝒫 A, U ⊆ V → F U ⊆ F V.

Let U be given.

Assume HU.

Let V be given.

Assume HV HUV.

We will prove {g y|y ∈ B ∖ {f x|x ∈ A ∖ U}} ⊆ {g y|y ∈ B ∖ {f x|x ∈ A ∖ V}}.

Apply image_monotone g to the current goal.

We will prove B ∖ {f x|x ∈ A ∖ U} ⊆ B ∖ {f x|x ∈ A ∖ V}.

Apply setminus_antimonotone to the current goal.

We will prove {f x|x ∈ A ∖ V} ⊆ {f x|x ∈ A ∖ U}.

Apply image_monotone f to the current goal.

We will prove A ∖ V ⊆ A ∖ U.

Apply setminus_antimonotone to the current goal.

An exact proof term for the current goal is HUV.

Apply KnasterTarski_set A F L1 L2 to the current goal.

Let Y be given.

Assume H1.

Apply H1 to the current goal.

Assume H1: Y ∈ 𝒫 A.

Assume H2: F Y = Y.

Set h to be the term λx ⇒ if x ∈ Y then inv B g x else f x of type set → set.

We will prove ∃f : set → set, bij A B f.

We use h to witness the existential quantifier.

Apply bijI to the current goal.

Let x be given.

Assume Hx.

We will prove (if x ∈ Y then inv B g x else f x) ∈ B.

Apply xm (x ∈ Y) to the current goal.

Assume H3: x ∈ Y.

rewrite the current goal using If_i_1 (x ∈ Y) (inv B g x) (f x) H3 (from left to right).

We will prove inv B g x ∈ B.

We prove the intermediate claim L1: x ∈ F Y.

rewrite the current goal using H2 (from left to right).

An exact proof term for the current goal is H3.

Apply ReplE_impred (B ∖ {f x|x ∈ A ∖ Y}) g x L1 to the current goal.

Let y be given.

Assume H4: y ∈ B ∖ {f x|x ∈ A ∖ Y}.

Assume H5: x = g y.

We prove the intermediate claim L2: y ∈ B.

An exact proof term for the current goal is setminusE1 B {f x|x ∈ A ∖ Y} y H4.

rewrite the current goal using H5 (from left to right).

We will prove inv B g (g y) ∈ B.

rewrite the current goal using inj_linv B g Hg2 y L2 (from left to right).

We will prove y ∈ B.

An exact proof term for the current goal is L2.

Assume H3: x ∉ Y.

rewrite the current goal using If_i_0 (x ∈ Y) (inv B g x) (f x) H3 (from left to right).

We will prove f x ∈ B.

Apply Hf1 to the current goal.

An exact proof term for the current goal is Hx.

Let x be given.

Assume Hx.

Let y be given.

Assume Hy.

We will prove (if x ∈ Y then inv B g x else f x) = (if y ∈ Y then inv B g y else f y) → x = y.

Apply xm (x ∈ Y) to the current goal.

Assume H3: x ∈ Y.

rewrite the current goal using If_i_1 (x ∈ Y) (inv B g x) (f x) H3 (from left to right).

We will prove inv B g x = (if y ∈ Y then inv B g y else f y) → x = y.

We prove the intermediate claim Lx: x ∈ F Y.

rewrite the current goal using H2 (from left to right).

An exact proof term for the current goal is H3.

Apply ReplE_impred (B ∖ {f x|x ∈ A ∖ Y}) g x Lx to the current goal.

Let z be given.

Assume Hz1: z ∈ B ∖ {f x|x ∈ A ∖ Y}.

Assume Hz2: x = g z.

Apply setminusE B {f x|x ∈ A ∖ Y} z Hz1 to the current goal.

Assume Hz1a Hz1b.

Apply xm (y ∈ Y) to the current goal.

Assume H4: y ∈ Y.

rewrite the current goal using If_i_1 (y ∈ Y) (inv B g y) (f y) H4 (from left to right).

We will prove inv B g x = inv B g y → x = y.

We prove the intermediate claim Ly: y ∈ F Y.

rewrite the current goal using H2 (from left to right).

An exact proof term for the current goal is H4.

Apply ReplE_impred (B ∖ {f x|x ∈ A ∖ Y}) g y Ly to the current goal.

Let w be given.

Assume Hw1: w ∈ B ∖ {f x|x ∈ A ∖ Y}.

Assume Hw2: y = g w.

rewrite the current goal using Hz2 (from left to right).

rewrite the current goal using Hw2 (from left to right).

rewrite the current goal using inj_linv B g Hg2 z Hz1a (from left to right).

rewrite the current goal using inj_linv B g Hg2 w (setminusE1 B {f x|x ∈ A ∖ Y} w Hw1) (from left to right).

Assume H5: z = w.

We will prove g z = g w.

Use f_equal.

An exact proof term for the current goal is H5.

Assume H4: y ∉ Y.

rewrite the current goal using If_i_0 (y ∈ Y) (inv B g y) (f y) H4 (from left to right).

We will prove inv B g x = f y → x = y.

rewrite the current goal using Hz2 (from left to right).

rewrite the current goal using inj_linv B g Hg2 z Hz1a (from left to right).

We will prove z = f y → g z = y.

Assume H5: z = f y.

We will prove False.

Apply Hz1b to the current goal.

We will prove z ∈ {f x|x ∈ A ∖ Y}.

rewrite the current goal using H5 (from left to right).

Apply ReplI to the current goal.

We will prove y ∈ A ∖ Y.

Apply setminusI to the current goal.

An exact proof term for the current goal is Hy.

An exact proof term for the current goal is H4.

Assume H3: x ∉ Y.

rewrite the current goal using If_i_0 (x ∈ Y) (inv B g x) (f x) H3 (from left to right).

We will prove f x = (if y ∈ Y then inv B g y else f y) → x = y.

Apply xm (y ∈ Y) to the current goal.

Assume H4: y ∈ Y.

rewrite the current goal using If_i_1 (y ∈ Y) (inv B g y) (f y) H4 (from left to right).

We will prove f x = inv B g y → x = y.

We prove the intermediate claim Ly: y ∈ F Y.

rewrite the current goal using H2 (from left to right).

An exact proof term for the current goal is H4.

Apply ReplE_impred (B ∖ {f x|x ∈ A ∖ Y}) g y Ly to the current goal.

Let w be given.

Assume Hw1: w ∈ B ∖ {f x|x ∈ A ∖ Y}.

Assume Hw2: y = g w.

Apply setminusE B {f x|x ∈ A ∖ Y} w Hw1 to the current goal.

Assume Hw1a Hw1b.

rewrite the current goal using Hw2 (from left to right).

rewrite the current goal using inj_linv B g Hg2 w Hw1a (from left to right).

Assume H5: f x = w.

We will prove False.

Apply Hw1b to the current goal.

We will prove w ∈ {f x|x ∈ A ∖ Y}.

rewrite the current goal using H5 (from right to left).

Apply ReplI to the current goal.

Apply setminusI to the current goal.

An exact proof term for the current goal is Hx.

An exact proof term for the current goal is H3.

Assume H4: y ∉ Y.

rewrite the current goal using If_i_0 (y ∈ Y) (inv B g y) (f y) H4 (from left to right).

We will prove f x = f y → x = y.

An exact proof term for the current goal is Hf2 x Hx y Hy.

Let w be given.

Assume Hw: w ∈ B.

Apply xm (w ∈ {f x|x ∈ A ∖ Y}) to the current goal.

Assume H3: w ∈ {f x|x ∈ A ∖ Y}.

Apply ReplE_impred (A ∖ Y) f w H3 to the current goal.

Let x be given.

Assume H4: x ∈ A ∖ Y.

Assume H5: w = f x.

Apply setminusE A Y x H4 to the current goal.

Assume H6: x ∈ A.

Assume H7: x ∉ Y.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H6.

We will prove (if x ∈ Y then inv B g x else f x) = w.

rewrite the current goal using If_i_0 (x ∈ Y) (inv B g x) (f x) H7 (from left to right).

Use symmetry.

An exact proof term for the current goal is H5.

Assume H3: w ∉ {f x|x ∈ A ∖ Y}.

We prove the intermediate claim Lgw: g w ∈ Y.

rewrite the current goal using H2 (from right to left).

We will prove g w ∈ F Y.

We will prove g w ∈ {g y|y ∈ B ∖ {f x|x ∈ A ∖ Y}}.

Apply ReplI to the current goal.

Apply setminusI to the current goal.

We will prove w ∈ B.

An exact proof term for the current goal is Hw.

We will prove w ∉ {f x|x ∈ A ∖ Y}.

An exact proof term for the current goal is H3.

We use (g w) to witness the existential quantifier.

Apply andI to the current goal.

We will prove g w ∈ A.

Apply Hg1 to the current goal.

An exact proof term for the current goal is Hw.

We will prove (if g w ∈ Y then inv B g (g w) else f (g w)) = w.

rewrite the current goal using If_i_1 (g w ∈ Y) (inv B g (g w)) (f (g w)) Lgw (from left to right).

An exact proof term for the current goal is inj_linv B g Hg2 w Hw.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Subgoal 7 Subgoal 8 Main Goal

End of Section SchroederBernstein

Pigeonhole Principle

Beginning of Section PigeonHole

Theorem. (PigeonHole_nat) The following is provable:

∀n, nat_p n → ∀f : set → set, (∀i ∈ ordsucc n, f i ∈ n) → ¬ (∀i j ∈ ordsucc n, f i = f j → i = j)

Proof:

Apply nat_ind (λn ⇒ ∀f : set → set, (∀i ∈ ordsucc n, f i ∈ n) → ¬ (∀i j ∈ ordsucc n, f i = f j → i = j)) to the current goal.

We will prove ∀f : set → set, (∀i ∈ 1, f i ∈ 0) → ¬ (∀i j ∈ 1, f i = f j → i = j).

Let f be given.

Assume H1.

Apply EmptyE (f 0) (H1 0 In_0_1) to the current goal.

Let n be given.

Assume Hn: nat_p n.

Assume IH: ∀f : set → set, (∀i ∈ ordsucc n, f i ∈ n) → ¬ (∀i j ∈ ordsucc n, f i = f j → i = j).

Let f be given.

Assume H1: ∀i ∈ ordsucc (ordsucc n), f i ∈ ordsucc n.

Assume H2: ∀i j ∈ ordsucc (ordsucc n), f i = f j → i = j.

Apply xm (∃i ∈ ordsucc (ordsucc n), f i = n) to the current goal.

Assume H3.

Apply H3 to the current goal.

Let k be given.

Assume Hk.

Apply Hk to the current goal.

Assume Hk1: k ∈ ordsucc (ordsucc n).

Assume Hk2: f k = n.

Set f' to be the term λi : set ⇒ if k ⊆ i then f (ordsucc i) else f i.

Apply IH f' to the current goal.

We will prove ∀i ∈ ordsucc n, f' i ∈ n.

Let i be given.

Assume Hi: i ∈ ordsucc n.

Apply xm (k ⊆ i) to the current goal.

Assume H4: k ⊆ i.

We will prove (if k ⊆ i then f (ordsucc i) else f i) ∈ n.

rewrite the current goal using If_i_1 (k ⊆ i) (f (ordsucc i)) (f i) H4 (from left to right).

We will prove f (ordsucc i) ∈ n.

We prove the intermediate claim L1: ordsucc i ∈ ordsucc (ordsucc n).

Apply nat_ordsucc_in_ordsucc to the current goal.

Apply nat_ordsucc to the current goal.

An exact proof term for the current goal is Hn.

An exact proof term for the current goal is Hi.

Apply ordsuccE n (f (ordsucc i)) (H1 (ordsucc i) L1) to the current goal.

Assume H5: f (ordsucc i) ∈ n.

An exact proof term for the current goal is H5.

Assume H5: f (ordsucc i) = n.

We will prove False.

Apply In_irref i to the current goal.

We will prove i ∈ i.

We prove the intermediate claim L2: k = ordsucc i.

Apply H2 to the current goal.

An exact proof term for the current goal is Hk1.

An exact proof term for the current goal is L1.

rewrite the current goal using H5 (from left to right).

An exact proof term for the current goal is Hk2.

We prove the intermediate claim L3: i ∈ k.

rewrite the current goal using L2 (from left to right).

Apply ordsuccI2 to the current goal.

An exact proof term for the current goal is H4 i L3.

Assume H4: ¬ (k ⊆ i).

We will prove (if k ⊆ i then f (ordsucc i) else f i) ∈ n.

rewrite the current goal using If_i_0 (k ⊆ i) (f (ordsucc i)) (f i) H4 (from left to right).

We will prove f i ∈ n.

Apply ordsuccE n (f i) (H1 i (ordsuccI1 (ordsucc n) i Hi)) to the current goal.

Assume H5: f i ∈ n.

An exact proof term for the current goal is H5.

Assume H5: f i = n.

We will prove False.

Apply H4 to the current goal.

We will prove k ⊆ i.

We prove the intermediate claim L2: k = i.

Apply H2 to the current goal.

An exact proof term for the current goal is Hk1.

An exact proof term for the current goal is ordsuccI1 (ordsucc n) i Hi.

rewrite the current goal using H5 (from left to right).

An exact proof term for the current goal is Hk2.

rewrite the current goal using L2 (from right to left).

An exact proof term for the current goal is (λx Hx ⇒ Hx).

We will prove ∀i j ∈ ordsucc n, f' i = f' j → i = j.

Let i be given.

Assume Hi.

Let j be given.

Assume Hj.

We will prove (if k ⊆ i then f (ordsucc i) else f i) = (if k ⊆ j then f (ordsucc j) else f j) → i = j.

We prove the intermediate claim Li1: i ∈ ordsucc (ordsucc n).

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is Hi.

We prove the intermediate claim Li2: ordsucc i ∈ ordsucc (ordsucc n).

Apply nat_ordsucc_in_ordsucc to the current goal.

Apply nat_ordsucc to the current goal.

An exact proof term for the current goal is Hn.

An exact proof term for the current goal is Hi.

We prove the intermediate claim Lj1: j ∈ ordsucc (ordsucc n).

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is Hj.

We prove the intermediate claim Lj2: ordsucc j ∈ ordsucc (ordsucc n).

Apply nat_ordsucc_in_ordsucc to the current goal.

Apply nat_ordsucc to the current goal.

An exact proof term for the current goal is Hn.

An exact proof term for the current goal is Hj.

Apply xm (k ⊆ i) to the current goal.

Assume H4: k ⊆ i.

rewrite the current goal using If_i_1 (k ⊆ i) (f (ordsucc i)) (f i) H4 (from left to right).

Apply xm (k ⊆ j) to the current goal.

Assume H5: k ⊆ j.

rewrite the current goal using If_i_1 (k ⊆ j) (f (ordsucc j)) (f j) H5 (from left to right).

We will prove f (ordsucc i) = f (ordsucc j) → i = j.

Assume H6.

Apply ordsucc_inj to the current goal.

We will prove ordsucc i = ordsucc j.

An exact proof term for the current goal is H2 (ordsucc i) Li2 (ordsucc j) Lj2 H6.

Assume H5: ¬ (k ⊆ j).

rewrite the current goal using If_i_0 (k ⊆ j) (f (ordsucc j)) (f j) H5 (from left to right).

We will prove f (ordsucc i) = f j → i = j.

Assume H6.

We will prove False.

We prove the intermediate claim L3: ordsucc i = j.

Apply H2 to the current goal.

An exact proof term for the current goal is Li2.

An exact proof term for the current goal is Lj1.

An exact proof term for the current goal is H6.

Apply H5 to the current goal.

rewrite the current goal using L3 (from right to left).

Let x be given.

Assume Hx: x ∈ k.

Apply ordsuccI1 to the current goal.

Apply H4 to the current goal.

An exact proof term for the current goal is Hx.

Assume H4: ¬ (k ⊆ i).

rewrite the current goal using If_i_0 (k ⊆ i) (f (ordsucc i)) (f i) H4 (from left to right).

Apply xm (k ⊆ j) to the current goal.

Assume H5: k ⊆ j.

rewrite the current goal using If_i_1 (k ⊆ j) (f (ordsucc j)) (f j) H5 (from left to right).

We will prove f i = f (ordsucc j) → i = j.

Assume H6.

We will prove False.

We prove the intermediate claim L3: i = ordsucc j.

Apply H2 to the current goal.

An exact proof term for the current goal is Li1.

An exact proof term for the current goal is Lj2.

An exact proof term for the current goal is H6.

Apply H4 to the current goal.

rewrite the current goal using L3 (from left to right).

Let x be given.

Assume Hx: x ∈ k.

Apply ordsuccI1 to the current goal.

Apply H5 to the current goal.

An exact proof term for the current goal is Hx.

Assume H5: ¬ (k ⊆ j).

rewrite the current goal using If_i_0 (k ⊆ j) (f (ordsucc j)) (f j) H5 (from left to right).

We will prove f i = f j → i = j.

Apply H2 to the current goal.

An exact proof term for the current goal is Li1.

An exact proof term for the current goal is Lj1.

Assume H3: ¬ (∃i ∈ ordsucc (ordsucc n), f i = n).

Apply IH f to the current goal.

We will prove ∀i ∈ ordsucc n, f i ∈ n.

Let i be given.

Assume Hi: i ∈ ordsucc n.

Apply ordsuccE n (f i) (H1 i (ordsuccI1 (ordsucc n) i Hi)) to the current goal.

Assume Hfi: f i ∈ n.

An exact proof term for the current goal is Hfi.

Assume Hfi: f i = n.

Apply H3 to the current goal.

We use i to witness the existential quantifier.

Apply andI to the current goal.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is Hi.

An exact proof term for the current goal is Hfi.

We will prove ∀i j ∈ ordsucc n, f i = f j → i = j.

Let i be given.

Assume Hi.

Let j be given.

Assume Hj.

Apply H2 to the current goal.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is Hi.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is Hj.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Subgoal 7 Subgoal 8 Subgoal 9 Subgoal 10 Main Goal

Theorem. (PigeonHole_nat_bij) The following is provable:

∀n, nat_p n → ∀f : set → set, (∀i ∈ n, f i ∈ n) → (∀i j ∈ n, f i = f j → i = j) → bij n n f

Proof:

Let n be given.

Assume Hn.

Let f be given.

Assume Hf1 Hf2.

We will prove (∀i ∈ n, f i ∈ n) ∧ (∀i j ∈ n, f i = f j → i = j) ∧ (∀j ∈ n, ∃i ∈ n, f i = j).

Apply and3I to the current goal.

An exact proof term for the current goal is Hf1.

An exact proof term for the current goal is Hf2.

Let j be given.

Assume Hj: j ∈ n.

Apply dneg to the current goal.

Assume H1: ¬ ∃i ∈ n, f i = j.

Set f' to be the term λi : set ⇒ if i = n then j else f i.

Apply PigeonHole_nat n Hn f' to the current goal.

We will prove ∀i ∈ ordsucc n, f' i ∈ n.

Let i be given.

Assume Hi.

We will prove (if i = n then j else f i) ∈ n.

Apply xm (i = n) to the current goal.

Assume H1: i = n.

rewrite the current goal using If_i_1 (i = n) j (f i) H1 (from left to right).

We will prove j ∈ n.

An exact proof term for the current goal is Hj.

Assume H1: i ≠ n.

rewrite the current goal using If_i_0 (i = n) j (f i) H1 (from left to right).

We will prove f i ∈ n.

Apply Hf1 to the current goal.

Apply ordsuccE n i Hi to the current goal.

Assume H2: i ∈ n.

An exact proof term for the current goal is H2.

Assume H2: i = n.

Apply H1 H2 to the current goal.

We will prove ∀i k ∈ ordsucc n, f' i = f' k → i = k.

Let i be given.

Assume Hi.

Let k be given.

Assume Hk.

We prove the intermediate claim Li: i ≠ n → i ∈ n.

Assume Hin: i ≠ n.

Apply ordsuccE n i Hi to the current goal.

Assume H2.

An exact proof term for the current goal is H2.

Assume H2.

Apply Hin H2 to the current goal.

We prove the intermediate claim Lk: k ≠ n → k ∈ n.

Assume Hkn: k ≠ n.

Apply ordsuccE n k Hk to the current goal.

Assume H2.

An exact proof term for the current goal is H2.

Assume H2.

Apply Hkn H2 to the current goal.

We will prove (if i = n then j else f i) = (if k = n then j else f k) → i = k.

Apply xm (i = n) to the current goal.

Assume H2: i = n.

Apply xm (k = n) to the current goal.

Assume H3: k = n.

Assume _.

rewrite the current goal using H3 (from left to right).

An exact proof term for the current goal is H2.

Assume H3: k ≠ n.

rewrite the current goal using If_i_1 (i = n) j (f i) H2 (from left to right).

rewrite the current goal using If_i_0 (k = n) j (f k) H3 (from left to right).

Assume H4: j = f k.

Apply H1 to the current goal.

We use k to witness the existential quantifier.

Apply andI to the current goal.

We will prove k ∈ n.

An exact proof term for the current goal is Lk H3.

Use symmetry.

An exact proof term for the current goal is H4.

Assume H2: i ≠ n.

Apply xm (k = n) to the current goal.

Assume H3: k = n.

rewrite the current goal using If_i_0 (i = n) j (f i) H2 (from left to right).

rewrite the current goal using If_i_1 (k = n) j (f k) H3 (from left to right).

Assume H4: f i = j.

Apply H1 to the current goal.

We use i to witness the existential quantifier.

Apply andI to the current goal.

We will prove i ∈ n.

An exact proof term for the current goal is Li H2.

An exact proof term for the current goal is H4.

Assume H3: k ≠ n.

rewrite the current goal using If_i_0 (i = n) j (f i) H2 (from left to right).

rewrite the current goal using If_i_0 (k = n) j (f k) H3 (from left to right).

We will prove f i = f k → i = k.

Apply Hf2 to the current goal.

We will prove i ∈ n.

An exact proof term for the current goal is Li H2.

We will prove k ∈ n.

An exact proof term for the current goal is Lk H3.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

End of Section PigeonHole

Finite Sets

Definition. We define finite to be λX ⇒ ∃n ∈ ω, equip X n of type set → prop.

Theorem. (finite_ind) The following is provable:

∀p : set → prop, p Empty → (∀X y, finite X → y ∉ X → p X → p (X ∪ {y})) → ∀X, finite X → p X

Proof:

Let p be given.

Assume H1 H2.

We prove the intermediate claim L1: ∀n, nat_p n → ∀X, equip X n → p X.

Apply nat_ind to the current goal.

Let X be given.

Assume H3: equip X 0.

rewrite the current goal using equip_0_Empty X H3 (from left to right).

An exact proof term for the current goal is H1.

Let n be given.

Assume Hn.

Assume IHn: ∀X, equip X n → p X.

Let X be given.

Assume H3: equip X (ordsucc n).

Apply equip_sym X (ordsucc n) H3 to the current goal.

Let f be given.

Assume Hf: bij (ordsucc n) X f.

Apply bijE (ordsucc n) X f Hf to the current goal.

Assume Hf1: ∀i ∈ ordsucc n, f i ∈ X.

Assume Hf2: ∀i j ∈ ordsucc n, f i = f j → i = j.

Assume Hf3: ∀x ∈ X, ∃i ∈ ordsucc n, f i = x.

Set Z to be the term {f i|i ∈ n}.

Set y to be the term f n.

We prove the intermediate claim L1a: X = Z ∪ {y}.

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ X.

Apply Hf3 x Hx to the current goal.

Let i be given.

Assume H.

Apply H to the current goal.

Assume Hi: i ∈ ordsucc n.

Assume H4: f i = x.

Apply ordsuccE n i Hi to the current goal.

Assume H5: i ∈ n.

Apply binunionI1 to the current goal.

We will prove x ∈ Z.

rewrite the current goal using H4 (from right to left).

We will prove f i ∈ Z.

Apply ReplI to the current goal.

An exact proof term for the current goal is H5.

Assume H5: i = n.

Apply binunionI2 to the current goal.

We will prove x ∈ {y}.

rewrite the current goal using H4 (from right to left).

rewrite the current goal using H5 (from left to right).

An exact proof term for the current goal is SingI (f n).

Let x be given.

Assume Hx: x ∈ Z ∪ {y}.

Apply binunionE Z {y} x Hx to the current goal.

Assume H4: x ∈ Z.

Apply ReplE_impred n f x H4 to the current goal.

Let i be given.

Assume Hi: i ∈ n.

Assume H5: x = f i.

We will prove x ∈ X.

rewrite the current goal using H5 (from left to right).

We will prove f i ∈ X.

An exact proof term for the current goal is Hf1 i (ordsuccI1 n i Hi).

Assume H4: x ∈ {y}.

rewrite the current goal using SingE y x H4 (from left to right).

We will prove f n ∈ X.

An exact proof term for the current goal is Hf1 n (ordsuccI2 n).

We prove the intermediate claim L1b: equip Z n.

Apply equip_sym to the current goal.

We will prove ∃f : set → set, bij n Z f.

We use f to witness the existential quantifier.

Apply bijI to the current goal.

Let i be given.

Assume Hi.

We will prove f i ∈ {f i|i ∈ n}.

Apply ReplI to the current goal.

An exact proof term for the current goal is Hi.

Let i be given.

Assume Hi.

Let j be given.

Assume Hj.

Apply Hf2 to the current goal.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is Hi.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is Hj.

Apply ReplE' to the current goal.

Let i be given.

Assume Hi: i ∈ n.

We will prove ∃i' ∈ n, f i' = f i.

We use i to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hi.

Use reflexivity.

rewrite the current goal using L1a (from left to right).

We will prove p (Z ∪ {y}).

Apply H2 Z y to the current goal.

We will prove finite Z.

We will prove ∃n ∈ ω, equip Z n.

We use n to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is nat_p_omega n Hn.

An exact proof term for the current goal is L1b.

We will prove y ∉ Z.

Assume H4: y ∈ Z.

Apply ReplE_impred n f y H4 to the current goal.

Let i be given.

Assume Hi: i ∈ n.

Assume H5: y = f i.

Apply In_irref n to the current goal.

We will prove n ∈ n.

rewrite the current goal using Hf2 n (ordsuccI2 n) i (ordsuccI1 n i Hi) H5 (from left to right) at position 1.

We will prove i ∈ n.

An exact proof term for the current goal is Hi.

We will prove p Z.

An exact proof term for the current goal is IHn Z L1b.

Let X be given.

Assume H3.

Apply H3 to the current goal.

Let n be given.

Assume H.

Apply H to the current goal.

Assume Hn: n ∈ ω.

Assume H4: equip X n.

An exact proof term for the current goal is L1 n (omega_nat_p n Hn) X H4.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Main Goal

Theorem. (finite_Empty) The following is provable:

finite 0

Proof:

We will prove ∃n ∈ ω, equip 0 n.

We use 0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is nat_p_omega 0 nat_0.

Apply equip_ref to the current goal.

∎

Try to prove it yourself. Main Goal

Theorem. (adjoin_finite) The following is provable:

∀X y, finite X → finite (X ∪ {y})

Proof:

Let X and y be given.

Assume H1.

Apply H1 to the current goal.

Let n be given.

Assume H.

Apply H to the current goal.

Assume Hn: n ∈ ω.

Assume H2: equip X n.

Apply equip_sym X n H2 to the current goal.

Let f be given.

Assume Hf: bij n X f.

Apply bijE n X f Hf to the current goal.

Assume Hf1: ∀i ∈ n, f i ∈ X.

Assume Hf2: ∀i j ∈ n, f i = f j → i = j.

Assume Hf3: ∀x ∈ X, ∃i ∈ n, f i = x.

Apply xm (y ∈ X) to the current goal.

Assume H3: y ∈ X.

We prove the intermediate claim L1: X ∪ {y} = X.

Apply set_ext to the current goal.

Let x be given.

Assume Hx.

Apply binunionE X {y} x Hx to the current goal.

Assume H4.

An exact proof term for the current goal is H4.

Assume H4: x ∈ {y}.

rewrite the current goal using SingE y x H4 (from left to right).

An exact proof term for the current goal is H3.

Apply binunion_Subq_1 to the current goal.

rewrite the current goal using L1 (from left to right).

An exact proof term for the current goal is H1.

Assume H3: y ∉ X.

We will prove ∃m ∈ ω, equip (X ∪ {y}) m.

We use ordsucc n to witness the existential quantifier.

Apply andI to the current goal.

Apply omega_ordsucc to the current goal.

An exact proof term for the current goal is Hn.

We will prove equip (X ∪ {y}) (ordsucc n).

Apply equip_sym to the current goal.

We will prove ∃g : set → set, bij (ordsucc n) (X ∪ {y}) g.

We prove the intermediate claim Lg: ∃g : set → set, (∀i ∈ n, g i = f i) ∧ g n = y.

We use (λi : set ⇒ if i ∈ n then f i else y) to witness the existential quantifier.

Apply andI to the current goal.

Let i be given.

Assume Hi.

An exact proof term for the current goal is If_i_1 (i ∈ n) (f i) y Hi.

An exact proof term for the current goal is If_i_0 (n ∈ n) (f n) y (In_irref n).

Apply Lg to the current goal.

Let g be given.

Assume H.

Apply H to the current goal.

Assume Hg1 Hg2.

We use g to witness the existential quantifier.

Apply bijI to the current goal.

We will prove ∀i ∈ ordsucc n, g i ∈ X ∪ {y}.

Let i be given.

Assume Hi.

Apply ordsuccE n i Hi to the current goal.

Assume H4: i ∈ n.

Apply binunionI1 to the current goal.

rewrite the current goal using Hg1 i H4 (from left to right).

We will prove f i ∈ X.

An exact proof term for the current goal is Hf1 i H4.

Assume H4: i = n.

Apply binunionI2 to the current goal.

rewrite the current goal using H4 (from left to right).

rewrite the current goal using Hg2 (from left to right).

Apply SingI to the current goal.

We will prove ∀i j ∈ ordsucc n, g i = g j → i = j.

Let i be given.

Assume Hi.

Let j be given.

Assume Hj.

Apply ordsuccE n i Hi to the current goal.

Assume H4: i ∈ n.

rewrite the current goal using Hg1 i H4 (from left to right).

Apply ordsuccE n j Hj to the current goal.

Assume H5: j ∈ n.

rewrite the current goal using Hg1 j H5 (from left to right).

An exact proof term for the current goal is Hf2 i H4 j H5.

Assume H5: j = n.

rewrite the current goal using H5 (from left to right).

rewrite the current goal using Hg2 (from left to right).

Assume H6: f i = y.

We will prove False.

Apply H3 to the current goal.

We will prove y ∈ X.

rewrite the current goal using H6 (from right to left).

An exact proof term for the current goal is Hf1 i H4.

Assume H4: i = n.

rewrite the current goal using H4 (from left to right).

rewrite the current goal using Hg2 (from left to right).

Apply ordsuccE n j Hj to the current goal.

Assume H5: j ∈ n.

rewrite the current goal using Hg1 j H5 (from left to right).

Assume H6: y = f j.

We will prove False.

Apply H3 to the current goal.

We will prove y ∈ X.

rewrite the current goal using H6 (from left to right).

An exact proof term for the current goal is Hf1 j H5.

Assume H5: j = n.

rewrite the current goal using H5 (from left to right).

Assume _.

We will prove n = n.

Use reflexivity.

We will prove ∀x ∈ X ∪ {y}, ∃i ∈ ordsucc n, g i = x.

Let x be given.

Assume Hx.

Apply binunionE X {y} x Hx to the current goal.

Assume H4: x ∈ X.

Apply Hf3 x H4 to the current goal.

Let i be given.

Assume H.

Apply H to the current goal.

Assume Hi: i ∈ n.

Assume H5: f i = x.

We use i to witness the existential quantifier.

Apply andI to the current goal.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is Hi.

We will prove g i = x.

rewrite the current goal using Hg1 i Hi (from left to right).

An exact proof term for the current goal is H5.

Assume H4: x ∈ {y}.

We use n to witness the existential quantifier.

Apply andI to the current goal.

Apply ordsuccI2 to the current goal.

We will prove g n = x.

rewrite the current goal using SingE y x H4 (from left to right).

An exact proof term for the current goal is Hg2.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Theorem. (binunion_finite) The following is provable:

∀X, finite X → ∀Y, finite Y → finite (X ∪ Y)

Proof:

Let X be given.

Assume HX.

Apply finite_ind to the current goal.

We will prove finite (X ∪ 0).

rewrite the current goal using binunion_idr X (from left to right).

An exact proof term for the current goal is HX.

Let Y and z be given.

Assume HY: finite Y.

Assume Hz: z ∉ Y.

Assume IH: finite (X ∪ Y).

We will prove finite (X ∪ (Y ∪ {z})).

rewrite the current goal using binunion_asso (from left to right).

We will prove finite ((X ∪ Y) ∪ {z}).

Apply adjoin_finite to the current goal.

An exact proof term for the current goal is IH.

∎

Try to prove it yourself. Main Goal

Theorem. (famunion_nat_finite) The following is provable:

∀X : set → set, ∀n, nat_p n → (∀i ∈ n, finite (X i)) → finite (⋃_{i ∈ n}X i)

Proof:

Let X be given.

Apply nat_ind to the current goal.

Assume _.

We will prove finite (⋃_{i ∈ 0}X i).

rewrite the current goal using famunion_Empty (from left to right).

An exact proof term for the current goal is finite_Empty.

Let n be given.

Assume Hn.

Assume IHn: (∀i ∈ n, finite (X i)) → finite (⋃_{i ∈ n}X i).

Assume H1: ∀i ∈ ordsucc n, finite (X i).

We will prove finite (⋃_{i ∈ ordsucc n}X i).

We prove the intermediate claim L1: (⋃_{i ∈ ordsucc n}X i) = (⋃_{i ∈ n}X i) ∪ X n.

Apply set_ext to the current goal.

Let z be given.

Assume Hz: z ∈ ⋃_{i ∈ ordsucc n}X i.

Apply famunionE_impred (ordsucc n) X z Hz to the current goal.

Let i be given.

Assume Hi: i ∈ ordsucc n.

Assume H2: z ∈ X i.

Apply ordsuccE n i Hi to the current goal.

Assume H3: i ∈ n.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is famunionI n X i z H3 H2.

Assume H3: i = n.

Apply binunionI2 to the current goal.

rewrite the current goal using H3 (from right to left).

An exact proof term for the current goal is H2.

Let z be given.

Apply binunionE' to the current goal.

Assume Hz.

Apply famunionE_impred n X z Hz to the current goal.

Let i be given.

Assume Hi: i ∈ n.

Assume H2: z ∈ X i.

Apply famunionI (ordsucc n) X i z to the current goal.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is Hi.

An exact proof term for the current goal is H2.

Assume Hz.

Apply famunionI (ordsucc n) X n z to the current goal.

Apply ordsuccI2 to the current goal.

An exact proof term for the current goal is Hz.

rewrite the current goal using L1 (from left to right).

We will prove finite ((⋃_{i ∈ n}X i) ∪ X n).

Apply binunion_finite to the current goal.

Apply IHn to the current goal.

Let i be given.

Assume Hi: i ∈ n.

Apply H1 to the current goal.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is Hi.

Apply H1 n to the current goal.

Apply ordsuccI2 to the current goal.

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (Subq_finite) The following is provable:

∀X, finite X → ∀Y, Y ⊆ X → finite Y

Proof:

Apply finite_ind to the current goal.

Let Y be given.

Assume H1: Y ⊆ 0.

We will prove finite Y.

rewrite the current goal using Empty_Subq_eq Y H1 (from left to right).

An exact proof term for the current goal is finite_Empty.

Let X and z be given.

Assume HX: finite X.

Assume Hz: z ∉ X.

Assume IH: ∀Y, Y ⊆ X → finite Y.

Let Y be given.

Assume H1: Y ⊆ X ∪ {z}.

We will prove finite Y.

Apply xm (z ∈ Y) to the current goal.

Assume H2: z ∈ Y.

We prove the intermediate claim L1: Y = (Y ∖ {z}) ∪ {z}.

Apply set_ext to the current goal.

Let w be given.

Assume Hw: w ∈ Y.

Apply xm (w ∈ {z}) to the current goal.

Assume H3: w ∈ {z}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is H3.

Assume H3: w ∉ {z}.

Apply binunionI1 to the current goal.

Apply setminusI to the current goal.

An exact proof term for the current goal is Hw.

An exact proof term for the current goal is H3.

Let w be given.

Assume Hw: w ∈ (Y ∖ {z}) ∪ {z}.

Apply binunionE (Y ∖ {z}) {z} w Hw to the current goal.

Assume H3: w ∈ Y ∖ {z}.

An exact proof term for the current goal is setminusE1 Y {z} w H3.

Assume H3: w ∈ {z}.

We will prove w ∈ Y.

rewrite the current goal using SingE z w H3 (from left to right).

An exact proof term for the current goal is H2.

rewrite the current goal using L1 (from left to right).

Apply adjoin_finite to the current goal.

We will prove finite (Y ∖ {z}).

Apply IH to the current goal.

Let y be given.

Assume Hy: y ∈ Y ∖ {z}.

Apply setminusE Y {z} y Hy to the current goal.

Assume Hy1: y ∈ Y.

Assume Hy2: y ∉ {z}.

We will prove y ∈ X.

Apply binunionE X {z} y (H1 y Hy1) to the current goal.

Assume H3: y ∈ X.

An exact proof term for the current goal is H3.

Assume H3: y ∈ {z}.

We will prove False.

Apply Hy2 to the current goal.

An exact proof term for the current goal is H3.

Assume H2: z ∉ Y.

Apply IH to the current goal.

Let y be given.

Assume Hy: y ∈ Y.

We will prove y ∈ X.

Apply binunionE X {z} y (H1 y Hy) to the current goal.

Assume H3: y ∈ X.

An exact proof term for the current goal is H3.

Assume H3: y ∈ {z}.

We will prove False.

Apply H2 to the current goal.

We will prove z ∈ Y.

rewrite the current goal using SingE z y H3 (from right to left).

An exact proof term for the current goal is Hy.

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (TransSet_In_ordsucc_Subq) The following is provable:

∀x y, TransSet y → x ∈ ordsucc y → x ⊆ y

Proof:

Let x and y be given.

Assume H1 H2.

Apply ordsuccE y x H2 to the current goal.

Assume H3: x ∈ y.

An exact proof term for the current goal is H1 x H3.

Assume H3: x = y.

rewrite the current goal using H3 (from left to right).

Apply Subq_ref to the current goal.

∎

Try to prove it yourself. Main Goal

Theorem. (exandE_i) The following is provable:

∀P Q : set → prop, (∃x, P x ∧ Q x) → ∀r : prop, (∀x, P x → Q x → r) → r

Proof:

Let P and Q be given.

Assume H1.

Let r be given.

Assume Hr.

Apply H1 to the current goal.

Let x be given.

Assume H2.

Apply H2 to the current goal.

An exact proof term for the current goal is Hr x.

∎

Try to prove it yourself. Main Goal

Theorem. (exandE_ii) The following is provable:

∀P Q : (set → set) → prop, (∃x : set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set, P x → Q x → p) → p

Proof:

Let P and Q be given.

Assume H.

Let p be given.

Assume Hp.

Apply H to the current goal.

Let x be given.

Assume H0.

Apply H0 to the current goal.

Assume H1 H2.

An exact proof term for the current goal is Hp x H1 H2.

∎

Try to prove it yourself. Main Goal

Theorem. (exandE_iii) The following is provable:

∀P Q : (set → set → set) → prop, (∃x : set → set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set → set, P x → Q x → p) → p

Proof:

Let P and Q be given.

Assume H.

Let p be given.

Assume Hp.

Apply H to the current goal.

Let x be given.

Assume H0.

Apply H0 to the current goal.

Assume H1 H2.

An exact proof term for the current goal is Hp x H1 H2.

∎

Try to prove it yourself. Main Goal

Theorem. (exandE_iiii) The following is provable:

∀P Q : (set → set → set → set) → prop, (∃x : set → set → set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set → set → set, P x → Q x → p) → p

Proof:

Let P and Q be given.

Assume H.

Let p be given.

Assume Hp.

Apply H to the current goal.

Let x be given.

Assume H0.

Apply H0 to the current goal.

Assume H1 H2.

An exact proof term for the current goal is Hp x H1 H2.

∎

Try to prove it yourself. Main Goal

Beginning of Section Descr_ii

Variable P : (set → set) → prop

Definition. We define Descr_ii to be λx : set ⇒ Eps_i (λy ⇒ ∀h : set → set, P h → h x = y) of type set → set.

Hypothesis Pex : ∃f : set → set, P f

Hypothesis Puniq : ∀f g : set → set, P f → P g → f = g

Theorem. (Descr_ii_prop) The following is provable:

P Descr_ii

Proof:

Apply Pex to the current goal.

Let f be given.

Assume Hf: P f.

We prove the intermediate claim L1: f = Descr_ii.

Apply func_ext set set to the current goal.

Let x be given.

We will prove f x = Descr_ii x.

We will prove f x = Eps_i (λy ⇒ ∀h : set → set, P h → h x = y).

We prove the intermediate claim L2: ∀h : set → set, P h → h x = f x.

Let h be given.

Assume Hh.

rewrite the current goal using Puniq f h Hf Hh (from left to right).

An exact proof term for the current goal is (λq H ⇒ H).

We prove the intermediate claim L3: ∀h : set → set, P h → h x = Descr_ii x.

An exact proof term for the current goal is Eps_i_ax (λy ⇒ ∀h : set → set, P h → h x = y) (f x) L2.

An exact proof term for the current goal is L3 f Hf.

rewrite the current goal using L1 (from right to left).

An exact proof term for the current goal is Hf.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Main Goal

End of Section Descr_ii

Beginning of Section Descr_iii

Variable P : (set → set → set) → prop

Definition. We define Descr_iii to be λx y : set ⇒ Eps_i (λz ⇒ ∀h : set → set → set, P h → h x y = z) of type set → set → set.

Hypothesis Pex : ∃f : set → set → set, P f

Hypothesis Puniq : ∀f g : set → set → set, P f → P g → f = g

Theorem. (Descr_iii_prop) The following is provable:

P Descr_iii

Proof:

Apply Pex to the current goal.

Let f be given.

Assume Hf: P f.

We prove the intermediate claim L1: f = Descr_iii.

Apply func_ext set (set → set) to the current goal.

Let x be given.

Apply func_ext set set to the current goal.

Let y be given.

We will prove f x y = Descr_iii x y.

We will prove f x y = Eps_i (λz ⇒ ∀h : set → set → set, P h → h x y = z).

We prove the intermediate claim L2: ∀h : set → set → set, P h → h x y = f x y.

Let h be given.

Assume Hh.

rewrite the current goal using Puniq f h Hf Hh (from left to right).

An exact proof term for the current goal is (λq H ⇒ H).

We prove the intermediate claim L3: ∀h : set → set → set, P h → h x y = Descr_iii x y.

An exact proof term for the current goal is Eps_i_ax (λz ⇒ ∀h : set → set → set, P h → h x y = z) (f x y) L2.

An exact proof term for the current goal is L3 f Hf.

rewrite the current goal using L1 (from right to left).

An exact proof term for the current goal is Hf.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Main Goal

End of Section Descr_iii

Beginning of Section Descr_Vo1

Variable P : Vo 1 → prop

Definition. We define Descr_Vo1 to be λx : set ⇒ ∀h : set → prop, P h → h x of type Vo 1.

Hypothesis Pex : ∃f : Vo 1, P f

Hypothesis Puniq : ∀f g : Vo 1, P f → P g → f = g

Theorem. (Descr_Vo1_prop) The following is provable:

P Descr_Vo1

Proof:

Apply Pex to the current goal.

Let f be given.

Assume Hf: P f.

We prove the intermediate claim L1: f = Descr_Vo1.

Apply func_ext set prop to the current goal.

Let x be given.

We will prove f x = Descr_Vo1 x.

Apply prop_ext_2 to the current goal.

Assume H1: f x.

Let h be given.

Assume Hh: P h.

We will prove h x.

rewrite the current goal using Puniq f h Hf Hh (from right to left).

An exact proof term for the current goal is H1.

Assume H1: Descr_Vo1 x.

An exact proof term for the current goal is H1 f Hf.

rewrite the current goal using L1 (from right to left).

An exact proof term for the current goal is Hf.

∎

Try to prove it yourself. Subgoal 1 Main Goal

End of Section Descr_Vo1

Beginning of Section If_ii

Variable p : prop

Variable f g : set → set

Definition. We define If_ii to be λx ⇒ if p then f x else g x of type set → set.

Theorem. (If_ii_1) The following is provable:

p → If_ii = f

Proof:

Assume H1.

Apply func_ext set set to the current goal.

Let x be given.

We will prove If_ii x = f x.

An exact proof term for the current goal is If_i_1 p (f x) (g x) H1.

∎

Try to prove it yourself. Main Goal

Theorem. (If_ii_0) The following is provable:

¬ p → If_ii = g

Proof:

Assume H1.

Apply func_ext set set to the current goal.

Let x be given.

We will prove If_ii x = g x.

An exact proof term for the current goal is If_i_0 p (f x) (g x) H1.

∎

Try to prove it yourself. Main Goal

End of Section If_ii

Beginning of Section If_iii

Variable p : prop

Variable f g : set → set → set

Definition. We define If_iii to be λx y ⇒ if p then f x y else g x y of type set → set → set.

Theorem. (If_iii_1) The following is provable:

p → If_iii = f

Proof:

Assume H1.

Apply func_ext set (set → set) to the current goal.

Let x be given.

Apply func_ext set set to the current goal.

Let y be given.

We will prove If_iii x y = f x y.

An exact proof term for the current goal is If_i_1 p (f x y) (g x y) H1.

∎

Try to prove it yourself. Main Goal

Theorem. (If_iii_0) The following is provable:

¬ p → If_iii = g

Proof:

Assume H1.

Apply func_ext set (set → set) to the current goal.

Let x be given.

Apply func_ext set set to the current goal.

Let y be given.

We will prove If_iii x y = g x y.

An exact proof term for the current goal is If_i_0 p (f x y) (g x y) H1.

∎

Try to prove it yourself. Main Goal

End of Section If_iii

Beginning of Section EpsilonRec_i

Variable F : set → (set → set) → set

Definition. We define In_rec_i_G to be λX Y ⇒ ∀R : set → set → prop, (∀X : set, ∀f : set → set, (∀x ∈ X, R x (f x)) → R X (F X f)) → R X Y of type set → set → prop.

Definition. We define In_rec_i to be λX ⇒ Eps_i (In_rec_i_G X) of type set → set.

Theorem. (In_rec_i_G_c) The following is provable:

∀X : set, ∀f : set → set, (∀x ∈ X, In_rec_i_G x (f x)) → In_rec_i_G X (F X f)

Proof:

Let X of type set be given.

Let f of type set → set be given.

Assume H1: ∀x ∈ X, In_rec_i_G x (f x).

We will prove In_rec_i_G X (F X f).

Let R of type set → set → prop be given.

Assume H2: ∀X : set, ∀f : set → set, (∀x ∈ X, R x (f x)) → R X (F X f).

We will prove R X (F X f).

Apply (H2 X f) to the current goal.

We will prove ∀x ∈ X, R x (f x).

Let x of type set be given.

Assume H3: x ∈ X.

We will prove R x (f x).

An exact proof term for the current goal is (H1 x H3 R H2).

∎

Try to prove it yourself. Main Goal

Theorem. (In_rec_i_G_inv) The following is provable:

∀X : set, ∀Y : set, In_rec_i_G X Y → ∃f : set → set, (∀x ∈ X, In_rec_i_G x (f x)) ∧ Y = F X f

Proof:

Let X and Y be given.

Assume H1: In_rec_i_G X Y.

Set R to be the term (λX : set ⇒ λY : set ⇒ ∃f : set → set, (∀x ∈ X, In_rec_i_G x (f x)) ∧ Y = F X f).

Apply (H1 R) to the current goal.

We will prove ∀Z : set, ∀g : set → set, (∀z ∈ Z, R z (g z)) → R Z (F Z g).

Let Z and g be given.

Assume IH: ∀z ∈ Z, ∃f : set → set, (∀x ∈ z, In_rec_i_G x (f x)) ∧ g z = F z f.

We will prove ∃f : set → set, (∀x ∈ Z, In_rec_i_G x (f x)) ∧ F Z g = F Z f.

We use g to witness the existential quantifier.

Apply andI to the current goal.

Let z be given.

Assume H2: z ∈ Z.

Apply (exandE_ii (λf ⇒ ∀x ∈ z, In_rec_i_G x (f x)) (λf ⇒ g z = F z f) (IH z H2)) to the current goal.

Let f of type set → set be given.

Assume H3: ∀x ∈ z, In_rec_i_G x (f x).

Assume H4: g z = F z f.

We will prove In_rec_i_G z (g z).

rewrite the current goal using H4 (from left to right).

We will prove In_rec_i_G z (F z f).

An exact proof term for the current goal is (In_rec_i_G_c z f H3).

Use reflexivity.

∎

Try to prove it yourself. Main Goal

Hypothesis Fr : ∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h

Theorem. (In_rec_i_G_f) The following is provable:

∀X : set, ∀Y Z : set, In_rec_i_G X Y → In_rec_i_G X Z → Y = Z

Proof:

Apply In_ind to the current goal.

Let X be given.

Assume IH: ∀x ∈ X, ∀y z : set, In_rec_i_G x y → In_rec_i_G x z → y = z.

Let Y and Z be given.

Assume H1: In_rec_i_G X Y.

Assume H2: In_rec_i_G X Z.

We will prove Y = Z.

We prove the intermediate claim L1: ∃f : set → set, (∀x ∈ X, In_rec_i_G x (f x)) ∧ Y = F X f.

An exact proof term for the current goal is (In_rec_i_G_inv X Y H1).

We prove the intermediate claim L2: ∃f : set → set, (∀x ∈ X, In_rec_i_G x (f x)) ∧ Z = F X f.

An exact proof term for the current goal is (In_rec_i_G_inv X Z H2).

Apply (exandE_ii (λf ⇒ ∀x ∈ X, In_rec_i_G x (f x)) (λf ⇒ Y = F X f) L1) to the current goal.

Let g be given.

Assume H3: ∀x ∈ X, In_rec_i_G x (g x).

Assume H4: Y = F X g.

Apply (exandE_ii (λf ⇒ ∀x ∈ X, In_rec_i_G x (f x)) (λf ⇒ Z = F X f) L2) to the current goal.

Let h be given.

Assume H5: ∀x ∈ X, In_rec_i_G x (h x).

Assume H6: Z = F X h.

We will prove Y = Z.

rewrite the current goal using H4 (from left to right).

rewrite the current goal using H6 (from left to right).

We will prove F X g = F X h.

Apply Fr to the current goal.

We will prove ∀x ∈ X, g x = h x.

Let x be given.

Assume H7: x ∈ X.

An exact proof term for the current goal is (IH x H7 (g x) (h x) (H3 x H7) (H5 x H7)).

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Theorem. (In_rec_i_G_In_rec_i) The following is provable:

∀X : set, In_rec_i_G X (In_rec_i X)

Proof:

Apply In_ind to the current goal.

Let X be given.

Assume IH: ∀x ∈ X, In_rec_i_G x (In_rec_i x).

We will prove In_rec_i_G X (In_rec_i X).

We will prove In_rec_i_G X (Eps_i (In_rec_i_G X)).

Apply (Eps_i_ax (In_rec_i_G X) (F X In_rec_i)) to the current goal.

We will prove In_rec_i_G X (F X In_rec_i).

An exact proof term for the current goal is (In_rec_i_G_c X In_rec_i IH).

∎

Try to prove it yourself. Main Goal

Theorem. (In_rec_i_G_In_rec_i_d) The following is provable:

∀X : set, In_rec_i_G X (F X In_rec_i)

Proof:

Let X and R be given.

Assume H1: ∀X : set, ∀f : set → set, (∀x ∈ X, R x (f x)) → R X (F X f).

Apply (H1 X In_rec_i) to the current goal.

Let x be given.

Assume _.

An exact proof term for the current goal is (In_rec_i_G_In_rec_i x R H1).

∎

Try to prove it yourself. Main Goal

Theorem. (In_rec_i_eq) The following is provable:

∀X : set, In_rec_i X = F X In_rec_i

Proof:

An exact proof term for the current goal is (λX : set ⇒ In_rec_i_G_f X (In_rec_i X) (F X In_rec_i) (In_rec_i_G_In_rec_i X) (In_rec_i_G_In_rec_i_d X)).

∎

Try to prove it yourself. Main Goal

End of Section EpsilonRec_i

Beginning of Section EpsilonRec_ii

Variable F : set → (set → (set → set)) → (set → set)

Definition. We define In_rec_G_ii to be λX Y ⇒ ∀R : set → (set → set) → prop, (∀X : set, ∀f : set → (set → set), (∀x ∈ X, R x (f x)) → R X (F X f)) → R X Y of type set → (set → set) → prop.

Definition. We define In_rec_ii to be λX ⇒ Descr_ii (In_rec_G_ii X) of type set → (set → set).

Theorem. (In_rec_G_ii_c) The following is provable:

∀X : set, ∀f : set → (set → set), (∀x ∈ X, In_rec_G_ii x (f x)) → In_rec_G_ii X (F X f)

Proof:

Let X of type set be given.

Let f of type set → (set → set) be given.

Assume H1: ∀x ∈ X, In_rec_G_ii x (f x).

We will prove In_rec_G_ii X (F X f).

Let R of type set → (set → set) → prop be given.

Assume H2: ∀X : set, ∀f : set → (set → set), (∀x ∈ X, R x (f x)) → R X (F X f).

We will prove R X (F X f).

Apply (H2 X f) to the current goal.

We will prove ∀x ∈ X, R x (f x).

Let x of type set be given.

Assume H3: x ∈ X.

We will prove R x (f x).

An exact proof term for the current goal is (H1 x H3 R H2).

∎

Try to prove it yourself. Main Goal

Theorem. (In_rec_G_ii_inv) The following is provable:

∀X : set, ∀Y : (set → set), In_rec_G_ii X Y → ∃f : set → (set → set), (∀x ∈ X, In_rec_G_ii x (f x)) ∧ Y = F X f

Proof:

Let X and Y be given.

Assume H1: In_rec_G_ii X Y.

Set R to be the term (λX : set ⇒ λY : (set → set) ⇒ ∃f : set → (set → set), (∀x ∈ X, In_rec_G_ii x (f x)) ∧ Y = F X f).

Apply (H1 R) to the current goal.

We will prove ∀Z : set, ∀g : set → (set → set), (∀z ∈ Z, R z (g z)) → R Z (F Z g).

Let Z and g be given.

Assume IH: ∀z ∈ Z, ∃f : set → (set → set), (∀x ∈ z, In_rec_G_ii x (f x)) ∧ g z = F z f.

We will prove ∃f : set → (set → set), (∀x ∈ Z, In_rec_G_ii x (f x)) ∧ F Z g = F Z f.

We use g to witness the existential quantifier.

Apply andI to the current goal.

Let z be given.

Assume H2: z ∈ Z.

Apply (exandE_iii (λf ⇒ ∀x ∈ z, In_rec_G_ii x (f x)) (λf ⇒ g z = F z f) (IH z H2)) to the current goal.

Let f of type set → (set → set) be given.

Assume H3: ∀x ∈ z, In_rec_G_ii x (f x).

Assume H4: g z = F z f.

We will prove In_rec_G_ii z (g z).

rewrite the current goal using H4 (from left to right).

We will prove In_rec_G_ii z (F z f).

An exact proof term for the current goal is (In_rec_G_ii_c z f H3).

An exact proof term for the current goal is (λq H ⇒ H).

∎

Try to prove it yourself. Main Goal

Hypothesis Fr : ∀X : set, ∀g h : set → (set → set), (∀x ∈ X, g x = h x) → F X g = F X h

Theorem. (In_rec_G_ii_f) The following is provable:

∀X : set, ∀Y Z : (set → set), In_rec_G_ii X Y → In_rec_G_ii X Z → Y = Z

Proof:

Apply In_ind to the current goal.

Let X be given.

Assume IH: ∀x ∈ X, ∀y z : (set → set), In_rec_G_ii x y → In_rec_G_ii x z → y = z.

Let Y and Z be given.

Assume H1: In_rec_G_ii X Y.

Assume H2: In_rec_G_ii X Z.

We will prove Y = Z.

We prove the intermediate claim L1: ∃f : set → (set → set), (∀x ∈ X, In_rec_G_ii x (f x)) ∧ Y = F X f.

An exact proof term for the current goal is (In_rec_G_ii_inv X Y H1).

We prove the intermediate claim L2: ∃f : set → (set → set), (∀x ∈ X, In_rec_G_ii x (f x)) ∧ Z = F X f.

An exact proof term for the current goal is (In_rec_G_ii_inv X Z H2).

Apply (exandE_iii (λf ⇒ ∀x ∈ X, In_rec_G_ii x (f x)) (λf ⇒ Y = F X f) L1) to the current goal.

Let g be given.

Assume H3: ∀x ∈ X, In_rec_G_ii x (g x).

Assume H4: Y = F X g.

Apply (exandE_iii (λf ⇒ ∀x ∈ X, In_rec_G_ii x (f x)) (λf ⇒ Z = F X f) L2) to the current goal.

Let h be given.

Assume H5: ∀x ∈ X, In_rec_G_ii x (h x).

Assume H6: Z = F X h.

We will prove Y = Z.

rewrite the current goal using H4 (from left to right).

rewrite the current goal using H6 (from left to right).

We will prove F X g = F X h.

Apply Fr to the current goal.

We will prove ∀x ∈ X, g x = h x.

Let x be given.

Assume H7: x ∈ X.

An exact proof term for the current goal is (IH x H7 (g x) (h x) (H3 x H7) (H5 x H7)).

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Theorem. (In_rec_G_ii_In_rec_ii) The following is provable:

∀X : set, In_rec_G_ii X (In_rec_ii X)

Proof:

Apply In_ind to the current goal.

Let X be given.

Assume IH: ∀x ∈ X, In_rec_G_ii x (In_rec_ii x).

We will prove In_rec_G_ii X (In_rec_ii X).

We will prove In_rec_G_ii X (Descr_ii (In_rec_G_ii X)).

Apply (Descr_ii_prop (In_rec_G_ii X)) to the current goal.

We use (F X In_rec_ii) to witness the existential quantifier.

We will prove In_rec_G_ii X (F X In_rec_ii).

An exact proof term for the current goal is (In_rec_G_ii_c X In_rec_ii IH).

An exact proof term for the current goal is In_rec_G_ii_f X.

∎

Try to prove it yourself. Main Goal

Theorem. (In_rec_G_ii_In_rec_ii_d) The following is provable:

∀X : set, In_rec_G_ii X (F X In_rec_ii)

Proof:

Let X and R be given.

Assume H1: ∀X : set, ∀f : set → (set → set), (∀x ∈ X, R x (f x)) → R X (F X f).

Apply (H1 X In_rec_ii) to the current goal.

Let x be given.

Assume _.

An exact proof term for the current goal is (In_rec_G_ii_In_rec_ii x R H1).

∎

Try to prove it yourself. Main Goal

Theorem. (In_rec_ii_eq) The following is provable:

∀X : set, In_rec_ii X = F X In_rec_ii

Proof:

An exact proof term for the current goal is (λX : set ⇒ In_rec_G_ii_f X (In_rec_ii X) (F X In_rec_ii) (In_rec_G_ii_In_rec_ii X) (In_rec_G_ii_In_rec_ii_d X)).

∎

Try to prove it yourself. Main Goal

End of Section EpsilonRec_ii

Beginning of Section EpsilonRec_iii

Variable F : set → (set → (set → set → set)) → (set → set → set)

Definition. We define In_rec_G_iii to be λX Y ⇒ ∀R : set → (set → set → set) → prop, (∀X : set, ∀f : set → (set → set → set), (∀x ∈ X, R x (f x)) → R X (F X f)) → R X Y of type set → (set → set → set) → prop.

Definition. We define In_rec_iii to be λX ⇒ Descr_iii (In_rec_G_iii X) of type set → (set → set → set).

Theorem. (In_rec_G_iii_c) The following is provable:

∀X : set, ∀f : set → (set → set → set), (∀x ∈ X, In_rec_G_iii x (f x)) → In_rec_G_iii X (F X f)

Proof:

Let X of type set be given.

Let f of type set → (set → set → set) be given.

Assume H1: ∀x ∈ X, In_rec_G_iii x (f x).

We will prove In_rec_G_iii X (F X f).

Let R of type set → (set → set → set) → prop be given.

Assume H2: ∀X : set, ∀f : set → (set → set → set), (∀x ∈ X, R x (f x)) → R X (F X f).

We will prove R X (F X f).

Apply (H2 X f) to the current goal.

We will prove ∀x ∈ X, R x (f x).

Let x of type set be given.

Assume H3: x ∈ X.

We will prove R x (f x).

An exact proof term for the current goal is (H1 x H3 R H2).

∎

Try to prove it yourself. Main Goal

Theorem. (In_rec_G_iii_inv) The following is provable:

∀X : set, ∀Y : (set → set → set), In_rec_G_iii X Y → ∃f : set → (set → set → set), (∀x ∈ X, In_rec_G_iii x (f x)) ∧ Y = F X f

Proof:

Let X and Y be given.

Assume H1: In_rec_G_iii X Y.

Set R to be the term (λX : set ⇒ λY : (set → set → set) ⇒ ∃f : set → (set → set → set), (∀x ∈ X, In_rec_G_iii x (f x)) ∧ Y = F X f).

Apply (H1 R) to the current goal.

We will prove ∀Z : set, ∀g : set → (set → set → set), (∀z ∈ Z, R z (g z)) → R Z (F Z g).

Let Z and g be given.

Assume IH: ∀z ∈ Z, ∃f : set → (set → set → set), (∀x ∈ z, In_rec_G_iii x (f x)) ∧ g z = F z f.

We will prove ∃f : set → (set → set → set), (∀x ∈ Z, In_rec_G_iii x (f x)) ∧ F Z g = F Z f.

We use g to witness the existential quantifier.

Apply andI to the current goal.

Let z be given.

Assume H2: z ∈ Z.

Apply (exandE_iiii (λf ⇒ ∀x ∈ z, In_rec_G_iii x (f x)) (λf ⇒ g z = F z f) (IH z H2)) to the current goal.

Let f of type set → (set → set → set) be given.

Assume H3: ∀x ∈ z, In_rec_G_iii x (f x).

Assume H4: g z = F z f.

We will prove In_rec_G_iii z (g z).

rewrite the current goal using H4 (from left to right).

We will prove In_rec_G_iii z (F z f).

An exact proof term for the current goal is (In_rec_G_iii_c z f H3).

An exact proof term for the current goal is (λq H ⇒ H).

∎

Try to prove it yourself. Main Goal

Hypothesis Fr : ∀X : set, ∀g h : set → (set → set → set), (∀x ∈ X, g x = h x) → F X g = F X h

Theorem. (In_rec_G_iii_f) The following is provable:

∀X : set, ∀Y Z : (set → set → set), In_rec_G_iii X Y → In_rec_G_iii X Z → Y = Z

Proof:

Apply In_ind to the current goal.

Let X be given.

Assume IH: ∀x ∈ X, ∀y z : (set → set → set), In_rec_G_iii x y → In_rec_G_iii x z → y = z.

Let Y and Z be given.

Assume H1: In_rec_G_iii X Y.

Assume H2: In_rec_G_iii X Z.

We will prove Y = Z.

We prove the intermediate claim L1: ∃f : set → (set → set → set), (∀x ∈ X, In_rec_G_iii x (f x)) ∧ Y = F X f.

An exact proof term for the current goal is (In_rec_G_iii_inv X Y H1).

We prove the intermediate claim L2: ∃f : set → (set → set → set), (∀x ∈ X, In_rec_G_iii x (f x)) ∧ Z = F X f.

An exact proof term for the current goal is (In_rec_G_iii_inv X Z H2).

Apply (exandE_iiii (λf ⇒ ∀x ∈ X, In_rec_G_iii x (f x)) (λf ⇒ Y = F X f) L1) to the current goal.

Let g be given.

Assume H3: ∀x ∈ X, In_rec_G_iii x (g x).

Assume H4: Y = F X g.

Apply (exandE_iiii (λf ⇒ ∀x ∈ X, In_rec_G_iii x (f x)) (λf ⇒ Z = F X f) L2) to the current goal.

Let h be given.

Assume H5: ∀x ∈ X, In_rec_G_iii x (h x).

Assume H6: Z = F X h.

We will prove Y = Z.

rewrite the current goal using H4 (from left to right).

rewrite the current goal using H6 (from left to right).

We will prove F X g = F X h.

Apply Fr to the current goal.

We will prove ∀x ∈ X, g x = h x.

Let x be given.

Assume H7: x ∈ X.

An exact proof term for the current goal is (IH x H7 (g x) (h x) (H3 x H7) (H5 x H7)).

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Theorem. (In_rec_G_iii_In_rec_iii) The following is provable:

∀X : set, In_rec_G_iii X (In_rec_iii X)

Proof:

Apply In_ind to the current goal.

Let X be given.

Assume IH: ∀x ∈ X, In_rec_G_iii x (In_rec_iii x).

We will prove In_rec_G_iii X (In_rec_iii X).

We will prove In_rec_G_iii X (Descr_iii (In_rec_G_iii X)).

Apply (Descr_iii_prop (In_rec_G_iii X)) to the current goal.

We use (F X In_rec_iii) to witness the existential quantifier.

We will prove In_rec_G_iii X (F X In_rec_iii).

An exact proof term for the current goal is (In_rec_G_iii_c X In_rec_iii IH).

An exact proof term for the current goal is In_rec_G_iii_f X.

∎

Try to prove it yourself. Main Goal

Theorem. (In_rec_G_iii_In_rec_iii_d) The following is provable:

∀X : set, In_rec_G_iii X (F X In_rec_iii)

Proof:

Let X and R be given.

Assume H1: ∀X : set, ∀f : set → (set → set → set), (∀x ∈ X, R x (f x)) → R X (F X f).

Apply (H1 X In_rec_iii) to the current goal.

Let x be given.

Assume _.

An exact proof term for the current goal is (In_rec_G_iii_In_rec_iii x R H1).

∎

Try to prove it yourself. Main Goal

Theorem. (In_rec_iii_eq) The following is provable:

∀X : set, In_rec_iii X = F X In_rec_iii

Proof:

An exact proof term for the current goal is (λX : set ⇒ In_rec_G_iii_f X (In_rec_iii X) (F X In_rec_iii) (In_rec_G_iii_In_rec_iii X) (In_rec_G_iii_In_rec_iii_d X)).

∎

Try to prove it yourself. Main Goal

End of Section EpsilonRec_iii

Beginning of Section NatRec

Variable z : set

Variable f : set → set → set

Let F : set → (set → set) → set ≝ λn g ⇒ if ⋃ n ∈ n then f (⋃ n) (g (⋃ n)) else z

Definition. We define nat_primrec to be In_rec_i F of type set → set.

Theorem. (nat_primrec_r) The following is provable:

∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h

Proof:

Let X, g and h be given.

Assume H1: ∀x ∈ X, g x = h x.

We will prove F X g = F X h.

Apply xm (⋃ X ∈ X) to the current goal.

Assume H2: (⋃ X ∈ X).

We will prove (if ⋃ X ∈ X then f (⋃ X) (g (⋃ X)) else z) = (if ⋃ X ∈ X then f (⋃ X) (h (⋃ X)) else z).

rewrite the current goal using (H1 (⋃ X) H2) (from left to right).

We will prove (if ⋃ X ∈ X then f (⋃ X) (h (⋃ X)) else z) = (if ⋃ X ∈ X then f (⋃ X) (h (⋃ X)) else z).

An exact proof term for the current goal is (λq H ⇒ H).

Assume H2: ¬ (⋃ X ∈ X).

We will prove (if ⋃ X ∈ X then f (⋃ X) (g (⋃ X)) else z) = (if ⋃ X ∈ X then f (⋃ X) (h (⋃ X)) else z).

We prove the intermediate claim L1: (if ⋃ X ∈ X then f (⋃ X) (g (⋃ X)) else z) = z.

An exact proof term for the current goal is (If_i_0 (⋃ X ∈ X) (f (⋃ X) (g (⋃ X))) z H2).

We prove the intermediate claim L2: (if ⋃ X ∈ X then f (⋃ X) (h (⋃ X)) else z) = z.

An exact proof term for the current goal is (If_i_0 (⋃ X ∈ X) (f (⋃ X) (h (⋃ X))) z H2).

rewrite the current goal using L2 (from left to right).

An exact proof term for the current goal is L1.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Theorem. (nat_primrec_0) The following is provable:

nat_primrec 0 = z

Proof:

We will prove (In_rec_i F 0 = z).

rewrite the current goal using (In_rec_i_eq F nat_primrec_r) (from left to right).

We will prove F 0 (In_rec_i F) = z.

We will prove (if ⋃ 0 ∈ 0 then f (⋃ 0) (In_rec_i F (⋃ 0)) else z) = z.

An exact proof term for the current goal is (If_i_0 (⋃ 0 ∈ 0) (f (⋃ 0) (In_rec_i F (⋃ 0))) z (EmptyE (⋃ 0))).

∎

Try to prove it yourself. Main Goal

Theorem. (nat_primrec_S) The following is provable:

∀n : set, nat_p n → nat_primrec (ordsucc n) = f n (nat_primrec n)

Proof:

Let n be given.

Assume Hn: nat_p n.

We will prove (In_rec_i F (ordsucc n) = f n (In_rec_i F n)).

rewrite the current goal using (In_rec_i_eq F nat_primrec_r) (from left to right) at position 1.

We will prove F (ordsucc n) (In_rec_i F) = f n (In_rec_i F n).

We will prove (if ⋃ (ordsucc n) ∈ ordsucc n then f (⋃ (ordsucc n)) (In_rec_i F (⋃ (ordsucc n))) else z) = f n (In_rec_i F n).

rewrite the current goal using (Union_ordsucc_eq n Hn) (from left to right).

We will prove (if n ∈ ordsucc n then f n (In_rec_i F n) else z) = f n (In_rec_i F n).

An exact proof term for the current goal is (If_i_1 (n ∈ ordsucc n) (f n (In_rec_i F n)) z (ordsuccI2 n)).

∎

Try to prove it yourself. Main Goal

End of Section NatRec

Beginning of Section NatArith

Definition. We define add_nat to be λn m : set ⇒ nat_primrec n (λ_ r ⇒ ordsucc r) m of type set → set → set.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.

Theorem. (add_nat_0R) The following is provable:

∀n : set, n + 0 = n

Proof:

Let n be given.

An exact proof term for the current goal is (nat_primrec_0 n (λ_ r ⇒ ordsucc r)).

∎

Try to prove it yourself. Main Goal

Theorem. (add_nat_SR) The following is provable:

∀n m : set, nat_p m → n + ordsucc m = ordsucc (n + m)

Proof:

Let n and m be given.

Assume Hm.

An exact proof term for the current goal is (nat_primrec_S n (λ_ r ⇒ ordsucc r) m Hm).

∎

Try to prove it yourself. Main Goal

Theorem. (add_nat_p) The following is provable:

∀n : set, nat_p n → ∀m : set, nat_p m → nat_p (n + m)

Proof:

Let n be given.

Assume Hn: nat_p n.

Apply nat_ind to the current goal.

We will prove nat_p (n + 0).

rewrite the current goal using (add_nat_0R n) (from left to right).

We will prove nat_p n.

An exact proof term for the current goal is Hn.

Let m be given.

Assume Hm: nat_p m.

Assume IHm: nat_p (n + m).

We will prove nat_p (n + ordsucc m).

rewrite the current goal using (add_nat_SR n m Hm) (from left to right).

We will prove nat_p (ordsucc (n + m)).

Apply nat_ordsucc to the current goal.

We will prove nat_p (n + m).

An exact proof term for the current goal is IHm.

∎

Try to prove it yourself. Main Goal

Theorem. (add_nat_1_1_2) The following is provable:

1 + 1 = 2

Proof:

Use symmetry.

We will prove ordsucc 1 = 1 + ordsucc 0.

rewrite the current goal using add_nat_SR 1 0 nat_0 (from left to right).

We will prove ordsucc 1 = ordsucc (1 + 0).

rewrite the current goal using add_nat_0R 1 (from left to right).

An exact proof term for the current goal is (λq H ⇒ H).

∎

Try to prove it yourself. Main Goal

Definition. We define mul_nat to be λn m : set ⇒ nat_primrec 0 (λ_ r ⇒ n + r) m of type set → set → set.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.

Theorem. (mul_nat_0R) The following is provable:

∀n : set, n * 0 = 0

Proof:

Let n be given.

An exact proof term for the current goal is (nat_primrec_0 0 (λ_ r ⇒ n + r)).

∎

Try to prove it yourself. Main Goal

Theorem. (mul_nat_SR) The following is provable:

∀n m : set, nat_p m → n * ordsucc m = n + n * m

Proof:

Let n and m be given.

Assume Hm.

An exact proof term for the current goal is (nat_primrec_S 0 (λ_ r ⇒ n + r) m Hm).

∎

Try to prove it yourself. Main Goal

Theorem. (mul_nat_p) The following is provable:

∀n : set, nat_p n → ∀m : set, nat_p m → nat_p (n * m)

Proof:

Let n be given.

Assume Hn: nat_p n.

Apply nat_ind to the current goal.

We will prove nat_p (n * 0).

rewrite the current goal using (mul_nat_0R n) (from left to right).

We will prove nat_p 0.

An exact proof term for the current goal is nat_0.

Let m be given.

Assume Hm: nat_p m.

Assume IHm: nat_p (n * m).

We will prove nat_p (n * ordsucc m).

rewrite the current goal using (mul_nat_SR n m Hm) (from left to right).

We will prove nat_p (n + n * m).

An exact proof term for the current goal is (add_nat_p n Hn (n * m) IHm).

∎

Try to prove it yourself. Main Goal

End of Section NatArith

Definition. We define Inj1 to be In_rec_i (λX f ⇒ {0} ∪ {f x|x ∈ X}) of type set → set.

Theorem. (Inj1_eq) The following is provable:

∀X : set, Inj1 X = {0} ∪ {Inj1 x|x ∈ X}

Proof:

We prove the intermediate claim L1: ∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → {0} ∪ {g x|x ∈ X} = {0} ∪ {h x|x ∈ X}.

Let X, g and h be given.

Assume H: ∀x ∈ X, g x = h x.

We prove the intermediate claim L1a: {g x|x ∈ X} = {h x|x ∈ X}.

An exact proof term for the current goal is (ReplEq_ext X g h H).

We will prove {0} ∪ {g x|x ∈ X} = {0} ∪ {h x|x ∈ X}.

rewrite the current goal using L1a (from left to right).

Use reflexivity.

An exact proof term for the current goal is (In_rec_i_eq (λX f ⇒ {0} ∪ {f x|x ∈ X}) L1).

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Theorem. (Inj1I1) The following is provable:

∀X : set, 0 ∈ Inj1 X

Proof:

Let X be given.

rewrite the current goal using (Inj1_eq X) (from left to right).

We will prove 0 ∈ {0} ∪ {Inj1 x|x ∈ X}.

Apply binunionI1 to the current goal.

Apply SingI to the current goal.

∎

Try to prove it yourself. Main Goal

Theorem. (Inj1I2) The following is provable:

∀X x : set, x ∈ X → Inj1 x ∈ Inj1 X

Proof:

Let X and x be given.

Assume H: x ∈ X.

rewrite the current goal using (Inj1_eq X) (from left to right).

We will prove Inj1 x ∈ {0} ∪ {Inj1 x|x ∈ X}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is (ReplI X Inj1 x H).

∎

Try to prove it yourself. Main Goal

Theorem. (Inj1E) The following is provable:

∀X y : set, y ∈ Inj1 X → y = 0 ∨ ∃x ∈ X, y = Inj1 x

Proof:

Let X and y be given.

rewrite the current goal using (Inj1_eq X) (from left to right).

Assume H1: y ∈ {0} ∪ {Inj1 x|x ∈ X}.

We will prove y = 0 ∨ ∃x ∈ X, y = Inj1 x.

Apply (binunionE {0} {Inj1 x|x ∈ X} y H1) to the current goal.

Assume H2: y ∈ {0}.

Apply orIL to the current goal.

An exact proof term for the current goal is (SingE 0 y H2).

Assume H2: y ∈ {Inj1 x|x ∈ X}.

Apply orIR to the current goal.

We will prove ∃x ∈ X, y = Inj1 x.

An exact proof term for the current goal is (ReplE X Inj1 y H2).

∎

Try to prove it yourself. Main Goal

Theorem. (Inj1NE1) The following is provable:

∀x : set, Inj1 x ≠ 0

Proof:

Let x be given.

Assume H1: Inj1 x = 0.

Apply (EmptyE 0) to the current goal.

We will prove 0 ∈ 0.

rewrite the current goal using H1 (from right to left) at position 2.

We will prove 0 ∈ Inj1 x.

An exact proof term for the current goal is (Inj1I1 x).

∎

Try to prove it yourself. Main Goal

Theorem. (Inj1NE2) The following is provable:

∀x : set, Inj1 x ∉ {0}

Proof:

Let x be given.

Assume H1: Inj1 x ∈ {0}.

An exact proof term for the current goal is (Inj1NE1 x (SingE 0 (Inj1 x) H1)).

∎

Try to prove it yourself. Main Goal

Definition. We define Inj0 to be λX ⇒ {Inj1 x|x ∈ X} of type set → set.

Theorem. (Inj0I) The following is provable:

∀X x : set, x ∈ X → Inj1 x ∈ Inj0 X

Proof:

An exact proof term for the current goal is (λX x H ⇒ ReplI X Inj1 x H).

∎

Try to prove it yourself. Main Goal

Theorem. (Inj0E) The following is provable:

∀X y : set, y ∈ Inj0 X → ∃x : set, x ∈ X ∧ y = Inj1 x

Proof:

An exact proof term for the current goal is (λX y H ⇒ ReplE X Inj1 y H).

∎

Try to prove it yourself. Main Goal

Definition. We define Unj to be In_rec_i (λX f ⇒ {f x|x ∈ X ∖ {0}}) of type set → set.

Theorem. (Unj_eq) The following is provable:

∀X : set, Unj X = {Unj x|x ∈ X ∖ {0}}

Proof:

We prove the intermediate claim L1: ∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → {g x|x ∈ X ∖ {0}} = {h x|x ∈ X ∖ {0}}.

Let X, g and h be given.

Assume H1: ∀x ∈ X, g x = h x.

We will prove {g x|x ∈ X ∖ {0}} = {h x|x ∈ X ∖ {0}}.

Apply (ReplEq_ext (X ∖ {0}) g h) to the current goal.

Let x be given.

Assume H2: x ∈ X ∖ {0}.

We will prove g x = h x.

Apply H1 to the current goal.

We will prove x ∈ X.

An exact proof term for the current goal is (setminusE1 X {0} x H2).

An exact proof term for the current goal is (In_rec_i_eq (λX f ⇒ {f x|x ∈ X ∖ {0}}) L1).

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (Unj_Inj1_eq) The following is provable:

∀X : set, Unj (Inj1 X) = X

Proof:

Apply In_ind to the current goal.

Let X be given.

Assume IH: ∀x ∈ X, Unj (Inj1 x) = x.

We will prove Unj (Inj1 X) = X.

rewrite the current goal using Unj_eq (from left to right).

We will prove {Unj x|x ∈ Inj1 X ∖ {0}} = X.

Apply set_ext to the current goal.

We will prove {Unj x|x ∈ Inj1 X ∖ {0}} ⊆ X.

Let x be given.

Assume H1: x ∈ {Unj x|x ∈ Inj1 X ∖ {0}}.

We will prove x ∈ X.

Apply (ReplE_impred (Inj1 X ∖ {0}) Unj x H1) to the current goal.

Let y be given.

Assume H2: y ∈ Inj1 X ∖ {0}.

Assume H3: x = Unj y.

rewrite the current goal using H3 (from left to right).

We will prove Unj y ∈ X.

Apply (setminusE (Inj1 X) {0} y H2) to the current goal.

Assume H4: y ∈ Inj1 X.

Assume H5: y ∉ {0}.

Apply (Inj1E X y H4) to the current goal.

Assume H6: y = 0.

We will prove False.

Apply H5 to the current goal.

rewrite the current goal using H6 (from left to right).

We will prove 0 ∈ {0}.

Apply SingI to the current goal.

Assume H6: ∃x ∈ X, y = Inj1 x.

Apply (exandE_i (λx ⇒ x ∈ X) (λx ⇒ y = Inj1 x) H6) to the current goal.

Let z be given.

Assume H7: z ∈ X.

Assume H8: y = Inj1 z.

rewrite the current goal using H8 (from left to right).

We will prove Unj (Inj1 z) ∈ X.

rewrite the current goal using (IH z H7) (from left to right).

We will prove z ∈ X.

An exact proof term for the current goal is H7.

We will prove X ⊆ {Unj x|x ∈ Inj1 X ∖ {0}}.

Let x be given.

Assume H1: x ∈ X.

We will prove x ∈ {Unj x|x ∈ Inj1 X ∖ {0}}.

rewrite the current goal using (IH x H1) (from right to left).

We will prove Unj (Inj1 x) ∈ {Unj x|x ∈ Inj1 X ∖ {0}}.

Apply (ReplI (Inj1 X ∖ {0}) Unj) to the current goal.

We will prove Inj1 x ∈ Inj1 X ∖ {0}.

Apply setminusI to the current goal.

An exact proof term for the current goal is (Inj1I2 X x H1).

We will prove Inj1 x ∉ {0}.

An exact proof term for the current goal is (Inj1NE2 x).

∎

Try to prove it yourself. Main Goal

Theorem. (Inj1_inj) The following is provable:

∀X Y : set, Inj1 X = Inj1 Y → X = Y

Proof:

Let X and Y be given.

Assume H1: Inj1 X = Inj1 Y.

We will prove X = Y.

rewrite the current goal using (Unj_Inj1_eq X) (from right to left).

rewrite the current goal using (Unj_Inj1_eq Y) (from right to left).

rewrite the current goal using H1 (from left to right).

Use reflexivity.

∎

Try to prove it yourself. Main Goal

Theorem. (Unj_Inj0_eq) The following is provable:

∀X : set, Unj (Inj0 X) = X

Proof:

Let X be given.

rewrite the current goal using (Unj_eq (Inj0 X)) (from left to right).

We will prove {Unj x|x ∈ Inj0 X ∖ {0}} = X.

Apply set_ext to the current goal.

We will prove {Unj x|x ∈ Inj0 X ∖ {0}} ⊆ X.

Let x be given.

Assume H1: x ∈ {Unj x|x ∈ Inj0 X ∖ {0}}.

We will prove x ∈ X.

Apply (ReplE_impred (Inj0 X ∖ {0}) Unj x H1) to the current goal.

Let y be given.

Assume H2: y ∈ Inj0 X ∖ {0}.

Assume H3: x = Unj y.

Apply (setminusE (Inj0 X) {0} y H2) to the current goal.

Assume H4: y ∈ {Inj1 x|x ∈ X}.

Assume H5: y ∉ {0}.

Apply (ReplE_impred X Inj1 y H4) to the current goal.

Let z be given.

Assume H6: z ∈ X.

Assume H7: y = Inj1 z.

We prove the intermediate claim L1: x = z.

rewrite the current goal using H3 (from left to right).

We will prove Unj y = z.

rewrite the current goal using H7 (from left to right).

We will prove Unj (Inj1 z) = z.

An exact proof term for the current goal is (Unj_Inj1_eq z).

We will prove x ∈ X.

rewrite the current goal using L1 (from left to right).

We will prove z ∈ X.

An exact proof term for the current goal is H6.

We will prove X ⊆ {Unj x|x ∈ Inj0 X ∖ {0}}.

Let x be given.

Assume H1: x ∈ X.

We will prove x ∈ {Unj x|x ∈ Inj0 X ∖ {0}}.

rewrite the current goal using (Unj_Inj1_eq x) (from right to left).

We will prove Unj (Inj1 x) ∈ {Unj x|x ∈ Inj0 X ∖ {0}}.

Apply (ReplI (Inj0 X ∖ {0}) Unj) to the current goal.

We will prove Inj1 x ∈ Inj0 X ∖ {0}.

Apply setminusI to the current goal.

We will prove Inj1 x ∈ {Inj1 x|x ∈ X}.

Apply ReplI to the current goal.

An exact proof term for the current goal is H1.

We will prove Inj1 x ∉ {0}.

An exact proof term for the current goal is (Inj1NE2 x).

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (Inj0_inj) The following is provable:

∀X Y : set, Inj0 X = Inj0 Y → X = Y

Proof:

Let X and Y be given.

Assume H1: Inj0 X = Inj0 Y.

We will prove X = Y.

rewrite the current goal using (Unj_Inj0_eq X) (from right to left).

rewrite the current goal using (Unj_Inj0_eq Y) (from right to left).

rewrite the current goal using H1 (from left to right).

Use reflexivity.

∎

Try to prove it yourself. Main Goal

Theorem. (Inj0_0) The following is provable:

Inj0 0 = 0

Proof:

An exact proof term for the current goal is (Repl_Empty Inj1).

∎

Try to prove it yourself. Main Goal

Theorem. (Inj0_Inj1_neq) The following is provable:

∀X Y : set, Inj0 X ≠ Inj1 Y

Proof:

Let X and Y be given.

Assume H1: Inj0 X = Inj1 Y.

We prove the intermediate claim L1: 0 ∈ Inj1 Y.

An exact proof term for the current goal is (Inj1I1 Y).

We prove the intermediate claim L2: 0 ∈ Inj0 X.

rewrite the current goal using H1 (from left to right).

An exact proof term for the current goal is L1.

Apply (Inj0E X 0 L2) to the current goal.

Let x be given.

Assume H2: x ∈ X ∧ 0 = Inj1 x.

Apply Inj1NE1 x to the current goal.

Use symmetry.

An exact proof term for the current goal is andER (x ∈ X) (0 = Inj1 x) H2.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Disjoint Sums, a.k.a. Ordered Pairs

Definition. We define setsum to be λX Y ⇒ {Inj0 x|x ∈ X} ∪ {Inj1 y|y ∈ Y} of type set → set → set.

Notation. We use + as an infix operator with priority 450 and which associates to the left corresponding to applying term setsum.

Theorem. (Inj0_setsum) The following is provable:

∀X Y x : set, x ∈ X → Inj0 x ∈ X + Y

Proof:

Let X, Y and x be given.

Assume H: x ∈ X.

We will prove Inj0 x ∈ {Inj0 x|x ∈ X} ∪ {Inj1 y|y ∈ Y}.

Apply binunionI1 to the current goal.

We will prove Inj0 x ∈ {Inj0 x|x ∈ X}.

Apply ReplI to the current goal.

An exact proof term for the current goal is H.

∎

Try to prove it yourself. Main Goal

Theorem. (Inj1_setsum) The following is provable:

∀X Y y : set, y ∈ Y → Inj1 y ∈ X + Y

Proof:

Let X, Y and y be given.

Assume H: y ∈ Y.

We will prove Inj1 y ∈ {Inj0 x|x ∈ X} ∪ {Inj1 y|y ∈ Y}.

Apply binunionI2 to the current goal.

We will prove Inj1 y ∈ {Inj1 y|y ∈ Y}.

Apply ReplI to the current goal.

An exact proof term for the current goal is H.

∎

Try to prove it yourself. Main Goal

Theorem. (setsum_Inj_inv) The following is provable:

∀X Y z : set, z ∈ X + Y → (∃x ∈ X, z = Inj0 x) ∨ (∃y ∈ Y, z = Inj1 y)

Proof:

Let X, Y and z be given.

Assume H1: z ∈ {Inj0 x|x ∈ X} ∪ {Inj1 y|y ∈ Y}.

Apply (binunionE {Inj0 x|x ∈ X} {Inj1 y|y ∈ Y} z H1) to the current goal.

Assume H2: z ∈ {Inj0 x|x ∈ X}.

Apply orIL to the current goal.

An exact proof term for the current goal is (ReplE X Inj0 z H2).

Assume H2: z ∈ {Inj1 y|y ∈ Y}.

Apply orIR to the current goal.

An exact proof term for the current goal is (ReplE Y Inj1 z H2).

∎

Try to prove it yourself. Main Goal

Theorem. (Inj0_setsum_0L) The following is provable:

∀X : set, 0 + X = Inj0 X

Proof:

Let X be given.

Apply set_ext to the current goal.

Let z be given.

Assume H1: z ∈ 0 + X.

We will prove z ∈ Inj0 X.

Apply (setsum_Inj_inv 0 X z H1) to the current goal.

Assume H2: ∃x ∈ 0, z = Inj0 x.

Apply (exandE_i (λx ⇒ x ∈ 0) (λx ⇒ z = Inj0 x) H2) to the current goal.

Let x be given.

Assume H3: x ∈ 0.

We will prove False.

An exact proof term for the current goal is (EmptyE x H3).

Assume H2: ∃x ∈ X, z = Inj1 x.

Apply (exandE_i (λx ⇒ x ∈ X) (λx ⇒ z = Inj1 x) H2) to the current goal.

Let x be given.

Assume H3: x ∈ X.

Assume H4: z = Inj1 x.

rewrite the current goal using H4 (from left to right).

We will prove Inj1 x ∈ Inj0 X.

An exact proof term for the current goal is (Inj0I X x H3).

Let z be given.

Assume H1: z ∈ Inj0 X.

We will prove z ∈ 0 + X.

Apply (exandE_i (λx ⇒ x ∈ X) (λx ⇒ z = Inj1 x) (Inj0E X z H1)) to the current goal.

Let x be given.

Assume H2: x ∈ X.

Assume H3: z = Inj1 x.

rewrite the current goal using H3 (from left to right).

We will prove Inj1 x ∈ 0 + X.

Apply Inj1_setsum to the current goal.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (Subq_1_Sing0) The following is provable:

1 ⊆ {0}

Proof:

Let x be given.

Assume H1: x ∈ 1.

We will prove x ∈ {0}.

Apply ordsuccE 0 x H1 to the current goal.

Assume H2: x ∈ 0.

We will prove False.

An exact proof term for the current goal is (EmptyE x H2).

Assume H2: x = 0.

rewrite the current goal using H2 (from left to right).

We will prove 0 ∈ {0}.

An exact proof term for the current goal is (SingI 0).

∎

Try to prove it yourself. Main Goal

Theorem. (Inj1_setsum_1L) The following is provable:

∀X : set, 1 + X = Inj1 X

Proof:

Let X be given.

Apply set_ext to the current goal.

Let z be given.

Assume H1: z ∈ 1 + X.

We will prove z ∈ Inj1 X.

Apply (setsum_Inj_inv 1 X z H1) to the current goal.

Assume H2: ∃x ∈ 1, z = Inj0 x.

Apply (exandE_i (λx ⇒ x ∈ 1) (λx ⇒ z = Inj0 x) H2) to the current goal.

Let x be given.

Assume H3: x ∈ 1.

Assume H4: z = Inj0 x.

rewrite the current goal using H4 (from left to right).

We will prove Inj0 x ∈ Inj1 X.

We prove the intermediate claim L1: x = 0.

An exact proof term for the current goal is (SingE 0 x (Subq_1_Sing0 x H3)).

rewrite the current goal using L1 (from left to right).

We will prove Inj0 0 ∈ Inj1 X.

rewrite the current goal using Inj0_0 (from left to right).

We will prove 0 ∈ Inj1 X.

An exact proof term for the current goal is (Inj1I1 X).

Assume H2: ∃x ∈ X, z = Inj1 x.

Apply (exandE_i (λx ⇒ x ∈ X) (λx ⇒ z = Inj1 x) H2) to the current goal.

Let x be given.

Assume H3: x ∈ X.

Assume H4: z = Inj1 x.

rewrite the current goal using H4 (from left to right).

We will prove Inj1 x ∈ Inj1 X.

An exact proof term for the current goal is (Inj1I2 X x H3).

Let z be given.

Assume H1: z ∈ Inj1 X.

We will prove z ∈ 1 + X.

Apply (Inj1E X z H1) to the current goal.

Assume H2: z = 0.

rewrite the current goal using H2 (from left to right).

We will prove 0 ∈ 1 + X.

rewrite the current goal using Inj0_0 (from right to left) at position 1.

We will prove Inj0 0 ∈ 1 + X.

Apply Inj0_setsum to the current goal.

We will prove 0 ∈ 1.

An exact proof term for the current goal is In_0_1.

Assume H2: ∃x ∈ X, z = Inj1 x.

Apply (exandE_i (λx ⇒ x ∈ X) (λx ⇒ z = Inj1 x) H2) to the current goal.

Let x be given.

Assume H2: x ∈ X.

Assume H3: z = Inj1 x.

rewrite the current goal using H3 (from left to right).

We will prove Inj1 x ∈ 1 + X.

Apply Inj1_setsum to the current goal.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (nat_setsum1_ordsucc) The following is provable:

∀n : set, nat_p n → 1 + n = ordsucc n

Proof:

We prove the intermediate claim L: ∀n : set, nat_p n → Inj1 n = ordsucc n.

Apply nat_complete_ind to the current goal.

Let n be given.

Assume Hn: nat_p n.

Assume IHn: ∀m ∈ n, Inj1 m = ordsucc m.

We will prove Inj1 n = ordsucc n.

Apply set_ext to the current goal.

We will prove Inj1 n ⊆ ordsucc n.

Let z be given.

Assume H1: z ∈ Inj1 n.

We will prove z ∈ ordsucc n.

Apply (Inj1E n z H1) to the current goal.

Assume H2: z = 0.

rewrite the current goal using H2 (from left to right).

We will prove 0 ∈ ordsucc n.

An exact proof term for the current goal is (nat_0_in_ordsucc n Hn).

Assume H2: ∃m ∈ n, z = Inj1 m.

Apply (exandE_i (λm ⇒ m ∈ n) (λm ⇒ z = Inj1 m) H2) to the current goal.

Let m be given.

Assume H3: m ∈ n.

Assume H4: z = Inj1 m.

rewrite the current goal using H4 (from left to right).

We will prove Inj1 m ∈ ordsucc n.

rewrite the current goal using (IHn m H3) (from left to right).

We will prove ordsucc m ∈ ordsucc n.

An exact proof term for the current goal is (nat_ordsucc_in_ordsucc n Hn m H3).

We will prove ordsucc n ⊆ Inj1 n.

Let m be given.

Assume H1: m ∈ ordsucc n.

We will prove m ∈ Inj1 n.

Apply (ordsuccE n m H1) to the current goal.

Assume H2: m ∈ n.

Apply (nat_inv m (nat_p_trans n Hn m H2)) to the current goal.

Assume H3: m = 0.

rewrite the current goal using H3 (from left to right).

We will prove 0 ∈ Inj1 n.

An exact proof term for the current goal is (Inj1I1 n).

Assume H3: ∃k, nat_p k ∧ m = ordsucc k.

Apply (exandE_i nat_p (λk ⇒ m = ordsucc k) H3) to the current goal.

Let k be given.

Assume H4: nat_p k.

Assume H5: m = ordsucc k.

rewrite the current goal using H5 (from left to right).

We will prove ordsucc k ∈ Inj1 n.

We prove the intermediate claim L1: k ∈ m.

rewrite the current goal using H5 (from left to right).

An exact proof term for the current goal is (ordsuccI2 k).

We prove the intermediate claim L2: k ∈ n.

An exact proof term for the current goal is (nat_trans n Hn m H2 k L1).

rewrite the current goal using (IHn k L2) (from right to left).

We will prove Inj1 k ∈ Inj1 n.

An exact proof term for the current goal is (Inj1I2 n k L2).

Assume H2: m = n.

rewrite the current goal using H2 (from left to right).

We will prove n ∈ Inj1 n.

Apply (nat_inv n Hn) to the current goal.

Assume H3: n = 0.

rewrite the current goal using H3 (from left to right) at position 1.

We will prove 0 ∈ Inj1 n.

An exact proof term for the current goal is (Inj1I1 n).

Assume H3: ∃k, nat_p k ∧ n = ordsucc k.

Apply (exandE_i nat_p (λk ⇒ n = ordsucc k) H3) to the current goal.

Let k be given.

Assume H4: nat_p k.

Assume H5: n = ordsucc k.

rewrite the current goal using H5 (from left to right) at position 1.

We will prove ordsucc k ∈ Inj1 n.

We prove the intermediate claim L1: k ∈ n.

rewrite the current goal using H5 (from left to right).

An exact proof term for the current goal is (ordsuccI2 k).

rewrite the current goal using (IHn k L1) (from right to left).

We will prove Inj1 k ∈ Inj1 n.

An exact proof term for the current goal is (Inj1I2 n k L1).

Let n be given.

Assume Hn: nat_p n.

We will prove 1 + n = ordsucc n.

rewrite the current goal using Inj1_setsum_1L (from left to right).

We will prove Inj1 n = ordsucc n.

An exact proof term for the current goal is (L n Hn).

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Main Goal

Theorem. (setsum_0_0) The following is provable:

0 + 0 = 0

Proof:

rewrite the current goal using (Inj0_setsum_0L 0) (from left to right).

We will prove Inj0 0 = 0.

An exact proof term for the current goal is Inj0_0.

∎

Try to prove it yourself. Main Goal

Theorem. (setsum_1_0_1) The following is provable:

1 + 0 = 1

Proof:

An exact proof term for the current goal is (nat_setsum1_ordsucc 0 nat_0).

∎

Try to prove it yourself. Main Goal

Theorem. (setsum_1_1_2) The following is provable:

1 + 1 = 2

Proof:

An exact proof term for the current goal is (nat_setsum1_ordsucc 1 nat_1).

∎

Try to prove it yourself. Main Goal

Beginning of Section pair_setsum

Let pair ≝ setsum

Definition. We define proj0 to be λZ ⇒ {Unj z|z ∈ Z, ∃x : set, Inj0 x = z} of type set → set.

Definition. We define proj1 to be λZ ⇒ {Unj z|z ∈ Z, ∃y : set, Inj1 y = z} of type set → set.

Theorem. (Inj0_pair_0_eq) The following is provable:

Inj0 = pair 0

Proof:

Apply (func_ext set set) to the current goal.

Let x be given.

Use symmetry.

We will prove 0 + x = Inj0 x.

An exact proof term for the current goal is (Inj0_setsum_0L x).

∎

Try to prove it yourself. Main Goal

Theorem. (Inj1_pair_1_eq) The following is provable:

Inj1 = pair 1

Proof:

Apply (func_ext set set) to the current goal.

Let x be given.

Use symmetry.

We will prove 1 + x = Inj1 x.

An exact proof term for the current goal is (Inj1_setsum_1L x).

∎

Try to prove it yourself. Main Goal

Theorem. (pairI0) The following is provable:

∀X Y x, x ∈ X → pair 0 x ∈ pair X Y

Proof:

rewrite the current goal using Inj0_pair_0_eq (from right to left).

An exact proof term for the current goal is Inj0_setsum.

∎

Try to prove it yourself. Main Goal

Theorem. (pairI1) The following is provable:

∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y

Proof:

rewrite the current goal using Inj1_pair_1_eq (from right to left).

An exact proof term for the current goal is Inj1_setsum.

∎

Try to prove it yourself. Main Goal

Theorem. (pairE) The following is provable:

∀X Y z, z ∈ pair X Y → (∃x ∈ X, z = pair 0 x) ∨ (∃y ∈ Y, z = pair 1 y)

Proof:

rewrite the current goal using Inj0_pair_0_eq (from right to left).

rewrite the current goal using Inj1_pair_1_eq (from right to left).

An exact proof term for the current goal is setsum_Inj_inv.

∎

Try to prove it yourself. Main Goal

Theorem. (pairE0) The following is provable:

∀X Y x, pair 0 x ∈ pair X Y → x ∈ X

Proof:

Let X, Y and x be given.

Assume H1: pair 0 x ∈ pair X Y.

We will prove x ∈ X.

Apply (pairE X Y (pair 0 x) H1) to the current goal.

rewrite the current goal using Inj0_pair_0_eq (from right to left).

Assume H2: ∃x' ∈ X, Inj0 x = Inj0 x'.

Apply (exandE_i (λx' ⇒ x' ∈ X) (λx' ⇒ Inj0 x = Inj0 x') H2) to the current goal.

Let x' be given.

Assume H3: x' ∈ X.

Assume H4: Inj0 x = Inj0 x'.

We will prove x ∈ X.

rewrite the current goal using (Inj0_inj x x' H4) (from left to right).

We will prove x' ∈ X.

An exact proof term for the current goal is H3.

rewrite the current goal using Inj0_pair_0_eq (from right to left).

rewrite the current goal using Inj1_pair_1_eq (from right to left).

Assume H2: ∃y ∈ Y, Inj0 x = Inj1 y.

We will prove False.

Apply (exandE_i (λy ⇒ y ∈ Y) (λy ⇒ Inj0 x = Inj1 y) H2) to the current goal.

Let y be given.

Assume _.

Assume H3: Inj0 x = Inj1 y.

An exact proof term for the current goal is (Inj0_Inj1_neq x y H3).

∎

Try to prove it yourself. Main Goal

Theorem. (pairE1) The following is provable:

∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y

Proof:

Let X, Y and y be given.

Assume H1: pair 1 y ∈ pair X Y.

We will prove y ∈ Y.

Apply (pairE X Y (pair 1 y) H1) to the current goal.

rewrite the current goal using Inj0_pair_0_eq (from right to left).

rewrite the current goal using Inj1_pair_1_eq (from right to left).

Assume H2: ∃x ∈ X, Inj1 y = Inj0 x.

We will prove False.

Apply (exandE_i (λx ⇒ x ∈ X) (λx ⇒ Inj1 y = Inj0 x) H2) to the current goal.

Let x be given.

Assume _.

Assume H3: Inj1 y = Inj0 x.

Apply (Inj0_Inj1_neq x y) to the current goal.

Use symmetry.

An exact proof term for the current goal is H3.

rewrite the current goal using Inj1_pair_1_eq (from right to left).

Assume H2: ∃y' ∈ Y, Inj1 y = Inj1 y'.

Apply (exandE_i (λy' ⇒ y' ∈ Y) (λy' ⇒ Inj1 y = Inj1 y') H2) to the current goal.

Let y' be given.

Assume H3: y' ∈ Y.

Assume H4: Inj1 y = Inj1 y'.

We will prove y ∈ Y.

rewrite the current goal using (Inj1_inj y y' H4) (from left to right).

We will prove y' ∈ Y.

An exact proof term for the current goal is H3.

∎

Try to prove it yourself. Main Goal

Theorem. (proj0I) The following is provable:

∀w u : set, pair 0 u ∈ w → u ∈ proj0 w

Proof:

rewrite the current goal using Inj0_pair_0_eq (from right to left).

Let w and u be given.

Assume H1: Inj0 u ∈ w.

We will prove u ∈ {Unj z|z ∈ w, ∃x : set, Inj0 x = z}.

rewrite the current goal using (Unj_Inj0_eq u) (from right to left).

We will prove Unj (Inj0 u) ∈ {Unj z|z ∈ w, ∃x : set, Inj0 x = z}.

Apply (ReplSepI w (λz ⇒ ∃x : set, Inj0 x = z) Unj (Inj0 u)) to the current goal.

We will prove Inj0 u ∈ w.

An exact proof term for the current goal is H1.

We will prove ∃x, Inj0 x = Inj0 u.

We use u to witness the existential quantifier.

Use reflexivity.

∎

Try to prove it yourself. Main Goal

Theorem. (proj0E) The following is provable:

∀w u : set, u ∈ proj0 w → pair 0 u ∈ w

Proof:

Let w and u be given.

Assume H1: u ∈ {Unj z|z ∈ w, ∃x : set, Inj0 x = z}.

rewrite the current goal using Inj0_pair_0_eq (from right to left).

We will prove Inj0 u ∈ w.

Apply (ReplSepE_impred w (λz ⇒ ∃x : set, Inj0 x = z) Unj u H1) to the current goal.

Let z be given.

Assume H2: z ∈ w.

Assume H3: ∃x, Inj0 x = z.

Assume H4: u = Unj z.

Apply H3 to the current goal.

Let x be given.

Assume H5: Inj0 x = z.

We will prove Inj0 u ∈ w.

rewrite the current goal using H4 (from left to right).

We will prove Inj0 (Unj z) ∈ w.

rewrite the current goal using H5 (from right to left).

We will prove Inj0 (Unj (Inj0 x)) ∈ w.

rewrite the current goal using Unj_Inj0_eq (from left to right).

We will prove Inj0 x ∈ w.

rewrite the current goal using H5 (from left to right).

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (proj1I) The following is provable:

∀w u : set, pair 1 u ∈ w → u ∈ proj1 w

Proof:

rewrite the current goal using Inj1_pair_1_eq (from right to left).

Let w and u be given.

Assume H1: Inj1 u ∈ w.

We will prove u ∈ {Unj z|z ∈ w, ∃y : set, Inj1 y = z}.

rewrite the current goal using (Unj_Inj1_eq u) (from right to left).

We will prove Unj (Inj1 u) ∈ {Unj z|z ∈ w, ∃y : set, Inj1 y = z}.

Apply (ReplSepI w (λz ⇒ ∃y : set, Inj1 y = z) Unj (Inj1 u)) to the current goal.

We will prove Inj1 u ∈ w.

An exact proof term for the current goal is H1.

We will prove ∃y, Inj1 y = Inj1 u.

We use u to witness the existential quantifier.

Use reflexivity.

∎

Try to prove it yourself. Main Goal

Theorem. (proj1E) The following is provable:

∀w u : set, u ∈ proj1 w → pair 1 u ∈ w

Proof:

Let w and u be given.

Assume H1: u ∈ {Unj z|z ∈ w, ∃y : set, Inj1 y = z}.

rewrite the current goal using Inj1_pair_1_eq (from right to left).

We will prove Inj1 u ∈ w.

Apply (ReplSepE_impred w (λz ⇒ ∃y : set, Inj1 y = z) Unj u H1) to the current goal.

Let z be given.

Assume H2: z ∈ w.

Assume H3: ∃y, Inj1 y = z.

Assume H4: u = Unj z.

Apply H3 to the current goal.

Let y be given.

Assume H5: Inj1 y = z.

We will prove Inj1 u ∈ w.

rewrite the current goal using H4 (from left to right).

We will prove Inj1 (Unj z) ∈ w.

rewrite the current goal using H5 (from right to left).

We will prove Inj1 (Unj (Inj1 y)) ∈ w.

rewrite the current goal using Unj_Inj1_eq (from left to right).

We will prove Inj1 y ∈ w.

rewrite the current goal using H5 (from left to right).

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (proj0_pair_eq) The following is provable:

∀X Y : set, proj0 (pair X Y) = X

Proof:

Let X and Y be given.

Apply set_ext to the current goal.

We will prove proj0 (pair X Y) ⊆ X.

Let u be given.

Assume H1: u ∈ proj0 (pair X Y).

We will prove u ∈ X.

Apply (pairE0 X Y u) to the current goal.

We will prove pair 0 u ∈ pair X Y.

An exact proof term for the current goal is (proj0E (pair X Y) u H1).

We will prove X ⊆ proj0 (pair X Y).

Let u be given.

Assume H1: u ∈ X.

We will prove u ∈ proj0 (pair X Y).

Apply proj0I to the current goal.

We will prove pair 0 u ∈ pair X Y.

Apply pairI0 to the current goal.

We will prove u ∈ X.

An exact proof term for the current goal is H1.

∎

Try to prove it yourself. Main Goal

Theorem. (proj1_pair_eq) The following is provable:

∀X Y : set, proj1 (pair X Y) = Y

Proof:

Let X and Y be given.

Apply set_ext to the current goal.

We will prove proj1 (pair X Y) ⊆ Y.

Let u be given.

Assume H1: u ∈ proj1 (pair X Y).

We will prove u ∈ Y.

Apply (pairE1 X Y u) to the current goal.

We will prove pair 1 u ∈ pair X Y.

An exact proof term for the current goal is (proj1E (pair X Y) u H1).

We will prove Y ⊆ proj1 (pair X Y).

Let u be given.

Assume H1: u ∈ Y.

We will prove u ∈ proj1 (pair X Y).

Apply proj1I to the current goal.

We will prove pair 1 u ∈ pair X Y.

Apply pairI1 to the current goal.

We will prove u ∈ Y.

An exact proof term for the current goal is H1.

∎

Try to prove it yourself. Main Goal

Σ Sets, a.k.a λs

Definition. We define Sigma to be λX Y ⇒ ⋃_{x ∈ X}{pair x y|y ∈ Y x} of type set → (set → set) → set.

Notation. We use ∑ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Sigma.

Theorem. (pair_Sigma) The following is provable:

∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, pair x y ∈ ∑x ∈ X, Y x

Proof:

Let X, Y and x be given.

Assume Hx: x ∈ X.

Let y be given.

Assume Hy: y ∈ Y x.

We will prove pair x y ∈ ⋃_{x ∈ X}{pair x y|y ∈ Y x}.

Apply (famunionI X (λx ⇒ {pair x y|y ∈ Y x}) x (pair x y)) to the current goal.

We will prove x ∈ X.

An exact proof term for the current goal is Hx.

We will prove pair x y ∈ {pair x y|y ∈ Y x}.

Apply ReplI to the current goal.

We will prove y ∈ Y x.

An exact proof term for the current goal is Hy.

∎

Try to prove it yourself. Main Goal

Theorem. (Sigma_eta_proj0_proj1) The following is provable:

∀X : set, ∀Y : set → set, ∀z ∈ (∑x ∈ X, Y x), pair (proj0 z) (proj1 z) = z ∧ proj0 z ∈ X ∧ proj1 z ∈ Y (proj0 z)

Proof:

Let X, Y and z be given.

Assume H1: z ∈ ∑x ∈ X, Y x.

We prove the intermediate claim L1: ∃x ∈ X, z ∈ {pair x y|y ∈ Y x}.

An exact proof term for the current goal is (famunionE X (λx ⇒ {pair x y|y ∈ Y x}) z H1).

Apply (exandE_i (λx ⇒ x ∈ X) (λx ⇒ z ∈ {pair x y|y ∈ Y x}) L1) to the current goal.

Let x be given.

Assume H2: x ∈ X.

Assume H3: z ∈ {pair x y|y ∈ Y x}.

Apply (ReplE_impred (Y x) (pair x) z H3) to the current goal.

Let y be given.

Assume H4: y ∈ Y x.

Assume H5: z = pair x y.

rewrite the current goal using H5 (from left to right).

We will prove pair (proj0 (pair x y)) (proj1 (pair x y)) = pair x y ∧ proj0 (pair x y) ∈ X ∧ proj1 (pair x y) ∈ Y (proj0 (pair x y)).

rewrite the current goal using proj0_pair_eq (from left to right).

We will prove pair x (proj1 (pair x y)) = pair x y ∧ x ∈ X ∧ proj1 (pair x y) ∈ Y x.

rewrite the current goal using proj1_pair_eq (from left to right).

We will prove pair x y = pair x y ∧ x ∈ X ∧ y ∈ Y x.

Apply and3I to the current goal.

We will prove pair x y = pair x y.

Use reflexivity.

We will prove x ∈ X.

An exact proof term for the current goal is H2.

We will prove y ∈ Y x.

An exact proof term for the current goal is H4.

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (proj_Sigma_eta) The following is provable:

∀X : set, ∀Y : set → set, ∀z ∈ (∑x ∈ X, Y x), pair (proj0 z) (proj1 z) = z

Proof:

Let X, Y and z be given.

Assume H1: z ∈ ∑x ∈ X, Y x.

Apply (and3E (pair (proj0 z) (proj1 z) = z) (proj0 z ∈ X) (proj1 z ∈ Y (proj0 z)) (Sigma_eta_proj0_proj1 X Y z H1)) to the current goal.

Assume H2 _ _.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (proj0_Sigma) The following is provable:

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → proj0 z ∈ X

Proof:

Let X, Y and z be given.

Assume H1: z ∈ ∑x ∈ X, Y x.

Apply (and3E (pair (proj0 z) (proj1 z) = z) (proj0 z ∈ X) (proj1 z ∈ Y (proj0 z)) (Sigma_eta_proj0_proj1 X Y z H1)) to the current goal.

Assume _ H2 _.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (proj1_Sigma) The following is provable:

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → proj1 z ∈ Y (proj0 z)

Proof:

Let X, Y and z be given.

Assume H1: z ∈ ∑x ∈ X, Y x.

Apply (and3E (pair (proj0 z) (proj1 z) = z) (proj0 z ∈ X) (proj1 z ∈ Y (proj0 z)) (Sigma_eta_proj0_proj1 X Y z H1)) to the current goal.

Assume _ _ H2.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (pair_Sigma_E1) The following is provable:

∀X : set, ∀Y : set → set, ∀x y : set, pair x y ∈ (∑x ∈ X, Y x) → y ∈ Y x

Proof:

Let X, Y, x and y be given.

Assume H1: pair x y ∈ ∑x ∈ X, Y x.

We will prove y ∈ Y x.

rewrite the current goal using (proj0_pair_eq x y) (from right to left).

We will prove y ∈ Y (proj0 (pair x y)).

rewrite the current goal using (proj1_pair_eq x y) (from right to left) at position 1.

We will prove proj1 (pair x y) ∈ Y (proj0 (pair x y)).

An exact proof term for the current goal is (proj1_Sigma X Y (pair x y) H1).

∎

Try to prove it yourself. Main Goal

Theorem. (Sigma_E) The following is provable:

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → ∃x ∈ X, ∃y ∈ Y x, z = pair x y

Proof:

Let X, Y and z be given.

Assume Hz: z ∈ ∑x ∈ X, Y x.

Apply (and3E (pair (proj0 z) (proj1 z) = z) (proj0 z ∈ X) (proj1 z ∈ Y (proj0 z)) (Sigma_eta_proj0_proj1 X Y z Hz)) to the current goal.

Assume H1: pair (proj0 z) (proj1 z) = z.

Assume H2: proj0 z ∈ X.

Assume H3: proj1 z ∈ Y (proj0 z).

We use (proj0 z) to witness the existential quantifier.

Apply andI to the current goal.

We will prove proj0 z ∈ X.

An exact proof term for the current goal is H2.

We use (proj1 z) to witness the existential quantifier.

Apply andI to the current goal.

We will prove proj1 z ∈ Y (proj0 z).

An exact proof term for the current goal is H3.

We will prove z = pair (proj0 z) (proj1 z).

Use symmetry.

An exact proof term for the current goal is H1.

∎

Try to prove it yourself. Main Goal

Definition. We define setprod to be λX Y : set ⇒ ∑x ∈ X, Y of type set → set → set.

Notation. We use ⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.

Let lam : set → (set → set) → set ≝ Sigma

Definition. We define ap to be λf x ⇒ {proj1 z|z ∈ f, ∃y : set, z = pair x y} of type set → set → set.

Notation. When x is a set, a term x y is notation for ap x y.

Notation. λ x ∈ A ⇒ B is notation for the set Sigma A (λ x : set ⇒ B).

Theorem. (lamI) The following is provable:

∀X : set, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, pair x y ∈ λx ∈ X ⇒ F x

Proof:

An exact proof term for the current goal is pair_Sigma.

∎

Try to prove it yourself. Main Goal

Theorem. (lamE) The following is provable:

∀X : set, ∀F : set → set, ∀z : set, z ∈ (λx ∈ X ⇒ F x) → ∃x ∈ X, ∃y ∈ F x, z = pair x y

Proof:

An exact proof term for the current goal is Sigma_E.

∎

Try to prove it yourself. Main Goal

Theorem. (apI) The following is provable:

∀f x y, pair x y ∈ f → y ∈ f x

Proof:

Let f, x and y be given.

Assume H1: pair x y ∈ f.

We will prove y ∈ {proj1 z|z ∈ f, ∃y : set, z = pair x y}.

rewrite the current goal using (proj1_pair_eq x y) (from right to left).

We will prove proj1 (pair x y) ∈ {proj1 z|z ∈ f, ∃y : set, z = pair x y}.

Apply (ReplSepI f (λz ⇒ ∃y : set, z = pair x y) proj1 (pair x y) H1) to the current goal.

We will prove ∃y' : set, pair x y = pair x y'.

We use y to witness the existential quantifier.

Use reflexivity.

∎

Try to prove it yourself. Main Goal

Theorem. (apE) The following is provable:

∀f x y, y ∈ f x → pair x y ∈ f

Proof:

Let f, x and y be given.

Assume H1: y ∈ {proj1 z|z ∈ f, ∃y : set, z = pair x y}.

We will prove pair x y ∈ f.

Apply (ReplSepE_impred f (λz ⇒ ∃y : set, z = pair x y) proj1 y H1) to the current goal.

Let z be given.

Assume Hz: z ∈ f.

Assume H1: ∃y : set, z = pair x y.

Assume H2: y = proj1 z.

Apply H1 to the current goal.

Let v be given.

Assume H3: z = pair x v.

We prove the intermediate claim L1: y = v.

rewrite the current goal using H2 (from left to right).

rewrite the current goal using H3 (from left to right).

We will prove proj1 (pair x v) = v.

Apply proj1_pair_eq to the current goal.

We prove the intermediate claim L2: z = pair x y.

rewrite the current goal using L1 (from left to right).

An exact proof term for the current goal is H3.

rewrite the current goal using L2 (from right to left).

An exact proof term for the current goal is Hz.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Theorem. (beta) The following is provable:

∀X : set, ∀F : set → set, ∀x : set, x ∈ X → (λx ∈ X ⇒ F x) x = F x

Proof:

Let X, F and x be given.

Assume Hx: x ∈ X.

Apply set_ext to the current goal.

Let w be given.

Assume Hw: w ∈ (λx ∈ X ⇒ F x) x.

We prove the intermediate claim L1: pair x w ∈ (λx ∈ X ⇒ F x).

An exact proof term for the current goal is (apE (λx ∈ X ⇒ F x) x w Hw).

An exact proof term for the current goal is (pair_Sigma_E1 X F x w L1).

Let w be given.

Assume Hw: w ∈ F x.

We will prove w ∈ (λx ∈ X ⇒ F x) x.

Apply apI to the current goal.

We will prove pair x w ∈ λx ∈ X ⇒ F x.

We will prove pair x w ∈ ∑x ∈ X, F x.

Apply pair_Sigma to the current goal.

An exact proof term for the current goal is Hx.

An exact proof term for the current goal is Hw.

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (proj0_ap_0) The following is provable:

∀u, proj0 u = u 0

Proof:

Let u be given.

Apply set_ext to the current goal.

Let w be given.

Assume H1: w ∈ proj0 u.

We will prove w ∈ u 0.

Apply apI to the current goal.

We will prove pair 0 w ∈ u.

Apply proj0E to the current goal.

We will prove w ∈ proj0 u.

An exact proof term for the current goal is H1.

Let w be given.

Assume H1: w ∈ u 0.

We will prove w ∈ proj0 u.

Apply proj0I to the current goal.

We will prove pair 0 w ∈ u.

Apply apE to the current goal.

We will prove w ∈ u 0.

An exact proof term for the current goal is H1.

∎

Try to prove it yourself. Main Goal

Theorem. (proj1_ap_1) The following is provable:

∀u, proj1 u = u 1

Proof:

Let u be given.

Apply set_ext to the current goal.

Let w be given.

Assume H1: w ∈ proj1 u.

We will prove w ∈ u 1.

Apply apI to the current goal.

We will prove pair 1 w ∈ u.

Apply proj1E to the current goal.

We will prove w ∈ proj1 u.

An exact proof term for the current goal is H1.

Let w be given.

Assume H1: w ∈ u 1.

We will prove w ∈ proj1 u.

Apply proj1I to the current goal.

We will prove pair 1 w ∈ u.

Apply apE to the current goal.

We will prove w ∈ u 1.

An exact proof term for the current goal is H1.

∎

Try to prove it yourself. Main Goal

Theorem. (pair_ap_0) The following is provable:

∀x y : set, (pair x y) 0 = x

Proof:

Let x and y be given.

rewrite the current goal using (proj0_ap_0 (pair x y)) (from right to left).

We will prove proj0 (pair x y) = x.

Apply proj0_pair_eq to the current goal.

∎

Try to prove it yourself. Main Goal

Theorem. (pair_ap_1) The following is provable:

∀x y : set, (pair x y) 1 = y

Proof:

Let x and y be given.

rewrite the current goal using (proj1_ap_1 (pair x y)) (from right to left).

We will prove proj1 (pair x y) = y.

Apply proj1_pair_eq to the current goal.

∎

Try to prove it yourself. Main Goal

Theorem. (ap0_Sigma) The following is provable:

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 0) ∈ X

Proof:

Let X, Y and z be given.

rewrite the current goal using proj0_ap_0 (from right to left).

Apply proj0_Sigma to the current goal.

∎

Try to prove it yourself. Main Goal

Theorem. (ap1_Sigma) The following is provable:

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 1) ∈ (Y (z 0))

Proof:

Let X, Y and z be given.

rewrite the current goal using proj0_ap_0 (from right to left).

rewrite the current goal using proj1_ap_1 (from right to left).

Apply proj1_Sigma to the current goal.

∎

Try to prove it yourself. Main Goal

Definition. We define pair_p to be λu : set ⇒ pair (u 0) (u 1) = u of type set → prop.

Theorem. (pair_p_I) The following is provable:

∀x y, pair_p (pair x y)

Proof:

Let x and y be given.

We will prove pair (pair x y 0) (pair x y 1) = pair x y.

rewrite the current goal using pair_ap_0 (from left to right).

rewrite the current goal using pair_ap_1 (from left to right).

Use reflexivity.

∎

Try to prove it yourself. Main Goal

Theorem. (Subq_2_UPair01) The following is provable:

2 ⊆ {0,1}

Proof:

Let x be given.

Assume H1: x ∈ 2.

Apply ordsuccE 1 x H1 to the current goal.

Assume H2: x ∈ 1.

We prove the intermediate claim L1: x = 0.

An exact proof term for the current goal is (SingE 0 x (Subq_1_Sing0 x H2)).

We will prove x ∈ {0,1}.

rewrite the current goal using L1 (from left to right).

We will prove 0 ∈ {0,1}.

An exact proof term for the current goal is (UPairI1 0 1).

Assume H2: x = 1.

We will prove x ∈ {0,1}.

rewrite the current goal using H2 (from left to right).

We will prove 1 ∈ {0,1}.

An exact proof term for the current goal is (UPairI2 0 1).

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (tuple_pair) The following is provable:

∀x y : set, pair x y = (x,y)

Proof:

Let x and y be given.

Apply set_ext to the current goal.

Let z be given.

Assume Hz: z ∈ pair x y.

Apply (pairE x y z Hz) to the current goal.

Assume H1: ∃u ∈ x, z = pair 0 u.

Apply (exandE_i (λu ⇒ u ∈ x) (λu ⇒ z = pair 0 u) H1) to the current goal.

Let u be given.

Assume Hu: u ∈ x.

Assume H2: z = pair 0 u.

We will prove z ∈ (x,y).

We will prove z ∈ λi ∈ 2 ⇒ if i = 0 then x else y.

rewrite the current goal using H2 (from left to right).

We will prove pair 0 u ∈ λi ∈ 2 ⇒ if i = 0 then x else y.

Apply (lamI 2 (λi ⇒ if i = 0 then x else y) 0 In_0_2 u) to the current goal.

We will prove u ∈ if 0 = 0 then x else y.

rewrite the current goal using (If_i_1 (0 = 0) x y (λq H ⇒ H)) (from left to right).

We will prove u ∈ x.

An exact proof term for the current goal is Hu.

Assume H1: ∃u ∈ y, z = pair 1 u.

Apply (exandE_i (λu ⇒ u ∈ y) (λu ⇒ z = pair 1 u) H1) to the current goal.

Let u be given.

Assume Hu: u ∈ y.

Assume H2: z = pair 1 u.

We will prove z ∈ (x,y).

We will prove z ∈ λi ∈ 2 ⇒ if i = 0 then x else y.

rewrite the current goal using H2 (from left to right).

We will prove pair 1 u ∈ λi ∈ 2 ⇒ if i = 0 then x else y.

Apply (lamI 2 (λi ⇒ if i = 0 then x else y) 1 In_1_2 u) to the current goal.

We will prove u ∈ if 1 = 0 then x else y.

rewrite the current goal using (If_i_0 (1 = 0) x y neq_1_0) (from left to right).

We will prove u ∈ y.

An exact proof term for the current goal is Hu.

Let z be given.

Assume Hz: z ∈ (x,y).

We will prove z ∈ pair x y.

We prove the intermediate claim L1: ∃i ∈ 2, ∃w ∈ (if i = 0 then x else y), z = pair i w.

An exact proof term for the current goal is (lamE 2 (λi ⇒ if i = 0 then x else y) z Hz).

Apply (exandE_i (λi ⇒ i ∈ 2) (λi ⇒ ∃w ∈ (if i = 0 then x else y), z = pair i w) L1) to the current goal.

Let i be given.

Assume Hi: i ∈ 2.

Assume H1: ∃w ∈ (if i = 0 then x else y), z = pair i w.

Apply (exandE_i (λw ⇒ w ∈ if i = 0 then x else y) (λw ⇒ z = pair i w) H1) to the current goal.

Let w be given.

Assume Hw: w ∈ if i = 0 then x else y.

Assume H2: z = pair i w.

We will prove z ∈ pair x y.

rewrite the current goal using H2 (from left to right).

We will prove pair i w ∈ pair x y.

We prove the intermediate claim L2: i ∈ {0,1}.

An exact proof term for the current goal is (Subq_2_UPair01 i Hi).

Apply (UPairE i 0 1 L2) to the current goal.

Assume Hi0: i = 0.

rewrite the current goal using Hi0 (from left to right).

We will prove pair 0 w ∈ pair x y.

Apply pairI0 to the current goal.

We will prove w ∈ x.

We prove the intermediate claim L3: (if i = 0 then x else y) = x.

An exact proof term for the current goal is (If_i_1 (i = 0) x y Hi0).

rewrite the current goal using L3 (from right to left).

An exact proof term for the current goal is Hw.

Assume Hi1: i = 1.

rewrite the current goal using Hi1 (from left to right).

We will prove pair 1 w ∈ pair x y.

Apply pairI1 to the current goal.

We will prove w ∈ y.

We prove the intermediate claim L3: (if i = 0 then x else y) = y.

rewrite the current goal using Hi1 (from left to right).

An exact proof term for the current goal is (If_i_0 (1 = 0) x y neq_1_0).

rewrite the current goal using L3 (from right to left).

An exact proof term for the current goal is Hw.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Main Goal

Π Sets

Definition. We define Pi to be λX Y ⇒ {f ∈ 𝒫 (∑x ∈ X, ⋃ (Y x))|∀x ∈ X, f x ∈ Y x} of type set → (set → set) → set.

Notation. We use ∏ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Pi.

Theorem. (PiI) The following is provable:

∀X : set, ∀Y : set → set, ∀f : set, (∀u ∈ f, pair_p u ∧ u 0 ∈ X) → (∀x ∈ X, f x ∈ Y x) → f ∈ ∏x ∈ X, Y x

Proof:

Let X, Y and f be given.

Assume H1: ∀u ∈ f, pair_p u ∧ u 0 ∈ X.

Assume H2: ∀x ∈ X, f x ∈ Y x.

We will prove f ∈ {f ∈ 𝒫 (∑x ∈ X, ⋃ (Y x))|∀x ∈ X, f x ∈ Y x}.

Apply SepI to the current goal.

We will prove f ∈ 𝒫 (∑x ∈ X, ⋃ (Y x)).

Apply PowerI to the current goal.

We will prove f ⊆ ∑x ∈ X, ⋃ (Y x).

Let z be given.

Assume Hz: z ∈ f.

We will prove z ∈ ∑x ∈ X, ⋃ (Y x).

Apply (H1 z Hz) to the current goal.

Assume H3: pair (z 0) (z 1) = z.

Assume H4: z 0 ∈ X.

rewrite the current goal using H3 (from right to left).

We will prove pair (z 0) (z 1) ∈ ∑x ∈ X, ⋃ (Y x).

Apply pair_Sigma to the current goal.

We will prove z 0 ∈ X.

An exact proof term for the current goal is H4.

We will prove z 1 ∈ ⋃ (Y (z 0)).

Apply (UnionI (Y (z 0)) (z 1) (f (z 0))) to the current goal.

We will prove z 1 ∈ f (z 0).

Apply apI to the current goal.

We will prove pair (z 0) (z 1) ∈ f.

rewrite the current goal using H3 (from left to right).

An exact proof term for the current goal is Hz.

We will prove f (z 0) ∈ Y (z 0).

An exact proof term for the current goal is (H2 (z 0) H4).

We will prove ∀x ∈ X, f x ∈ Y x.

An exact proof term for the current goal is H2.

∎

Try to prove it yourself. Main Goal

Theorem. (lam_Pi) The following is provable:

∀X : set, ∀Y : set → set, ∀F : set → set, (∀x ∈ X, F x ∈ Y x) → (λx ∈ X ⇒ F x) ∈ (∏x ∈ X, Y x)

Proof:

Let X, Y and F be given.

Assume H1: ∀x ∈ X, F x ∈ Y x.

We will prove (λx ∈ X ⇒ F x) ∈ (∏x ∈ X, Y x).

Apply PiI to the current goal.

We will prove ∀u ∈ (λx ∈ X ⇒ F x), pair_p u ∧ u 0 ∈ X.

Let u be given.

Assume Hu: u ∈ λx ∈ X ⇒ F x.

We prove the intermediate claim L1: ∃x ∈ X, ∃y ∈ F x, u = pair x y.

An exact proof term for the current goal is (lamE X F u Hu).

Apply (exandE_i (λx ⇒ x ∈ X) (λx ⇒ ∃y ∈ F x, u = pair x y) L1) to the current goal.

Let x be given.

Assume Hx: x ∈ X.

Assume H2: ∃y ∈ F x, u = pair x y.

Apply (exandE_i (λy ⇒ y ∈ F x) (λy ⇒ u = pair x y) H2) to the current goal.

Let y be given.

Assume Hy: y ∈ F x.

Assume H3: u = pair x y.

Apply andI to the current goal.

We will prove pair_p u.

rewrite the current goal using H3 (from left to right).

Apply pair_p_I to the current goal.

We will prove u 0 ∈ X.

rewrite the current goal using H3 (from left to right).

We will prove pair x y 0 ∈ X.

rewrite the current goal using pair_ap_0 (from left to right).

We will prove x ∈ X.

An exact proof term for the current goal is Hx.

We will prove ∀x ∈ X, (λx ∈ X ⇒ F x) x ∈ Y x.

Let x be given.

Assume Hx: x ∈ X.

rewrite the current goal using (beta X F x Hx) (from left to right).

We will prove F x ∈ Y x.

An exact proof term for the current goal is (H1 x Hx).

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (ap_Pi) The following is provable:

∀X : set, ∀Y : set → set, ∀f : set, ∀x : set, f ∈ (∏x ∈ X, Y x) → x ∈ X → f x ∈ Y x

Proof:

Let X, Y, f and x be given.

Assume Hf: f ∈ ∏x ∈ X, Y x.

An exact proof term for the current goal is (SepE2 (𝒫 (∑x ∈ X, ⋃ (Y x))) (λf ⇒ ∀x ∈ X, f x ∈ Y x) f Hf x).

∎

Try to prove it yourself. Main Goal

Definition. We define setexp to be λX Y : set ⇒ ∏y ∈ Y, X of type set → set → set.

Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.

Theorem. (pair_tuple_fun) The following is provable:

pair = (λx y ⇒ (x,y))

Proof:

Apply func_ext set (set → set) to the current goal.

Let x be given.

Apply func_ext set set to the current goal.

Let y be given.

We will prove pair x y = (x,y).

Apply tuple_pair to the current goal.

∎

Try to prove it yourself. Main Goal

Theorem. (lamI2) The following is provable:

∀X, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, (x,y) ∈ λx ∈ X ⇒ F x

Proof:

We will prove (∀X, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, ((λx y : set ⇒ (x,y)) x y) ∈ λx ∈ X ⇒ F x).

rewrite the current goal using pair_tuple_fun (from right to left).

An exact proof term for the current goal is lamI.

∎

Try to prove it yourself. Main Goal

Beginning of Section Tuples

Variable x0 x1 : set

Theorem. (tuple_2_0_eq) The following is provable:

(x0,x1) 0 = x0

Proof:

rewrite the current goal using beta 2 (λi ⇒ if i = 0 then x0 else x1) 0 In_0_2 (from left to right).

Apply If_i_1 to the current goal.

Use reflexivity.

∎

Try to prove it yourself. Main Goal

Theorem. (tuple_2_1_eq) The following is provable:

(x0,x1) 1 = x1

Proof:

rewrite the current goal using beta 2 (λi ⇒ if i = 0 then x0 else x1) 1 In_1_2 (from left to right).

Apply If_i_0 to the current goal.

Apply neq_1_0 to the current goal.

∎

Try to prove it yourself. Main Goal

End of Section Tuples

Theorem. (ReplEq_setprod_ext) The following is provable:

∀X Y, ∀F G : set → set → set, (∀x ∈ X, ∀y ∈ Y, F x y = G x y) → {F (w 0) (w 1)|w ∈ X ⨯ Y} = {G (w 0) (w 1)|w ∈ X ⨯ Y}

Proof:

Let X, Y, F and G be given.

Assume H1: ∀x ∈ X, ∀y ∈ Y, F x y = G x y.

Apply ReplEq_ext (X ⨯ Y) (λw ⇒ F (w 0) (w 1)) (λw ⇒ G (w 0) (w 1)) to the current goal.

We will prove ∀w ∈ X ⨯ Y, F (w 0) (w 1) = G (w 0) (w 1).

Let w be given.

Assume Hw: w ∈ X ⨯ Y.

Apply H1 to the current goal.

We will prove w 0 ∈ X.

An exact proof term for the current goal is ap0_Sigma X (λ_ ⇒ Y) w Hw.

We will prove w 1 ∈ Y.

An exact proof term for the current goal is ap1_Sigma X (λ_ ⇒ Y) w Hw.

∎

Try to prove it yourself. Main Goal

Theorem. (tuple_2_Sigma) The following is provable:

∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, (x,y) ∈ ∑x ∈ X, Y x

Proof:

An exact proof term for the current goal is lamI2.

∎

Try to prove it yourself. Main Goal

Theorem. (tuple_2_setprod) The following is provable:

∀X : set, ∀Y : set, ∀x ∈ X, ∀y ∈ Y, (x,y) ∈ X ⨯ Y

Proof:

An exact proof term for the current goal is λX Y x Hx y Hy ⇒ tuple_2_Sigma X (λ_ ⇒ Y) x Hx y Hy.

∎

Try to prove it yourself. Main Goal

End of Section pair_setsum