Primitive. 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)

In Proofgold the corresponding term root is c3f0de... and proposition id is 756d6e...

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

In Proofgold the corresponding term root is f81b39... and object id is 94e6a7...

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

In Proofgold the corresponding term root is 1db705... and object id is 266ad5...

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

In Proofgold the corresponding term root is f30435... and object id is 0dc3c7...

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

L12

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

In Proofgold the corresponding term root is 2ba7d0... and object id is 37da83...

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

L17

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

In Proofgold the corresponding term root is 957746... and object id is 86ae64...

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

L22

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

In Proofgold the corresponding term root is 98aaaf... and object id is 6588e5...

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

Beginning of Section Eq

L29

Variable A : SType

L30

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

L31

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

L39

Variable A B : SType

L40

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

L44

Variable A : SType

L45

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.

L50

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

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

In Proofgold the corresponding term root is 00ac81... and proposition id is 1d1e56...

Primitive. 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.

L54

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

In Proofgold the corresponding term root is 81c0ef... and object id is 317007...

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.

L56

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

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

In Proofgold the corresponding term root is b3b698... and proposition id is 21238a...

L58

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

In Proofgold the corresponding term root is 045211... and proposition id is 20faa5...

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.

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

L64

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

¬ ∃x : set, x ∈ Empty

In Proofgold the corresponding term root is 4da931... and proposition id is c7b0d7...

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

L68

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

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

In Proofgold the corresponding term root is bf4c26... and proposition id is 40660f...

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

L73

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

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

In Proofgold the corresponding term root is 746e5a... and proposition id is d67d71...

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

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

L78

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

In Proofgold the corresponding term root is 4f2357... and proposition id is 471122...

L80

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

In Proofgold the corresponding term root is 538bb7... and object id is e69f92...

L82

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

In Proofgold the corresponding term root is 57561d... and object id is e45ed9...

L84

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

In Proofgold the corresponding term root is 8b9cc0... and object id is d2954e...

L85

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.

In Proofgold the corresponding term root is 5574bb... and object id is 513534...

L87

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

In Proofgold the corresponding term root is 1bd4aa... and object id is e1eccf...

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

L93

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

∀N : set, N ∈ UnivOf N

In Proofgold the corresponding term root is efcc16... and proposition id is e805d4...

L95

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

∀N : set, TransSet (UnivOf N)

In Proofgold the corresponding term root is 053575... and proposition id is cf4f5c...

L97

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

∀N : set, ZF_closed (UnivOf N)

In Proofgold the corresponding term root is 770e35... and proposition id is 0e7363...

L99

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

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

In Proofgold the corresponding term root is 042dda... and proposition id is 1f7933...

L104

Theorem. (FalseE)

False → ∀p : prop, p

In Proofgold the corresponding term root is 0dcfe3... and proposition id is f9a230...

Proof:
Proof not loaded.

L108

Theorem. (TrueI)

True

In Proofgold the corresponding term root is f81b39... and proposition id is eb5cbf...

Proof:
Proof not loaded.

L112

Theorem. (andI)

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

In Proofgold the corresponding term root is 3c4f59... and proposition id is 3bf198...

Proof:
Proof not loaded.

L116

Theorem. (andEL)

∀A B : prop, A ∧ B → A

In Proofgold the corresponding term root is c2f006... and proposition id is 718be4...

Proof:
Proof not loaded.

L120

Theorem. (andER)

∀A B : prop, A ∧ B → B

In Proofgold the corresponding term root is f66b82... and proposition id is 5caea9...

Proof:
Proof not loaded.

L124

Theorem. (orIL)

∀A B : prop, A → A ∨ B

In Proofgold the corresponding term root is 55be8c... and proposition id is 382673...

Proof:
Proof not loaded.

L128

Theorem. (orIR)

∀A B : prop, B → A ∨ B

In Proofgold the corresponding term root is 3c63fc... and proposition id is 8d8e40...

Proof:
Proof not loaded.

Beginning of Section PropN

L134

Variable P1 P2 P3 : prop

L136

Theorem. (and3I)

P1 → P2 → P3 → P1 ∧ P2 ∧ P3

In Proofgold the corresponding term root is 23ac9c... and proposition id is cb999b...

Proof:
Proof not loaded.

L140

Theorem. (and3E)

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

In Proofgold the corresponding term root is 445f76... and proposition id is 50fabe...

Proof:
Proof not loaded.

L144

Theorem. (or3I1)

P1 → P1 ∨ P2 ∨ P3

In Proofgold the corresponding term root is e44f34... and proposition id is ef9071...

Proof:
Proof not loaded.

L148

Theorem. (or3I2)

P2 → P1 ∨ P2 ∨ P3

In Proofgold the corresponding term root is 8df6e1... and proposition id is 827a91...

Proof:
Proof not loaded.

L152

Theorem. (or3I3)

P3 → P1 ∨ P2 ∨ P3

In Proofgold the corresponding term root is 017a00... and proposition id is 3b7f5a...

Proof:
Proof not loaded.

L156

Theorem. (or3E)

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

In Proofgold the corresponding term root is 5d069d... and proposition id is 2120c9...

Proof:
Proof not loaded.

L160

Variable P4 : prop

L162

Theorem. (and4I)

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

In Proofgold the corresponding term root is ed32cb... and proposition id is 906aaf...

Proof:
Proof not loaded.

L166

Variable P5 : prop

L168

Theorem. (and5I)

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

In Proofgold the corresponding term root is 041ced... and proposition id is 11fc47...

Proof:
Proof not loaded.

End of Section PropN

L174

Theorem. (not_or_and_demorgan)

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

In Proofgold the corresponding term root is 8733b0... and proposition id is 27db91...

Proof:
Proof not loaded.

L182

Theorem. (not_ex_all_demorgan_i)

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

In Proofgold the corresponding term root is 73523e... and proposition id is 075ddf...

Proof:
Proof not loaded.

L188

Theorem. (iffI)

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

In Proofgold the corresponding term root is 7516b9... and proposition id is 4d966a...

Proof:
Proof not loaded.

L192

Theorem. (iffEL)

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

In Proofgold the corresponding term root is 0e94c6... and proposition id is 9a07f6...

Proof:
Proof not loaded.

L196

Theorem. (iffER)

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

In Proofgold the corresponding term root is 54702a... and proposition id is f5dfc0...

Proof:
Proof not loaded.

L200

Theorem. (iff_refl)

∀A : prop, A ↔ A

In Proofgold the corresponding term root is 01338d... and proposition id is 7b71b5...

Proof:
Proof not loaded.

L204

Theorem. (iff_sym)

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

In Proofgold the corresponding term root is 00bac1... and proposition id is 11f51b...

Proof:
Proof not loaded.

L213

Theorem. (iff_trans)

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

In Proofgold the corresponding term root is 363285... and proposition id is c3b8f1...

Proof:
Proof not loaded.

L226

Theorem. (eq_i_tra)

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

In Proofgold the corresponding term root is 193bbf... and proposition id is 7ecbc4...

Proof:
Proof not loaded.

L230

Theorem. (f_eq_i)

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

In Proofgold the corresponding term root is b0871b... and proposition id is 2a60fd...

Proof:
Proof not loaded.

L234

Theorem. (neq_i_sym)

∀x y, x ≠ y → y ≠ x

In Proofgold the corresponding term root is 5c0ec9... and proposition id is 1a9898...

Proof:
Proof not loaded.

L238

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

In Proofgold the corresponding term root is 36808c... and object id is 253451...

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

L244

Theorem. (Eps_i_ex)

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

In Proofgold the corresponding term root is be36f0... and proposition id is 6a2832...

Proof:
Proof not loaded.

L250

Theorem. (pred_ext)

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

In Proofgold the corresponding term root is e9e64b... and proposition id is d4b2d3...

Proof:
Proof not loaded.

L256

Theorem. (prop_ext_2)

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

In Proofgold the corresponding term root is a9ede2... and proposition id is a56fc7...

Proof:
Proof not loaded.

L262

Theorem. (Subq_ref)

∀X : set, X ⊆ X

In Proofgold the corresponding term root is 4c5395... and proposition id is 2efbac...

Proof:
Proof not loaded.

L266

Theorem. (Subq_tra)

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

In Proofgold the corresponding term root is 79accb... and proposition id is fed662...

Proof:
Proof not loaded.

L270

Theorem. (Subq_contra)

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

In Proofgold the corresponding term root is d15e87... and proposition id is bd5a2f...

Proof:
Proof not loaded.

L274

Theorem. (EmptyE)

∀x : set, x ∉ Empty

In Proofgold the corresponding term root is 93a77a... and proposition id is 8349ab...

Proof:
Proof not loaded.

L280

Theorem. (Subq_Empty)

∀X : set, Empty ⊆ X

In Proofgold the corresponding term root is a517cd... and proposition id is 2faec3...

Proof:
Proof not loaded.

L284

Theorem. (Empty_Subq_eq)

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

In Proofgold the corresponding term root is 2dd959... and proposition id is 988691...

Proof:
Proof not loaded.

L292

Theorem. (Empty_eq)

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

In Proofgold the corresponding term root is 3de0fd... and proposition id is 8b915b...

Proof:
Proof not loaded.

L302

Theorem. (UnionI)

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

In Proofgold the corresponding term root is 51b549... and proposition id is bade05...

Proof:
Proof not loaded.

L315

Theorem. (UnionE)

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

In Proofgold the corresponding term root is db4bc1... and proposition id is ab781b...

Proof:
Proof not loaded.

L319

Theorem. (UnionE_impred)

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

In Proofgold the corresponding term root is 8efd57... and proposition id is d621b2...

Proof:
Proof not loaded.

L327

Theorem. (PowerI)

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

In Proofgold the corresponding term root is 7143d7... and proposition id is 3c48d3...

Proof:
Proof not loaded.

L331

Theorem. (PowerE)

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

In Proofgold the corresponding term root is 149030... and proposition id is 647070...

Proof:
Proof not loaded.

L335

Theorem. (Empty_In_Power)

∀X : set, Empty ∈ 𝒫 X

In Proofgold the corresponding term root is d2656b... and proposition id is 487855...

Proof:
Proof not loaded.

L339

Theorem. (Self_In_Power)

∀X : set, X ∈ 𝒫 X

In Proofgold the corresponding term root is f81ef2... and proposition id is 8336ff...

Proof:
Proof not loaded.

L343

Theorem. (xm)

∀P : prop, P ∨ ¬ P

In Proofgold the corresponding term root is 62e4c3... and proposition id is 7b6737...

Proof:
Proof not loaded.

L395

Theorem. (dneg)

∀P : prop, ¬ ¬ P → P

In Proofgold the corresponding term root is 852f34... and proposition id is b7cc63...

Proof:
Proof not loaded.

L404

Theorem. (not_all_ex_demorgan_i)

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

In Proofgold the corresponding term root is 9bfa06... and proposition id is 4b1474...

Proof:
Proof not loaded.

L414

Theorem. (eq_or_nand)

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

In Proofgold the corresponding term root is 24ac29... and proposition id is d212ef...

Proof:
Proof not loaded.

L431

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

In Proofgold the corresponding term root is 163602... and object id is a0b944...

L433

Theorem. (exactly1of2_I1)

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

In Proofgold the corresponding term root is 8e1e45... and proposition id is 4f94fa...

Proof:
Proof not loaded.

L443

Theorem. (exactly1of2_I2)

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

In Proofgold the corresponding term root is c9fd90... and proposition id is 6c1ad9...

Proof:
Proof not loaded.

L453

Theorem. (exactly1of2_E)

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

In Proofgold the corresponding term root is 29b901... and proposition id is c67434...

Proof:
Proof not loaded.

L468

Theorem. (exactly1of2_or)

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

In Proofgold the corresponding term root is 18af73... and proposition id is e092f6...

Proof:
Proof not loaded.

L476

Theorem. (ReplI)

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

In Proofgold the corresponding term root is b146c5... and proposition id is f84982...

Proof:
Proof not loaded.

L486

Theorem. (ReplE)

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

In Proofgold the corresponding term root is 311cdf... and proposition id is d07e78...

Proof:
Proof not loaded.

L490

Theorem. (ReplE_impred)

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

In Proofgold the corresponding term root is 31e90a... and proposition id is 34fefd...

Proof:
Proof not loaded.

L499

Theorem. (ReplE')

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

In Proofgold the corresponding term root is e374fe... and proposition id is d4b7b0...

Proof:
Proof not loaded.

L506

Theorem. (Repl_Empty)

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

In Proofgold the corresponding term root is 2af2ac... and proposition id is 0835bc...

Proof:
Proof not loaded.

L517

Theorem. (ReplEq_ext_sub)

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

In Proofgold the corresponding term root is eb4c1d... and proposition id is 56aad0...

Proof:
Proof not loaded.

L532

Theorem. (ReplEq_ext)

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

In Proofgold the corresponding term root is 81eb90... and proposition id is 781846...

Proof:
Proof not loaded.

L541

Theorem. (Repl_inv_eq)

∀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

In Proofgold the corresponding term root is 968c7a... and proposition id is 9ce73d...

Proof:
Proof not loaded.

L565

Theorem. (Repl_invol_eq)

∀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

In Proofgold the corresponding term root is e15a6b... and proposition id is 5faff0...

Proof:
Proof not loaded.

L574

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.

In Proofgold the corresponding term root is b8ff52... and object id is 76c4c0...

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.

L577

Theorem. (If_i_correct)

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

In Proofgold the corresponding term root is 2a17ae... and proposition id is b5c26b...

Proof:
Proof not loaded.

L599

Theorem. (If_i_0)

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

In Proofgold the corresponding term root is fde1a8... and proposition id is a9abd3...

Proof:
Proof not loaded.

L610

Theorem. (If_i_1)

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

In Proofgold the corresponding term root is b1aa3f... and proposition id is a93c2c...

Proof:
Proof not loaded.

L621

Theorem. (If_i_or)

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

In Proofgold the corresponding term root is 3e1439... and proposition id is 4de742...

Proof:
Proof not loaded.

L630

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

In Proofgold the corresponding term root is 742438... and object id is dc3134...

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

L634

Theorem. (UPairE)

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

In Proofgold the corresponding term root is 5009cc... and proposition id is e67fc5...

Proof:
Proof not loaded.

L654

Theorem. (UPairI1)

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

In Proofgold the corresponding term root is b1eea2... and proposition id is bf3649...

Proof:
Proof not loaded.

L665

Theorem. (UPairI2)

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

In Proofgold the corresponding term root is 27455b... and proposition id is a0a5b8...

Proof:
Proof not loaded.

L678

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

In Proofgold the corresponding term root is bd01a8... and object id is b7dfc1...

Notation. {x} is notation for Sing x.

L680

Theorem. (SingI)

∀x : set, x ∈ {x}

In Proofgold the corresponding term root is 6591bd... and proposition id is 2f93be...

Proof:
Proof not loaded.

L684

Theorem. (SingE)

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

In Proofgold the corresponding term root is 9341fe... and proposition id is 3b0dd8...

Proof:
Proof not loaded.

L688

Theorem. (Sing_inj)

∀x y, {x} = {y} → x = y

In Proofgold the corresponding term root is dea1af... and proposition id is 96eb72...

Proof:
Proof not loaded.

L699

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

In Proofgold the corresponding term root is 5e1ac4... and object id is e14989...

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

L703

Theorem. (binunionI1)

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

In Proofgold the corresponding term root is 753b6e... and proposition id is e43c8d...

Proof:
Proof not loaded.

L713

Theorem. (binunionI2)

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

In Proofgold the corresponding term root is b8821c... and proposition id is 959535...

Proof:
Proof not loaded.

L723

Theorem. (binunionE)

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

In Proofgold the corresponding term root is 5a3195... and proposition id is 1ceeb0...

Proof:
Proof not loaded.

L746

Theorem. (binunionE')

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

In Proofgold the corresponding term root is e5b951... and proposition id is 570dd1...

Proof:
Proof not loaded.

L753

Theorem. (binunion_asso)

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

In Proofgold the corresponding term root is e0f701... and proposition id is 61dfba...

Proof:
Proof not loaded.

L779

Theorem. (binunion_com_Subq)

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

In Proofgold the corresponding term root is ee8f5a... and proposition id is d84076...

Proof:
Proof not loaded.

L787

Theorem. (binunion_com)

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

In Proofgold the corresponding term root is e20f4f... and proposition id is bed33e...

Proof:
Proof not loaded.

L793

Theorem. (binunion_idl)

∀X : set, Empty ∪ X = X

In Proofgold the corresponding term root is 8dc616... and proposition id is 52cd24...

Proof:
Proof not loaded.

L802

Theorem. (binunion_idr)

∀X : set, X ∪ Empty = X

In Proofgold the corresponding term root is 67e82f... and proposition id is d5a005...

Proof:
Proof not loaded.

L808

Theorem. (binunion_Subq_1)

∀X Y : set, X ⊆ X ∪ Y

In Proofgold the corresponding term root is b2c658... and proposition id is a9b3a8...

Proof:
Proof not loaded.

L812

Theorem. (binunion_Subq_2)

∀X Y : set, Y ⊆ X ∪ Y

In Proofgold the corresponding term root is 3cf229... and proposition id is 1507ce...

Proof:
Proof not loaded.

L816

Theorem. (binunion_Subq_min)

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

In Proofgold the corresponding term root is cc32a5... and proposition id is d64da4...

Proof:
Proof not loaded.

L827

Theorem. (Subq_binunion_eq)

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

In Proofgold the corresponding term root is f8ee53... and proposition id is c2d393...

Proof:
Proof not loaded.

L843

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

In Proofgold the corresponding term root is 1f3a09... and object id is 5bdda8...

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.

L849

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

In Proofgold the corresponding term root is b3e3bf... and object id is 241349...

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

L855

Theorem. (famunionI)

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

In Proofgold the corresponding term root is 0c23d0... and proposition id is e4f490...

Proof:
Proof not loaded.

L859

Theorem. (famunionE)

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

In Proofgold the corresponding term root is 48683a... and proposition id is ede6e5...

Proof:
Proof not loaded.

L880

Theorem. (famunionE_impred)

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

In Proofgold the corresponding term root is ab2266... and proposition id is 562023...

Proof:
Proof not loaded.

L888

Theorem. (famunion_Empty)

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

In Proofgold the corresponding term root is fc1bdd... and proposition id is 22bd10...

Proof:
Proof not loaded.

L895

Theorem. (famunion_Subq)

∀X, ∀f g : set → set, (∀x ∈ X, f x ⊆ g x) → famunion X f ⊆ famunion X g

In Proofgold the corresponding term root is 5f0b79... and proposition id is b1b158...

Proof:
Proof not loaded.

L905

Theorem. (famunion_ext)

∀X, ∀f g : set → set, (∀x ∈ X, f x = g x) → famunion X f = famunion X g

In Proofgold the corresponding term root is 8dc4c3... and proposition id is 5bc238...

Proof:
Proof not loaded.

Beginning of Section SepSec

L916

Variable X : set

L918

Variable P : set → prop

L919

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

L920

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

L923

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

In Proofgold the corresponding term root is f336a4... and object id is 7008ec...

End of Section SepSec

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

L929

Theorem. (SepI)

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

In Proofgold the corresponding term root is ea56bb... and proposition id is 147a6a...

Proof:
Proof not loaded.

L967

Theorem. (SepE)

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

In Proofgold the corresponding term root is 102830... and proposition id is 00899a...

Proof:
Proof not loaded.

L1018

Theorem. (SepE1)

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

In Proofgold the corresponding term root is d83445... and proposition id is 6399b0...

Proof:
Proof not loaded.

L1022

Theorem. (SepE2)

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

In Proofgold the corresponding term root is aa61ca... and proposition id is 104227...

Proof:
Proof not loaded.

L1026

Theorem. (Sep_Empty)

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

In Proofgold the corresponding term root is f36949... and proposition id is e3473a...

Proof:
Proof not loaded.

L1032

Theorem. (Sep_Subq)

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

In Proofgold the corresponding term root is 97d080... and proposition id is c17d45...

Proof:
Proof not loaded.

L1036

Theorem. (Sep_In_Power)

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

In Proofgold the corresponding term root is 612c94... and proposition id is fba53e...

Proof:
Proof not loaded.

L1042

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

In Proofgold the corresponding term root is ec807b... and object id is 9bdb56...

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

L1044

Theorem. (ReplSepI)

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

In Proofgold the corresponding term root is 35b8ec... and proposition id is aa7b2b...

Proof:
Proof not loaded.

L1048

Theorem. (ReplSepE)

∀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

In Proofgold the corresponding term root is 415ff1... and proposition id is b1bc76...

Proof:
Proof not loaded.

L1067

Theorem. (ReplSepE_impred)

∀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

In Proofgold the corresponding term root is 5d26e1... and proposition id is 063cea...

Proof:
Proof not loaded.

L1080

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

In Proofgold the corresponding term root is b2abd2... and object id is 2c68d8...

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

L1085

Theorem. (binintersectI)

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

In Proofgold the corresponding term root is fd656d... and proposition id is 9081a0...

Proof:
Proof not loaded.

L1089

Theorem. (binintersectE)

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

In Proofgold the corresponding term root is 463b5a... and proposition id is ca0636...

Proof:
Proof not loaded.

L1093

Theorem. (binintersectE1)

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

In Proofgold the corresponding term root is b12123... and proposition id is 51005e...

Proof:
Proof not loaded.

L1097

Theorem. (binintersectE2)

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

In Proofgold the corresponding term root is 39656f... and proposition id is 599de4...

Proof:
Proof not loaded.

L1101

Theorem. (binintersect_Subq_1)

∀X Y : set, X ∩ Y ⊆ X

In Proofgold the corresponding term root is f296ad... and proposition id is 303833...

Proof:
Proof not loaded.

L1105

Theorem. (binintersect_Subq_2)

∀X Y : set, X ∩ Y ⊆ Y

In Proofgold the corresponding term root is fcd5f5... and proposition id is 8b9fd2...

Proof:
Proof not loaded.

L1109

Theorem. (binintersect_Subq_eq_1)

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

In Proofgold the corresponding term root is 277eec... and proposition id is ec1cc3...

Proof:
Proof not loaded.

L1120

Theorem. (binintersect_Subq_max)

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

In Proofgold the corresponding term root is 95624d... and proposition id is 64636b...

Proof:
Proof not loaded.

L1131

Theorem. (binintersect_com_Subq)

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

In Proofgold the corresponding term root is 410255... and proposition id is 5977b8...

Proof:
Proof not loaded.

L1137

Theorem. (binintersect_com)

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

In Proofgold the corresponding term root is 1a2c6f... and proposition id is ea8a1c...

Proof:
Proof not loaded.

L1145

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

In Proofgold the corresponding term root is c68e5a... and object id is 913da1...

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

L1150

Theorem. (setminusI)

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

In Proofgold the corresponding term root is 0feeb8... and proposition id is 80db6a...

Proof:
Proof not loaded.

L1154

Theorem. (setminusE)

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

In Proofgold the corresponding term root is 6774f4... and proposition id is 71763a...

Proof:
Proof not loaded.

L1158

Theorem. (setminusE1)

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

In Proofgold the corresponding term root is 064bd5... and proposition id is d74baf...

Proof:
Proof not loaded.

L1162

Theorem. (setminusE2)

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

In Proofgold the corresponding term root is 3e6969... and proposition id is 36b273...

Proof:
Proof not loaded.

L1166

Theorem. (setminus_Subq)

∀X Y : set, X ∖ Y ⊆ X

In Proofgold the corresponding term root is 5a497a... and proposition id is 66f982...

Proof:
Proof not loaded.

L1170

Theorem. (setminus_Subq_contra)

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

In Proofgold the corresponding term root is b1f440... and proposition id is 9a06b2...

Proof:
Proof not loaded.

L1184

Theorem. (setminus_In_Power)

∀A U, A ∖ U ∈ 𝒫 A

In Proofgold the corresponding term root is 062275... and proposition id is f503e1...

Proof:
Proof not loaded.

L1188

Theorem. (setminus_idr)

∀X, X ∖ Empty = X

In Proofgold the corresponding term root is 20e108... and proposition id is ebb8ec...

Proof:
Proof not loaded.

L1198

Theorem. (In_irref)

∀x, x ∉ x

In Proofgold the corresponding term root is 12629a... and proposition id is 7bfd46...

Proof:
Proof not loaded.

L1207

Theorem. (In_no2cycle)

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

In Proofgold the corresponding term root is 6d0cb3... and proposition id is 344f30...

Proof:
Proof not loaded.

L1219

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

In Proofgold the corresponding term root is 65d883... and object id is 1452f7...

L1220

Theorem. (ordsuccI1)

∀x : set, x ⊆ ordsucc x

In Proofgold the corresponding term root is 5a2f15... and proposition id is 367d80...

Proof:
Proof not loaded.

L1225

Theorem. (ordsuccI2)

∀x : set, x ∈ ordsucc x

In Proofgold the corresponding term root is 2f6efd... and proposition id is 2be6be...

Proof:
Proof not loaded.

L1229

Theorem. (ordsuccE)

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

In Proofgold the corresponding term root is 01c4ee... and proposition id is 3849f5...

Proof:
Proof not loaded.

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

L1239

Theorem. (neq_0_ordsucc)

∀a : set, 0 ≠ ordsucc a

In Proofgold the corresponding term root is 1b20cb... and proposition id is 04c410...

Proof:
Proof not loaded.

L1247

Theorem. (neq_ordsucc_0)

∀a : set, ordsucc a ≠ 0

In Proofgold the corresponding term root is 9b391e... and proposition id is 346ee0...

Proof:
Proof not loaded.

L1251

Theorem. (ordsucc_inj)

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

In Proofgold the corresponding term root is 40cad6... and proposition id is 4869a1...

Proof:
Proof not loaded.

L1272

Theorem. (ordsucc_inj_contra)

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

In Proofgold the corresponding term root is 791304... and proposition id is 66f4df...

Proof:
Proof not loaded.

L1279

Theorem. (In_0_1)

0 ∈ 1

In Proofgold the corresponding term root is e984b0... and proposition id is 3be80a...

Proof:
Proof not loaded.

L1283

Theorem. (In_0_2)

0 ∈ 2

In Proofgold the corresponding term root is 56dc2c... and proposition id is 5a202e...

Proof:
Proof not loaded.

L1287

Theorem. (In_1_2)

1 ∈ 2

In Proofgold the corresponding term root is 8704b3... and proposition id is 431e9e...

Proof:
Proof not loaded.

L1291

Theorem. (In_1_3)

1 ∈ 3

In Proofgold the corresponding term root is 85201c... and proposition id is 8f3cec...

Proof:
Proof not loaded.

L1295

Theorem. (In_2_3)

2 ∈ 3

In Proofgold the corresponding term root is 4d67ce... and proposition id is ebdb5d...

Proof:
Proof not loaded.

L1299

Theorem. (In_1_4)

1 ∈ 4

In Proofgold the corresponding term root is 5cabbb... and proposition id is 1e2d5b...

Proof:
Proof not loaded.

L1303

Theorem. (In_2_4)

2 ∈ 4

In Proofgold the corresponding term root is 33c2ff... and proposition id is 2cbb94...

Proof:
Proof not loaded.

L1307

Theorem. (In_3_4)

3 ∈ 4

In Proofgold the corresponding term root is f25e44... and proposition id is 22a0af...

Proof:
Proof not loaded.

L1311

Theorem. (In_1_5)

1 ∈ 5

In Proofgold the corresponding term root is be96a3... and proposition id is 34c02d...

Proof:
Proof not loaded.

L1315

Theorem. (In_2_5)

2 ∈ 5

In Proofgold the corresponding term root is ec68b2... and proposition id is 7ed8e4...

Proof:
Proof not loaded.

L1319

Theorem. (In_3_5)

3 ∈ 5

In Proofgold the corresponding term root is eddd36... and proposition id is df92fe...

Proof:
Proof not loaded.

L1323

Theorem. (In_4_5)

4 ∈ 5

In Proofgold the corresponding term root is e72ad7... and proposition id is 03b9ff...

Proof:
Proof not loaded.

L1327

Theorem. (In_1_6)

1 ∈ 6

In Proofgold the corresponding term root is 4c8428... and proposition id is 327244...

Proof:
Proof not loaded.

L1331

Theorem. (In_1_7)

1 ∈ 7

In Proofgold the corresponding term root is aa5cde... and proposition id is 392ce8...

Proof:
Proof not loaded.

L1335

Theorem. (In_1_8)

1 ∈ 8

In Proofgold the corresponding term root is fbef0f... and proposition id is 0d7bd5...

Proof:
Proof not loaded.

L1339

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.

In Proofgold the corresponding term root is 458be3... and object id is cfd8eb...

L1341

Theorem. (nat_0)

nat_p 0

In Proofgold the corresponding term root is 1617bc... and proposition id is 457a72...

Proof:
Proof not loaded.

L1345

Theorem. (nat_ordsucc)

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

In Proofgold the corresponding term root is 87f001... and proposition id is 57e940...

Proof:
Proof not loaded.

L1349

Theorem. (nat_1)

nat_p 1

In Proofgold the corresponding term root is 2f83fa... and proposition id is 672d0d...

Proof:
Proof not loaded.

L1353

Theorem. (nat_2)

nat_p 2

In Proofgold the corresponding term root is a8be15... and proposition id is 9112e9...

Proof:
Proof not loaded.

L1357

Theorem. (nat_3)

nat_p 3

In Proofgold the corresponding term root is c0849f... and proposition id is 133bb7...

Proof:
Proof not loaded.

L1361

Theorem. (nat_4)

nat_p 4

In Proofgold the corresponding term root is 2c8e1a... and proposition id is 69ffc3...

Proof:
Proof not loaded.

L1365

Theorem. (nat_5)

nat_p 5

In Proofgold the corresponding term root is 1a2477... and proposition id is b84b25...

Proof:
Proof not loaded.

L1369

Theorem. (nat_6)

nat_p 6

In Proofgold the corresponding term root is 25de88... and proposition id is b4ec67...

Proof:
Proof not loaded.

L1373

Theorem. (nat_7)

nat_p 7

In Proofgold the corresponding term root is c2e74e... and proposition id is 86ad85...

Proof:
Proof not loaded.

L1377

Theorem. (nat_8)

nat_p 8

In Proofgold the corresponding term root is 18883c... and proposition id is f93125...

Proof:
Proof not loaded.

L1381

Theorem. (nat_0_in_ordsucc)

∀n, nat_p n → 0 ∈ ordsucc n

In Proofgold the corresponding term root is 9b50b9... and proposition id is 251f3d...

Proof:
Proof not loaded.

L1393

Theorem. (nat_ordsucc_in_ordsucc)

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

In Proofgold the corresponding term root is 819399... and proposition id is 4c2c95...

Proof:
Proof not loaded.

L1419

Theorem. (nat_ind)

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

In Proofgold the corresponding term root is 5d06f5... and proposition id is ecdce8...

Proof:
Proof not loaded.

L1447

Theorem. (nat_inv_impred)

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

In Proofgold the corresponding term root is eddc5f... and proposition id is 175e22...

Proof:
Proof not loaded.

L1451

Theorem. (nat_inv)

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

In Proofgold the corresponding term root is 5d4296... and proposition id is 4f4167...

Proof:
Proof not loaded.

L1459

Theorem. (nat_complete_ind)

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

In Proofgold the corresponding term root is d32e5b... and proposition id is 1e1608...

Proof:
Proof not loaded.

L1490

Theorem. (nat_p_trans)

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

In Proofgold the corresponding term root is e88449... and proposition id is 03b874...

Proof:
Proof not loaded.

L1511

Theorem. (nat_trans)

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

In Proofgold the corresponding term root is 6bc6e1... and proposition id is cad6fe...

Proof:
Proof not loaded.

L1537

Theorem. (nat_ordsucc_trans)

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

In Proofgold the corresponding term root is e42e58... and proposition id is bc868d...

Proof:
Proof not loaded.

L1553

Theorem. (Union_ordsucc_eq)

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

In Proofgold the corresponding term root is 87308c... and proposition id is e8cdeb...

Proof:
Proof not loaded.

L1576

Theorem. (cases_1)

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

In Proofgold the corresponding term root is 706605... and proposition id is c6f0c0...

Proof:
Proof not loaded.

L1585

Theorem. (cases_2)

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

In Proofgold the corresponding term root is 4693b2... and proposition id is 74563a...

Proof:
Proof not loaded.

L1594

Theorem. (cases_3)

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

In Proofgold the corresponding term root is 2a0ca2... and proposition id is 1a8a20...

Proof:
Proof not loaded.

L1603

Theorem. (neq_0_1)

0 ≠ 1

In Proofgold the corresponding term root is 9630fd... and proposition id is 74867a...

Proof:
Proof not loaded.

L1607

Theorem. (neq_1_0)

1 ≠ 0

In Proofgold the corresponding term root is 3a0478... and proposition id is 952fed...

Proof:
Proof not loaded.

L1611

Theorem. (neq_0_2)

0 ≠ 2

In Proofgold the corresponding term root is 055580... and proposition id is 9c9a3f...

Proof:
Proof not loaded.

L1615

Theorem. (neq_2_0)

2 ≠ 0

In Proofgold the corresponding term root is 4d54d8... and proposition id is 00b357...

Proof:
Proof not loaded.

L1619

Theorem. (neq_1_2)

1 ≠ 2

In Proofgold the corresponding term root is 1d088a... and proposition id is e5542e...

Proof:
Proof not loaded.

L1623

Theorem. (neq_1_3)

1 ≠ 3

In Proofgold the corresponding term root is d3b293... and proposition id is c0a1f7...

Proof:
Proof not loaded.

L1628

Theorem. (neq_2_3)

2 ≠ 3

In Proofgold the corresponding term root is 9a904f... and proposition id is 2cd643...

Proof:
Proof not loaded.

L1633

Theorem. (neq_2_4)

2 ≠ 4

In Proofgold the corresponding term root is 0bb647... and proposition id is c4e5df...

Proof:
Proof not loaded.

L1638

Theorem. (neq_3_4)

3 ≠ 4

In Proofgold the corresponding term root is 031ec9... and proposition id is 66a378...

Proof:
Proof not loaded.

L1643

Theorem. (ZF_closed_E)

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

In Proofgold the corresponding term root is d795d4... and proposition id is c78c79...

Proof:
Proof not loaded.

L1652

Theorem. (ZF_Union_closed)

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

In Proofgold the corresponding term root is a7cdf1... and proposition id is 250496...

Proof:
Proof not loaded.

L1657

Theorem. (ZF_Power_closed)

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

In Proofgold the corresponding term root is 5d781f... and proposition id is 7411dd...

Proof:
Proof not loaded.

L1662

Theorem. (ZF_Repl_closed)

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

In Proofgold the corresponding term root is 312268... and proposition id is 18f8ac...

Proof:
Proof not loaded.

L1667

Theorem. (ZF_UPair_closed)

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

In Proofgold the corresponding term root is 54256a... and proposition id is ef42d3...

Proof:
Proof not loaded.

L1751

Theorem. (ZF_Sing_closed)

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

In Proofgold the corresponding term root is 5d8a83... and proposition id is d02d66...

Proof:
Proof not loaded.

L1756

Theorem. (ZF_binunion_closed)

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

In Proofgold the corresponding term root is 8a6240... and proposition id is 1bacfd...

Proof:
Proof not loaded.

L1761

Theorem. (ZF_ordsucc_closed)

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

In Proofgold the corresponding term root is 68a6ba... and proposition id is 946e61...

Proof:
Proof not loaded.

L1766

Theorem. (nat_p_UnivOf_Empty)

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

In Proofgold the corresponding term root is c885b4... and proposition id is 645aee...

Proof:
Proof not loaded.

L1780

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

In Proofgold the corresponding term root is 6fc30a... and object id is ad9ad8...

L1781

Theorem. (omega_nat_p)

∀n ∈ ω, nat_p n

In Proofgold the corresponding term root is f44a30... and proposition id is c2c61b...

Proof:
Proof not loaded.

L1785

Theorem. (nat_p_omega)

∀n : set, nat_p n → n ∈ ω

In Proofgold the corresponding term root is 6a1b44... and proposition id is d5080f...

Proof:
Proof not loaded.

L1794

Theorem. (omega_ordsucc)

∀n ∈ ω, ordsucc n ∈ ω

In Proofgold the corresponding term root is 246d63... and proposition id is 17fb64...

Proof:
Proof not loaded.

L1802

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

In Proofgold the corresponding term root is ee28d9... and object id is 53ee8f...

L1804

Theorem. (ordinal_TransSet)

∀alpha : set, ordinal alpha → TransSet alpha

In Proofgold the corresponding term root is 0dbaa3... and proposition id is c9e708...

Proof:
Proof not loaded.

L1808

Theorem. (ordinal_Empty)

ordinal Empty

In Proofgold the corresponding term root is ce6bea... and proposition id is 7d95d1...

Proof:
Proof not loaded.

L1821

Theorem. (ordinal_Hered)

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

In Proofgold the corresponding term root is a7e78b... and proposition id is 43b0f3...

Proof:
Proof not loaded.

L1841

Theorem. (TransSet_ordsucc)

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

In Proofgold the corresponding term root is fc2157... and proposition id is ebf9e3...

Proof:
Proof not loaded.

L1862

Theorem. (ordinal_ordsucc)

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

In Proofgold the corresponding term root is 0ba97f... and proposition id is ab0f7f...

Proof:
Proof not loaded.

L1882

Theorem. (nat_p_ordinal)

∀n : set, nat_p n → ordinal n

In Proofgold the corresponding term root is 274fc4... and proposition id is 47cd49...

Proof:
Proof not loaded.

L1893

Theorem. (ordinal_1)

ordinal 1

In Proofgold the corresponding term root is c94d41... and proposition id is e325a5...

Proof:
Proof not loaded.

L1897

Theorem. (ordinal_2)

ordinal 2

In Proofgold the corresponding term root is a57075... and proposition id is e64a0d...

Proof:
Proof not loaded.

L1901

Theorem. (omega_TransSet)

TransSet ω

In Proofgold the corresponding term root is 8e89e6... and proposition id is c79e75...

Proof:
Proof not loaded.

L1914

Theorem. (omega_ordinal)

ordinal ω

In Proofgold the corresponding term root is 3d621a... and proposition id is 177484...

Proof:
Proof not loaded.

L1928

Theorem. (ordsucc_omega_ordinal)

ordinal (ordsucc ω)

In Proofgold the corresponding term root is 66659c... and proposition id is ecfad7...

Proof:
Proof not loaded.

L1932

Theorem. (TransSet_ordsucc_In_Subq)

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

In Proofgold the corresponding term root is d5d882... and proposition id is 3c2e45...

Proof:
Proof not loaded.

L1949

Theorem. (ordinal_ordsucc_In_Subq)

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

In Proofgold the corresponding term root is 57345e... and proposition id is b00304...

Proof:
Proof not loaded.

L1955

Theorem. (ordinal_trichotomy_or)

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

In Proofgold the corresponding term root is 078a34... and proposition id is 21f2d6...

Proof:
Proof not loaded.

L2023

Theorem. (ordinal_trichotomy_or_impred)

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

In Proofgold the corresponding term root is 7c0f0b... and proposition id is bb6d2d...

Proof:
Proof not loaded.

L2028

Theorem. (ordinal_In_Or_Subq)

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

In Proofgold the corresponding term root is 70fe0d... and proposition id is 7b99b0...

Proof:
Proof not loaded.

L2045

Theorem. (ordinal_linear)

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

In Proofgold the corresponding term root is 3f30a5... and proposition id is 3b1fce...

Proof:
Proof not loaded.

L2058

Theorem. (ordinal_ordsucc_In_eq)

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

In Proofgold the corresponding term root is 500378... and proposition id is 0c19e7...

Proof:
Proof not loaded.

L2075

Theorem. (ordinal_lim_or_succ)

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

In Proofgold the corresponding term root is 4450c0... and proposition id is a12697...

Proof:
Proof not loaded.

L2090

Theorem. (ordinal_ordsucc_In)

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

In Proofgold the corresponding term root is f4b1ed... and proposition id is 8ab1dc...

Proof:
Proof not loaded.

L2105

Theorem. (ordinal_famunion)

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

In Proofgold the corresponding term root is fc0359... and proposition id is b3f1e1...

Proof:
Proof not loaded.

L2136

Theorem. (ordinal_binintersect)

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

In Proofgold the corresponding term root is 43d507... and proposition id is 025328...

Proof:
Proof not loaded.

L2150

Theorem. (ordinal_binunion)

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

In Proofgold the corresponding term root is 861ae3... and proposition id is b24989...

Proof:
Proof not loaded.

L2165

Theorem. (ordinal_ind)

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

In Proofgold the corresponding term root is bb5575... and proposition id is 973cd8...

Proof:
Proof not loaded.

L2185

Theorem. (least_ordinal_ex)

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

In Proofgold the corresponding term root is df6c77... and proposition id is ab6fe1...

Proof:
Proof not loaded.

L2207

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.

In Proofgold the corresponding term root is 264b04... and object id is 442958...

L2213

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.

In Proofgold the corresponding term root is 76bef6... and object id is f7d93b...

L2221

Theorem. (bijI)

∀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

In Proofgold the corresponding term root is a9064f... and proposition id is 3229f9...

Proof:
Proof not loaded.

L2236

Theorem. (bijE)

∀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

In Proofgold the corresponding term root is 2cf278... and proposition id is cf0759...

Proof:
Proof not loaded.

L2252

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.

In Proofgold the corresponding term root is 896fa9... and object id is f3a015...

L2253

Theorem. (surj_rinv)

∀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

In Proofgold the corresponding term root is ebf371... and proposition id is 6489d2...

Proof:
Proof not loaded.

L2262

Theorem. (inj_linv)

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

In Proofgold the corresponding term root is 18ecce... and proposition id is d16557...

Proof:
Proof not loaded.

L2277

Theorem. (bij_inv)

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

In Proofgold the corresponding term root is ff1332... and proposition id is 69c537...

Proof:
Proof not loaded.

L2318

Theorem. (bij_id)

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

In Proofgold the corresponding term root is a8cefb... and proposition id is 707f37...

Proof:
Proof not loaded.

L2329

Theorem. (bij_comp)

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

In Proofgold the corresponding term root is abf851... and proposition id is 4c9045...

Proof:
Proof not loaded.

L2361

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

In Proofgold the corresponding term root is eb4419... and object id is 7f2bf6...

L2364

Theorem. (equip_ref)

∀X, equip X X

In Proofgold the corresponding term root is cc7e80... and proposition id is c41fb1...

Proof:
Proof not loaded.

L2371

Theorem. (equip_sym)

∀X Y, equip X Y → equip Y X

In Proofgold the corresponding term root is f28954... and proposition id is 272f04...

Proof:
Proof not loaded.

L2380

Theorem. (equip_tra)

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

In Proofgold the corresponding term root is 322bfb... and proposition id is d616c1...

Proof:
Proof not loaded.

L2391

Theorem. (equip_0_Empty)

∀X, equip X 0 → X = 0

In Proofgold the corresponding term root is 83ab2f... and proposition id is 4c101c...

Proof:
Proof not loaded.

Beginning of Section SchroederBernstein

L2406

Theorem. (KnasterTarski_set)

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

In Proofgold the corresponding term root is 2ffb9f... and proposition id is 31ef9d...

Proof:
Proof not loaded.

L2447

Theorem. (image_In_Power)

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

In Proofgold the corresponding term root is 6799e8... and proposition id is 43ed06...

Proof:
Proof not loaded.

L2460

Theorem. (image_monotone)

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

In Proofgold the corresponding term root is ac6fe8... and proposition id is f923c6...

Proof:
Proof not loaded.

L2471

Theorem. (setminus_antimonotone)

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

In Proofgold the corresponding term root is 67bd0e... and proposition id is f9b735...

Proof:
Proof not loaded.

L2479

Theorem. (SchroederBernstein)

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

In Proofgold the corresponding term root is e247a8... and proposition id is 03a2cd...

Proof:
Proof not loaded.

End of Section SchroederBernstein

Beginning of Section PigeonHole

L2637

Theorem. (PigeonHole_nat)

∀n, nat_p n → ∀f : set → set, (∀i ∈ ordsucc n, f i ∈ n) → ¬ (∀i j ∈ ordsucc n, f i = f j → i = j)

In Proofgold the corresponding term root is d756b7... and proposition id is 604a84...

Proof:
Proof not loaded.

L2784

Theorem. (PigeonHole_nat_bij)

∀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

In Proofgold the corresponding term root is cd3b8d... and proposition id is 44a08f...

Proof:
Proof not loaded.

End of Section PigeonHole

L2862

Definition. We define finite to be λX ⇒ ∃n ∈ ω, equip X n of type set → prop.

In Proofgold the corresponding term root is 04632d... and object id is 4c54a5...

L2864

Theorem. (finite_ind)

∀p : set → prop, p Empty → (∀X y, finite X → y ∉ X → p X → p (X ∪ {y})) → ∀X, finite X → p X

In Proofgold the corresponding term root is c53cb1... and proposition id is 19baca...

Proof:
Proof not loaded.

L2956

Theorem. (finite_Empty)

finite 0

In Proofgold the corresponding term root is c073c6... and proposition id is ec2c27...

Proof:
Proof not loaded.

L2963

Theorem. (adjoin_finite)

∀X y, finite X → finite (X ∪ {y})

In Proofgold the corresponding term root is def317... and proposition id is e6aa6d...

Proof:
Proof not loaded.

L3046

Theorem. (binunion_finite)

∀X, finite X → ∀Y, finite Y → finite (X ∪ Y)

In Proofgold the corresponding term root is fc26bb... and proposition id is 3365a6...

Proof:
Proof not loaded.

L3061

Theorem. (famunion_nat_finite)

∀X : set → set, ∀n, nat_p n → (∀i ∈ n, finite (X i)) → finite (⋃_{i ∈ n}X i)

In Proofgold the corresponding term root is 7f709a... and proposition id is f84ed0...

Proof:
Proof not loaded.

L3100

Theorem. (Subq_finite)

∀X, finite X → ∀Y, Y ⊆ X → finite Y

In Proofgold the corresponding term root is 6b062c... and proposition id is e4e3ee...

Proof:
Proof not loaded.

L3153

Theorem. (TransSet_In_ordsucc_Subq)

∀x y, TransSet y → x ∈ ordsucc y → x ⊆ y

In Proofgold the corresponding term root is f80c6e... and proposition id is 341993...

Proof:
Proof not loaded.

L3159

Theorem. (exandE_i)

∀P Q : set → prop, (∃x, P x ∧ Q x) → ∀r : prop, (∀x, P x → Q x → r) → r

In Proofgold the corresponding term root is 083f82... and proposition id is b1b26e...

Proof:
Proof not loaded.

L3164

Theorem. (exandE_ii)

∀P Q : (set → set) → prop, (∃x : set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set, P x → Q x → p) → p

In Proofgold the corresponding term root is c3e995... and proposition id is ed9d65...

Proof:
Proof not loaded.

L3171

Theorem. (exandE_iii)

∀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

In Proofgold the corresponding term root is 028a8f... and proposition id is 80b3b0...

Proof:
Proof not loaded.

L3178

Theorem. (exandE_iiii)

∀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

In Proofgold the corresponding term root is 7807d4... and proposition id is d1536a...

Proof:
Proof not loaded.

Beginning of Section Descr_ii

L3187

Variable P : (set → set) → prop

L3191

Definition. We define Descr_ii to be λx : set ⇒ Eps_i (λy ⇒ ∀h : set → set, P h → h x = y) of type set → set.

In Proofgold the corresponding term root is 3bae39... and object id is 3a4ad2...

L3192

Hypothesis Pex : ∃f : set → set, P f

L3194

Hypothesis Puniq : ∀f g : set → set, P f → P g → f = g

L3195

Theorem. (Descr_ii_prop)

P Descr_ii

In Proofgold the corresponding term root is 45bfc0... and proposition id is e705d1...

Proof:
Proof not loaded.

End of Section Descr_ii

Beginning of Section Descr_iii

L3216

Variable P : (set → set → set) → prop

L3220

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.

In Proofgold the corresponding term root is ca5fc1... and object id is 877e40...

L3221

Hypothesis Pex : ∃f : set → set → set, P f

L3223

Hypothesis Puniq : ∀f g : set → set → set, P f → P g → f = g

L3224

Theorem. (Descr_iii_prop)

P Descr_iii

In Proofgold the corresponding term root is 261c3d... and proposition id is 160421...

Proof:
Proof not loaded.

End of Section Descr_iii

Beginning of Section Descr_Vo1

L3247

Variable P : Vo 1 → prop

L3251

Definition. We define Descr_Vo1 to be λx : set ⇒ ∀h : set → prop, P h → h x of type Vo 1.

In Proofgold the corresponding term root is 615c0a... and object id is a4ecdd...

L3252

Hypothesis Pex : ∃f : Vo 1, P f

L3254

Hypothesis Puniq : ∀f g : Vo 1, P f → P g → f = g

L3255

Theorem. (Descr_Vo1_prop)

P Descr_Vo1

In Proofgold the corresponding term root is f550ef... and proposition id is 2213e2...

Proof:
Proof not loaded.

End of Section Descr_Vo1

Beginning of Section If_ii

L3275

Variable p : prop

L3277

Variable f g : set → set

L3280

Definition. We define If_ii to be λx ⇒ if p then f x else g x of type set → set.

In Proofgold the corresponding term root is 17057f... and object id is e29015...

L3281

Theorem. (If_ii_1)

p → If_ii = f

In Proofgold the corresponding term root is 31521e... and proposition id is 342a1f...

Proof:
Proof not loaded.

L3288

Theorem. (If_ii_0)

¬ p → If_ii = g

In Proofgold the corresponding term root is 6acab0... and proposition id is 36418b...

Proof:
Proof not loaded.

End of Section If_ii

Beginning of Section If_iii

L3299

Variable p : prop

L3301

Variable f g : set → set → set

L3304

Definition. We define If_iii to be λx y ⇒ if p then f x y else g x y of type set → set → set.

In Proofgold the corresponding term root is 331476... and object id is dd7e2b...

L3305

Theorem. (If_iii_1)

p → If_iii = f

In Proofgold the corresponding term root is 2d62ee... and proposition id is 48bc10...

Proof:
Proof not loaded.

L3315

Theorem. (If_iii_0)

¬ p → If_iii = g

In Proofgold the corresponding term root is 9b77d9... and proposition id is d11201...

Proof:
Proof not loaded.

End of Section If_iii

Beginning of Section EpsilonRec_i

L3329

Variable F : set → (set → set) → set

L3331

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.

In Proofgold the corresponding term root is fde509... and object id is a81e18...

L3339

Definition. We define In_rec_i to be λX ⇒ Eps_i (In_rec_i_G X) of type set → set.

In Proofgold the corresponding term root is fac413... and object id is 93aac4...

L3340

Theorem. (In_rec_i_G_c)

∀X : set, ∀f : set → set, (∀x ∈ X, In_rec_i_G x (f x)) → In_rec_i_G X (F X f)

In Proofgold the corresponding term root is 4da597... and proposition id is bc452e...

Proof:
Proof not loaded.

L3356

Theorem. (In_rec_i_G_inv)

∀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

In Proofgold the corresponding term root is ba1774... and proposition id is 5cfac2...

Proof:
Proof not loaded.

L3379

Hypothesis Fr : ∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h

L3381

Theorem. (In_rec_i_G_f)

∀X : set, ∀Y Z : set, In_rec_i_G X Y → In_rec_i_G X Z → Y = Z

In Proofgold the corresponding term root is 25f7ff... and proposition id is 02b4e4...

Proof:
Proof not loaded.

L3412

Theorem. (In_rec_i_G_In_rec_i)

∀X : set, In_rec_i_G X (In_rec_i X)

In Proofgold the corresponding term root is 095407... and proposition id is dc2359...

Proof:
Proof not loaded.

L3423

Theorem. (In_rec_i_G_In_rec_i_d)

∀X : set, In_rec_i_G X (F X In_rec_i)

In Proofgold the corresponding term root is b480fe... and proposition id is 5b92ff...

Proof:
Proof not loaded.

L3431

Theorem. (In_rec_i_eq)

∀X : set, In_rec_i X = F X In_rec_i

In Proofgold the corresponding term root is 110653... and proposition id is e8653b...

Proof:
Proof not loaded.

End of Section EpsilonRec_i

Beginning of Section EpsilonRec_ii

L3439

Variable F : set → (set → (set → set)) → (set → set)

L3441

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.

In Proofgold the corresponding term root is 6edba9... and object id is b31dbf...

L3449

Definition. We define In_rec_ii to be λX ⇒ Descr_ii (In_rec_G_ii X) of type set → (set → set).

In Proofgold the corresponding term root is f3c9ab... and object id is 3841bd...

L3450

Theorem. (In_rec_G_ii_c)

∀X : set, ∀f : set → (set → set), (∀x ∈ X, In_rec_G_ii x (f x)) → In_rec_G_ii X (F X f)

In Proofgold the corresponding term root is 381613... and proposition id is 49fbeb...

Proof:
Proof not loaded.

L3466

Theorem. (In_rec_G_ii_inv)

∀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

In Proofgold the corresponding term root is 336cfe... and proposition id is b4a180...

Proof:
Proof not loaded.

L3489

Hypothesis Fr : ∀X : set, ∀g h : set → (set → set), (∀x ∈ X, g x = h x) → F X g = F X h

L3491

Theorem. (In_rec_G_ii_f)

∀X : set, ∀Y Z : (set → set), In_rec_G_ii X Y → In_rec_G_ii X Z → Y = Z

In Proofgold the corresponding term root is 64b6e8... and proposition id is a3826b...

Proof:
Proof not loaded.

L3522

Theorem. (In_rec_G_ii_In_rec_ii)

∀X : set, In_rec_G_ii X (In_rec_ii X)

In Proofgold the corresponding term root is b2f81f... and proposition id is 2893f4...

Proof:
Proof not loaded.

L3535

Theorem. (In_rec_G_ii_In_rec_ii_d)

∀X : set, In_rec_G_ii X (F X In_rec_ii)

In Proofgold the corresponding term root is 2ff1ca... and proposition id is f12072...

Proof:
Proof not loaded.

L3543

Theorem. (In_rec_ii_eq)

∀X : set, In_rec_ii X = F X In_rec_ii

In Proofgold the corresponding term root is f7aff6... and proposition id is 7bb1e9...

Proof:
Proof not loaded.

End of Section EpsilonRec_ii

Beginning of Section EpsilonRec_iii

L3551

Variable F : set → (set → (set → set → set)) → (set → set → set)

L3553

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.

In Proofgold the corresponding term root is 533cc7... and object id is 7a2f6b...

L3561

Definition. We define In_rec_iii to be λX ⇒ Descr_iii (In_rec_G_iii X) of type set → (set → set → set).

In Proofgold the corresponding term root is 9b3a85... and object id is 651077...

L3562

Theorem. (In_rec_G_iii_c)

∀X : set, ∀f : set → (set → set → set), (∀x ∈ X, In_rec_G_iii x (f x)) → In_rec_G_iii X (F X f)

In Proofgold the corresponding term root is 4ea572... and proposition id is a7d90f...

Proof:
Proof not loaded.

L3578

Theorem. (In_rec_G_iii_inv)

∀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

In Proofgold the corresponding term root is 5f6e0c... and proposition id is f47dae...

Proof:
Proof not loaded.

L3601

Hypothesis Fr : ∀X : set, ∀g h : set → (set → set → set), (∀x ∈ X, g x = h x) → F X g = F X h

L3603

Theorem. (In_rec_G_iii_f)

∀X : set, ∀Y Z : (set → set → set), In_rec_G_iii X Y → In_rec_G_iii X Z → Y = Z

In Proofgold the corresponding term root is 574d71... and proposition id is 40978a...

Proof:
Proof not loaded.

L3634

Theorem. (In_rec_G_iii_In_rec_iii)

∀X : set, In_rec_G_iii X (In_rec_iii X)

In Proofgold the corresponding term root is d8c3ba... and proposition id is 37f9a7...

Proof:
Proof not loaded.

L3647

Theorem. (In_rec_G_iii_In_rec_iii_d)

∀X : set, In_rec_G_iii X (F X In_rec_iii)

In Proofgold the corresponding term root is 60c6d7... and proposition id is c05f77...

Proof:
Proof not loaded.

L3655

Theorem. (In_rec_iii_eq)

∀X : set, In_rec_iii X = F X In_rec_iii

In Proofgold the corresponding term root is 5f0574... and proposition id is a0709d...

Proof:
Proof not loaded.

End of Section EpsilonRec_iii

Beginning of Section NatRec

L3663

Variable z : set

L3665

Variable f : set → set → set

L3666

Let F : set → (set → set) → set ≝ λn g ⇒ if ⋃ n ∈ n then f (⋃ n) (g (⋃ n)) else z

L3667

Definition. We define nat_primrec to be In_rec_i F of type set → set.

In Proofgold the corresponding term root is 3be1c5... and object id is 1a64d5...

L3669

Theorem. (nat_primrec_r)

∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h

In Proofgold the corresponding term root is c955cd... and proposition id is 9ba887...

Proof:
Proof not loaded.

L3689

Theorem. (nat_primrec_0)

nat_primrec 0 = z

In Proofgold the corresponding term root is 416eaf... and proposition id is be11a2...

Proof:
Proof not loaded.

L3697

Theorem. (nat_primrec_S)

∀n : set, nat_p n → nat_primrec (ordsucc n) = f n (nat_primrec n)

In Proofgold the corresponding term root is 797185... and proposition id is fe4c88...

Proof:
Proof not loaded.

End of Section NatRec

Beginning of Section NatArith

L3713

Definition. We define add_nat to be λn m : set ⇒ nat_primrec n (λ_ r ⇒ ordsucc r) m of type set → set → set.

In Proofgold the corresponding term root is afa8ae... and object id is 29768b...

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.

L3717

Theorem. (add_nat_0R)

∀n : set, n + 0 = n

In Proofgold the corresponding term root is 402bcb... and proposition id is 23277f...

Proof:
Proof not loaded.

L3722

Theorem. (add_nat_SR)

∀n m : set, nat_p m → n + ordsucc m = ordsucc (n + m)

In Proofgold the corresponding term root is a53523... and proposition id is e61e18...

Proof:
Proof not loaded.

L3727

Theorem. (add_nat_p)

∀n : set, nat_p n → ∀m : set, nat_p m → nat_p (n + m)

In Proofgold the corresponding term root is a68eaa... and proposition id is 4c1d5d...

Proof:
Proof not loaded.

L3746

Theorem. (add_nat_1_1_2)

1 + 1 = 2

In Proofgold the corresponding term root is 174b87... and proposition id is 77f23f...

Proof:
Proof not loaded.

L3755

Theorem. (add_nat_0L)

∀m : set, nat_p m → 0 + m = m

In Proofgold the corresponding term root is 8ceeb9... and proposition id is 84fbe4...

Proof:
Proof not loaded.

L3769

Theorem. (add_nat_SL)

∀n : set, nat_p n → ∀m : set, nat_p m → ordsucc n + m = ordsucc (n + m)

In Proofgold the corresponding term root is 9c442a... and proposition id is e6efb7...

Proof:
Proof not loaded.

L3788

Theorem. (add_nat_com)

∀n : set, nat_p n → ∀m : set, nat_p m → n + m = m + n

In Proofgold the corresponding term root is 40e952... and proposition id is 4ab179...

Proof:
Proof not loaded.

L3806

Theorem. (nat_Subq_add_ex)

∀n, nat_p n → ∀m, nat_p m → n ⊆ m → ∃k, nat_p k ∧ m = k + n

In Proofgold the corresponding term root is a1e406... and proposition id is 2c7fa4...

Proof:
Proof not loaded.

L3844

Definition. We define mul_nat to be λn m : set ⇒ nat_primrec 0 (λ_ r ⇒ n + r) m of type set → set → set.

In Proofgold the corresponding term root is 35a1ef... and object id is 80ccc6...

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.

L3848

Theorem. (mul_nat_0R)

∀n : set, n * 0 = 0

In Proofgold the corresponding term root is b2f56c... and proposition id is 1e5b2c...

Proof:
Proof not loaded.

L3853

Theorem. (mul_nat_SR)

∀n m : set, nat_p m → n * ordsucc m = n + n * m

In Proofgold the corresponding term root is 37df54... and proposition id is 6dd6fc...

Proof:
Proof not loaded.

L3858

Theorem. (mul_nat_p)

∀n : set, nat_p n → ∀m : set, nat_p m → nat_p (n * m)

In Proofgold the corresponding term root is d63438... and proposition id is e910cb...

Proof:
Proof not loaded.

End of Section NatArith

L3877

Definition. We define Inj1 to be In_rec_i (λX f ⇒ {0} ∪ {f x|x ∈ X}) of type set → set.

In Proofgold the corresponding term root is 8f0026... and object id is 7736ca...

L3880

Theorem. (Inj1_eq)

∀X : set, Inj1 X = {0} ∪ {Inj1 x|x ∈ X}

In Proofgold the corresponding term root is 73d189... and proposition id is b80457...

Proof:
Proof not loaded.

(*** Injection of set into itself that will correspond to x |-> (1,x) after pairing is defined. ***)

L3897

Theorem. (Inj1I1)

∀X : set, 0 ∈ Inj1 X

In Proofgold the corresponding term root is 3c2cc4... and proposition id is 4ccac3...

Proof:
Proof not loaded.

L3905

Theorem. (Inj1I2)

∀X x : set, x ∈ X → Inj1 x ∈ Inj1 X

In Proofgold the corresponding term root is b6f23b... and proposition id is 086475...

Proof:
Proof not loaded.

L3914

Theorem. (Inj1E)

∀X y : set, y ∈ Inj1 X → y = 0 ∨ ∃x ∈ X, y = Inj1 x

In Proofgold the corresponding term root is d4177b... and proposition id is 259217...

Proof:
Proof not loaded.

L3929

Theorem. (Inj1NE1)

∀x : set, Inj1 x ≠ 0

In Proofgold the corresponding term root is 5e3197... and proposition id is 09bd10...

Proof:
Proof not loaded.

L3939

Theorem. (Inj1NE2)

∀x : set, Inj1 x ∉ {0}

In Proofgold the corresponding term root is 9e94b1... and proposition id is 3c4dd0...

Proof:
Proof not loaded.

L3945

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

In Proofgold the corresponding term root is 814321... and object id is 7d54be...

L3948

Theorem. (Inj0I)

∀X x : set, x ∈ X → Inj1 x ∈ Inj0 X

In Proofgold the corresponding term root is 7fc2e9... and proposition id is 565378...

Proof:
Proof not loaded.

(*** Injection of set into itself that will correspond to x |-> (0,x) after pairing is defined. ***)

L3952

Theorem. (Inj0E)

∀X y : set, y ∈ Inj0 X → ∃x : set, x ∈ X ∧ y = Inj1 x

In Proofgold the corresponding term root is 416684... and proposition id is 855213...

Proof:
Proof not loaded.

L3956

Definition. We define Unj to be In_rec_i (λX f ⇒ {f x|x ∈ X ∖ {0}}) of type set → set.

In Proofgold the corresponding term root is f202c1... and object id is 2e1675...

L3959

Theorem. (Unj_eq)

∀X : set, Unj X = {Unj x|x ∈ X ∖ {0}}

In Proofgold the corresponding term root is 3b1aa6... and proposition id is b4c852...

Proof:
Proof not loaded.

(*** Unj : Left inverse of Inj1 and Inj0 ***)

L3976

Theorem. (Unj_Inj1_eq)

∀X : set, Unj (Inj1 X) = X

In Proofgold the corresponding term root is e2cdfc... and proposition id is ae00e1...

Proof:
Proof not loaded.

L4028

Theorem. (Inj1_inj)

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

In Proofgold the corresponding term root is ce8b66... and proposition id is 3e918a...

Proof:
Proof not loaded.

L4038

Theorem. (Unj_Inj0_eq)

∀X : set, Unj (Inj0 X) = X

In Proofgold the corresponding term root is f3e39c... and proposition id is 3808ad...

Proof:
Proof not loaded.

L4086

Theorem. (Inj0_inj)

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

In Proofgold the corresponding term root is 662f53... and proposition id is 29f945...

Proof:
Proof not loaded.

L4096

Theorem. (Inj0_0)

Inj0 0 = 0

In Proofgold the corresponding term root is 171f47... and proposition id is 57f5af...

Proof:
Proof not loaded.

L4100

Theorem. (Inj0_Inj1_neq)

∀X Y : set, Inj0 X ≠ Inj1 Y

In Proofgold the corresponding term root is 21bb03... and proposition id is 2b14d8...

Proof:
Proof not loaded.

L4115

Definition. We define setsum to be λX Y ⇒ {Inj0 x|x ∈ X} ∪ {Inj1 y|y ∈ Y} of type set → set → set.

In Proofgold the corresponding term root is afe37e... and object id is 5b7e09...

Notation. We use + as an infix operator with priority 450 and which associates to the left corresponding to applying term setsum.

(*** setsum ***)

L4121

Theorem. (Inj0_setsum)

∀X Y x : set, x ∈ X → Inj0 x ∈ X + Y

In Proofgold the corresponding term root is 1c6408... and proposition id is 246ac5...

Proof:
Proof not loaded.

L4131

Theorem. (Inj1_setsum)

∀X Y y : set, y ∈ Y → Inj1 y ∈ X + Y

In Proofgold the corresponding term root is d47a0f... and proposition id is 2b4f94...

Proof:
Proof not loaded.

L4141

Theorem. (setsum_Inj_inv)

∀X Y z : set, z ∈ X + Y → (∃x ∈ X, z = Inj0 x) ∨ (∃y ∈ Y, z = Inj1 y)

In Proofgold the corresponding term root is 645a6c... and proposition id is a36400...

Proof:
Proof not loaded.

L4153

Theorem. (Inj0_setsum_0L)

∀X : set, 0 + X = Inj0 X

In Proofgold the corresponding term root is 0be1e7... and proposition id is 36fabd...

Proof:
Proof not loaded.

L4186

Theorem. (Subq_1_Sing0)

1 ⊆ {0}

In Proofgold the corresponding term root is aeae9a... and proposition id is abab2d...

Proof:
Proof not loaded.

L4200

Theorem. (Subq_Sing0_1)

{0} ⊆ 1

In Proofgold the corresponding term root is cd7864... and proposition id is 1806bf...

Proof:
Proof not loaded.

L4204

Theorem. (eq_1_Sing0)

1 = {0}

In Proofgold the corresponding term root is 5e5996... and proposition id is 264f38...

Proof:
Proof not loaded.

L4208

Theorem. (Inj1_setsum_1L)

∀X : set, 1 + X = Inj1 X

In Proofgold the corresponding term root is f8d721... and proposition id is 45b1c8...

Proof:
Proof not loaded.

L4259

Theorem. (nat_setsum1_ordsucc)

∀n : set, nat_p n → 1 + n = ordsucc n

In Proofgold the corresponding term root is 3be3cc... and proposition id is 8fbdda...

Proof:
Proof not loaded.

L4347

Theorem. (setsum_0_0)

0 + 0 = 0

In Proofgold the corresponding term root is 5dcaeb... and proposition id is 4f3651...

Proof:
Proof not loaded.

L4353

Theorem. (setsum_1_0_1)

1 + 0 = 1

In Proofgold the corresponding term root is c2107f... and proposition id is e8609a...

Proof:
Proof not loaded.

L4357

Theorem. (setsum_1_1_2)

1 + 1 = 2

In Proofgold the corresponding term root is 9c89c0... and proposition id is ef3f41...

Proof:
Proof not loaded.

Beginning of Section pair_setsum

L4363

Let pair ≝ setsum

L4365

Definition. We define proj0 to be λZ ⇒ {Unj z|z ∈ Z, ∃x : set, Inj0 x = z} of type set → set.

In Proofgold the corresponding term root is 21a488... and object id is 9c5e4e...

L4367

Definition. We define proj1 to be λZ ⇒ {Unj z|z ∈ Z, ∃y : set, Inj1 y = z} of type set → set.

In Proofgold the corresponding term root is 7aba21... and object id is 7fd81e...

L4368

Theorem. (Inj0_pair_0_eq)

Inj0 = pair 0

In Proofgold the corresponding term root is 0fe601... and proposition id is 490c2a...

Proof:
Proof not loaded.

L4376

Theorem. (Inj1_pair_1_eq)

Inj1 = pair 1

In Proofgold the corresponding term root is 0bbde8... and proposition id is 8272d7...

Proof:
Proof not loaded.

L4384

Theorem. (pairI0)

∀X Y x, x ∈ X → pair 0 x ∈ pair X Y

In Proofgold the corresponding term root is 21a414... and proposition id is 34813b...

Proof:
Proof not loaded.

L4389

Theorem. (pairI1)

∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y

In Proofgold the corresponding term root is bdaab5... and proposition id is b5248b...

Proof:
Proof not loaded.

L4394

Theorem. (pairE)

∀X Y z, z ∈ pair X Y → (∃x ∈ X, z = pair 0 x) ∨ (∃y ∈ Y, z = pair 1 y)

In Proofgold the corresponding term root is aac610... and proposition id is 0afdeb...

Proof:
Proof not loaded.

L4400

Theorem. (pairE0)

∀X Y x, pair 0 x ∈ pair X Y → x ∈ X

In Proofgold the corresponding term root is 042f30... and proposition id is f50b25...

Proof:
Proof not loaded.

L4426

Theorem. (pairE1)

∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y

In Proofgold the corresponding term root is 505cfc... and proposition id is 30a181...

Proof:
Proof not loaded.

L4454

Theorem. (proj0I)

∀w u : set, pair 0 u ∈ w → u ∈ proj0 w

In Proofgold the corresponding term root is be55b9... and proposition id is 840c8d...

Proof:
Proof not loaded.

L4469

Theorem. (proj0E)

∀w u : set, u ∈ proj0 w → pair 0 u ∈ w

In Proofgold the corresponding term root is b9afa9... and proposition id is 5b7f58...

Proof:
Proof not loaded.

L4493

Theorem. (proj1I)

∀w u : set, pair 1 u ∈ w → u ∈ proj1 w

In Proofgold the corresponding term root is fbddb7... and proposition id is 595b3c...

Proof:
Proof not loaded.

L4508

Theorem. (proj1E)

∀w u : set, u ∈ proj1 w → pair 1 u ∈ w

In Proofgold the corresponding term root is 06e32e... and proposition id is c3c3e6...

Proof:
Proof not loaded.

L4532

Theorem. (proj0_pair_eq)

∀X Y : set, proj0 (pair X Y) = X

In Proofgold the corresponding term root is d546f3... and proposition id is 0c12fb...

Proof:
Proof not loaded.

L4552

Theorem. (proj1_pair_eq)

∀X Y : set, proj1 (pair X Y) = Y

In Proofgold the corresponding term root is 9f98a8... and proposition id is e0cb0f...

Proof:
Proof not loaded.

L4572

Definition. We define Sigma to be λX Y ⇒ ⋃_{x ∈ X}{pair x y|y ∈ Y x} of type set → (set → set) → set.

In Proofgold the corresponding term root is 8acbb2... and object id is d64bcb...

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

(*** Sigma X Y = {(x,y) | x in X, y in Y x} ***)

L4580

Theorem. (pair_Sigma)

∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, pair x y ∈ ∑x ∈ X, Y x

In Proofgold the corresponding term root is 0d8645... and proposition id is 1456cb...

Proof:
Proof not loaded.

L4595

Theorem. (Sigma_eta_proj0_proj1)

∀X : set, ∀Y : set → set, ∀z ∈ (∑x ∈ X, Y x), pair (proj0 z) (proj1 z) = z ∧ proj0 z ∈ X ∧ proj1 z ∈ Y (proj0 z)

In Proofgold the corresponding term root is afe962... and proposition id is 77ba8e...

Proof:
Proof not loaded.

L4623

Theorem. (proj_Sigma_eta)

∀X : set, ∀Y : set → set, ∀z ∈ (∑x ∈ X, Y x), pair (proj0 z) (proj1 z) = z

In Proofgold the corresponding term root is 8b31cd... and proposition id is f30f76...

Proof:
Proof not loaded.

L4631

Theorem. (proj0_Sigma)

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → proj0 z ∈ X

In Proofgold the corresponding term root is ae12a7... and proposition id is 506869...

Proof:
Proof not loaded.

L4639

Theorem. (proj1_Sigma)

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → proj1 z ∈ Y (proj0 z)

In Proofgold the corresponding term root is 553db6... and proposition id is d79917...

Proof:
Proof not loaded.

L4647

Theorem. (pair_Sigma_E1)

∀X : set, ∀Y : set → set, ∀x y : set, pair x y ∈ (∑x ∈ X, Y x) → y ∈ Y x

In Proofgold the corresponding term root is c294a7... and proposition id is 81d8b0...

Proof:
Proof not loaded.

L4658

Theorem. (Sigma_E)

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → ∃x ∈ X, ∃y ∈ Y x, z = pair x y

In Proofgold the corresponding term root is 5b1bd2... and proposition id is 8ecfab...

Proof:
Proof not loaded.

L4676

Definition. We define setprod to be λX Y : set ⇒ ∑x ∈ X, Y of type set → set → set.

In Proofgold the corresponding term root is fc0b60... and object id is 107b6b...

Notation. We use ⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.

L4681

Let lam : set → (set → set) → set ≝ Sigma

L4684

Definition. We define ap to be λf x ⇒ {proj1 z|z ∈ f, ∃y : set, z = pair x y} of type set → set → set.

In Proofgold the corresponding term root is c7aaa6... and object id is a4d82c...

(*** lam X F = {(x,y) | x :e X, y :e F x} = \/_{x :e X} {(x,y) | y :e (F x)} = Sigma X F ***)

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).

Notation. We now use n-tuple notation (a₀,...,a_n-1) for n ≥ 2 for λ i ∈ n . if i = 0 then a₀ else ... if i = n-2 then a_n-2 else a_n-1.

(*** ap f x = {proj1 z | z :e f, exists y, z = pair x y}} ***)

L4690

Theorem. (lamI)

∀X : set, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, pair x y ∈ λx ∈ X ⇒ F x

In Proofgold the corresponding term root is 0d8645... and proposition id is 1456cb...

Proof:
Proof not loaded.

L4694

Theorem. (lamE)

∀X : set, ∀F : set → set, ∀z : set, z ∈ (λx ∈ X ⇒ F x) → ∃x ∈ X, ∃y ∈ F x, z = pair x y

In Proofgold the corresponding term root is 5b1bd2... and proposition id is 8ecfab...

Proof:
Proof not loaded.

L4698

Theorem. (apI)

∀f x y, pair x y ∈ f → y ∈ f x

In Proofgold the corresponding term root is 64667c... and proposition id is 770816...

Proof:
Proof not loaded.

L4710

Theorem. (apE)

∀f x y, y ∈ f x → pair x y ∈ f

In Proofgold the corresponding term root is 85693a... and proposition id is c08565...

Proof:
Proof not loaded.

L4738

Theorem. (beta)

∀X : set, ∀F : set → set, ∀x : set, x ∈ X → (λx ∈ X ⇒ F x) x = F x

In Proofgold the corresponding term root is 95991d... and proposition id is b5182d...

Proof:
Proof not loaded.

L4758

Theorem. (proj0_ap_0)

∀u, proj0 u = u 0

In Proofgold the corresponding term root is 588f37... and proposition id is d4f351...

Proof:
Proof not loaded.

L4778

Theorem. (proj1_ap_1)

∀u, proj1 u = u 1

In Proofgold the corresponding term root is d116b3... and proposition id is 2328b0...

Proof:
Proof not loaded.

L4798

Theorem. (pair_ap_0)

∀x y : set, (pair x y) 0 = x

In Proofgold the corresponding term root is ac34b9... and proposition id is bb0477...

Proof:
Proof not loaded.

L4805

Theorem. (pair_ap_1)

∀x y : set, (pair x y) 1 = y

In Proofgold the corresponding term root is 2274fc... and proposition id is cce3d2...

Proof:
Proof not loaded.

L4812

Theorem. (ap0_Sigma)

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 0) ∈ X

In Proofgold the corresponding term root is 861a79... and proposition id is 1affcc...

Proof:
Proof not loaded.

L4818

Theorem. (ap1_Sigma)

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 1) ∈ (Y (z 0))

In Proofgold the corresponding term root is ad3bfe... and proposition id is 520af5...

Proof:
Proof not loaded.

L4825

Definition. We define pair_p to be λu : set ⇒ pair (u 0) (u 1) = u of type set → prop.

In Proofgold the corresponding term root is ade2bb... and object id is 5c8a35...

L4828

Theorem. (pair_p_I)

∀x y, pair_p (pair x y)

In Proofgold the corresponding term root is 06d9a2... and proposition id is 8f2fde...

Proof:
Proof not loaded.

L4836

Theorem. (Subq_2_UPair01)

2 ⊆ {0,1}

In Proofgold the corresponding term root is d90884... and proposition id is 94203e...

Proof:
Proof not loaded.

L4854

Theorem. (tuple_pair)

∀x y : set, pair x y = (x,y)

In Proofgold the corresponding term root is c122f6... and proposition id is 18198e...

Proof:
Proof not loaded.

L4929

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.

In Proofgold the corresponding term root is 40f1c3... and object id is a7b1b0...

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

L4934

Theorem. (PiI)

∀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

In Proofgold the corresponding term root is 2b7ef4... and proposition id is 1f8f6f...

Proof:
Proof not loaded.

L4968

Theorem. (lam_Pi)

∀X : set, ∀Y : set → set, ∀F : set → set, (∀x ∈ X, F x ∈ Y x) → (λx ∈ X ⇒ F x) ∈ (∏x ∈ X, Y x)

In Proofgold the corresponding term root is c0b88f... and proposition id is 3733f8...

Proof:
Proof not loaded.

L5007

Theorem. (ap_Pi)

∀X : set, ∀Y : set → set, ∀f : set, ∀x : set, f ∈ (∏x ∈ X, Y x) → x ∈ X → f x ∈ Y x

In Proofgold the corresponding term root is 7c3617... and proposition id is cb962e...

Proof:
Proof not loaded.

L5013

Definition. We define setexp to be λX Y : set ⇒ ∏y ∈ Y, X of type set → set → set.

In Proofgold the corresponding term root is 1de7fc... and object id is 021ae0...

Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.

L5018

Theorem. (pair_tuple_fun)

pair = (λx y ⇒ (x,y))

In Proofgold the corresponding term root is b02dfa... and proposition id is ed37d0...

Proof:
Proof not loaded.

L5025

Theorem. (lamI2)

∀X, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, (x,y) ∈ λx ∈ X ⇒ F x

In Proofgold the corresponding term root is d4a9d9... and proposition id is de381f...

Proof:
Proof not loaded.

Beginning of Section Tuples

L5033

Variable x0 x1 : set

L5035

Theorem. (tuple_2_0_eq)

(x0,x1) 0 = x0

In Proofgold the corresponding term root is 42d452... and proposition id is ad9037...

Proof:
Proof not loaded.

L5040

Theorem. (tuple_2_1_eq)

(x0,x1) 1 = x1

In Proofgold the corresponding term root is 596569... and proposition id is 2c0ad1...

Proof:
Proof not loaded.

End of Section Tuples

L5047

Theorem. (ReplEq_setprod_ext)

∀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}

In Proofgold the corresponding term root is c486ab... and proposition id is f689a0...

Proof:
Proof not loaded.

L5058

Theorem. (tuple_2_Sigma)

∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, (x,y) ∈ ∑x ∈ X, Y x

In Proofgold the corresponding term root is d4a9d9... and proposition id is de381f...

Proof:
Proof not loaded.

L5062

Theorem. (tuple_2_setprod)

∀X : set, ∀Y : set, ∀x ∈ X, ∀y ∈ Y, (x,y) ∈ X ⨯ Y

In Proofgold the corresponding term root is e907b8... and proposition id is 1f9d7f...

Proof:
Proof not loaded.

End of Section pair_setsum