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.
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.
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.
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
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
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.
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.
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...
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.
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.
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.
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).
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...
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...
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...
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...
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...
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.
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...
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...
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...
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...
Axiom. (andI) We take the following as an axiom:
∀A B : prop, A → B → A ∧ B
In Proofgold the corresponding term root is 3c4f59... and proposition id is 3bf198...
Axiom. (orIL) We take the following as an axiom:
∀A B : prop, A → A ∨ B
In Proofgold the corresponding term root is 55be8c... and proposition id is 382673...
Axiom. (orIR) We take the following as an axiom:
∀A B : prop, B → A ∨ B
In Proofgold the corresponding term root is 3c63fc... and proposition id is 8d8e40...
Axiom. (iffI) We take the following as an axiom:
∀A B : prop, (A → B) → (B → A) → (A ↔ B)
In Proofgold the corresponding term root is 7516b9... and proposition id is 4d966a...
Axiom. (pred_ext) We take the following as an axiom:
∀P Q : set → prop, (∀x, P x ↔ Q x) → P = Q
In Proofgold the corresponding term root is e9e64b... and proposition id is d4b2d3...
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.
Axiom. (EmptyE) We take the following as an axiom:
∀x : set, x ∉ Empty
In Proofgold the corresponding term root is 93a77a... and proposition id is 8349ab...
Axiom. (PowerI) We take the following as an axiom:
∀X Y : set, Y ⊆ X → Y ∈ 𝒫 X
In Proofgold the corresponding term root is 7143d7... and proposition id is 3c48d3...
Axiom. (Subq_Empty) We take the following as an axiom:
∀X : set, Empty ⊆ X
In Proofgold the corresponding term root is a517cd... and proposition id is 2faec3...
Axiom. (Empty_In_Power) We take the following as an axiom:
∀X : set, Empty ∈ 𝒫 X
In Proofgold the corresponding term root is d2656b... and proposition id is 487855...
Axiom. (xm) We take the following as an axiom:
∀P : prop, P ∨ ¬ P
In Proofgold the corresponding term root is 62e4c3... and proposition id is 7b6737...
Axiom. (FalseE) We take the following as an axiom:
False → ∀p : prop, p
In Proofgold the corresponding term root is 0dcfe3... and proposition id is f9a230...
Axiom. (andEL) We take the following as an axiom:
∀A B : prop, A ∧ B → A
In Proofgold the corresponding term root is c2f006... and proposition id is 718be4...
Axiom. (andER) We take the following as an axiom:
∀A B : prop, A ∧ B → B
In Proofgold the corresponding term root is f66b82... and proposition id is 5caea9...
Beginning of Section PropN
Variable P1 P2 P3 : prop
Axiom. (and3I) We take the following as an axiom:
P1 → P2 → P3 → P1 ∧ P2 ∧ P3
In Proofgold the corresponding term root is 23ac9c... and proposition id is cb999b...
Axiom. (and3E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 → (∀p : prop, (P1 → P2 → P3 → p) → p)
In Proofgold the corresponding term root is 445f76... and proposition id is 50fabe...
Axiom. (or3I1) We take the following as an axiom:
P1 → P1 ∨ P2 ∨ P3
In Proofgold the corresponding term root is e44f34... and proposition id is ef9071...
Axiom. (or3I2) We take the following as an axiom:
P2 → P1 ∨ P2 ∨ P3
In Proofgold the corresponding term root is 8df6e1... and proposition id is 827a91...
Axiom. (or3I3) We take the following as an axiom:
P3 → P1 ∨ P2 ∨ P3
In Proofgold the corresponding term root is 017a00... and proposition id is 3b7f5a...
Axiom. (or3E) We take the following as an axiom:
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...
Variable P4 : prop
Axiom. (and4I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4
In Proofgold the corresponding term root is ed32cb... and proposition id is 906aaf...
Variable P5 : prop
Axiom. (and5I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5
In Proofgold the corresponding term root is 041ced... and proposition id is 11fc47...
Variable P6 : prop
Axiom. (and6I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P6 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6
In Proofgold the corresponding term root is 9817c7... and proposition id is a5dc29...
Variable P7 : prop
Axiom. (and7I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P6 → P7 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7
In Proofgold the corresponding term root is 6a4d8c... and proposition id is c89388...
End of Section PropN
Axiom. (not_or_and_demorgan) We take the following as an axiom:
∀A B : prop, ¬ (A ∨ B) → ¬ A ∧ ¬ B
In Proofgold the corresponding term root is 8733b0... and proposition id is 27db91...
Axiom. (not_ex_all_demorgan_i) We take the following as an axiom:
∀P : set → prop, (¬ ∃x, P x) → ∀x, ¬ P x
In Proofgold the corresponding term root is 73523e... and proposition id is 075ddf...
Axiom. (iffEL) We take the following as an axiom:
∀A B : prop, (A ↔ B) → A → B
In Proofgold the corresponding term root is 0e94c6... and proposition id is 9a07f6...
Axiom. (iffER) We take the following as an axiom:
∀A B : prop, (A ↔ B) → B → A
In Proofgold the corresponding term root is 54702a... and proposition id is f5dfc0...
Axiom. (iff_refl) We take the following as an axiom:
∀A : prop, A ↔ A
In Proofgold the corresponding term root is 01338d... and proposition id is 7b71b5...
Axiom. (iff_sym) We take the following as an axiom:
∀A B : prop, (A ↔ B) → (B ↔ A)
In Proofgold the corresponding term root is 00bac1... and proposition id is 11f51b...
Axiom. (iff_trans) We take the following as an axiom:
∀A B C : prop, (A ↔ B) → (B ↔ C) → (A ↔ C)
In Proofgold the corresponding term root is 363285... and proposition id is c3b8f1...
Axiom. (eq_i_tra) We take the following as an axiom:
∀x y z, x = y → y = z → x = z
In Proofgold the corresponding term root is 193bbf... and proposition id is 7ecbc4...
Axiom. (neq_i_sym) We take the following as an axiom:
∀x y, x ≠ y → y ≠ x
In Proofgold the corresponding term root is 5c0ec9... and proposition id is 1a9898...
Axiom. (Eps_i_ex) We take the following as an axiom:
∀P : set → prop, (∃x, P x) → P (Eps_i P)
In Proofgold the corresponding term root is be36f0... and proposition id is 6a2832...
Axiom. (prop_ext_2) We take the following as an axiom:
∀p q : prop, (p → q) → (q → p) → p = q
In Proofgold the corresponding term root is a9ede2... and proposition id is a56fc7...
Axiom. (Subq_ref) We take the following as an axiom:
∀X : set, X ⊆ X
In Proofgold the corresponding term root is 4c5395... and proposition id is 2efbac...
Axiom. (Subq_tra) We take the following as an axiom:
∀X Y Z : set, X ⊆ Y → Y ⊆ Z → X ⊆ Z
In Proofgold the corresponding term root is 79accb... and proposition id is fed662...
Axiom. (Empty_Subq_eq) We take the following as an axiom:
∀X : set, X ⊆ Empty → X = Empty
In Proofgold the corresponding term root is 2dd959... and proposition id is 988691...
Axiom. (Empty_eq) We take the following as an axiom:
∀X : set, (∀x, x ∉ X) → X = Empty
In Proofgold the corresponding term root is 3de0fd... and proposition id is 8b915b...
Axiom. (UnionI) We take the following as an axiom:
∀X x Y : set, x ∈ Y → Y ∈ X → x ∈ ⋃ X
In Proofgold the corresponding term root is 51b549... and proposition id is bade05...
Axiom. (UnionE) We take the following as an axiom:
∀X x : set, x ∈ ⋃ X → ∃Y : set, x ∈ Y ∧ Y ∈ X
In Proofgold the corresponding term root is db4bc1... and proposition id is ab781b...
Axiom. (UnionE_impred) We take the following as an axiom:
∀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...
Axiom. (PowerE) We take the following as an axiom:
∀X Y : set, Y ∈ 𝒫 X → Y ⊆ X
In Proofgold the corresponding term root is 149030... and proposition id is 647070...
Axiom. (Self_In_Power) We take the following as an axiom:
∀X : set, X ∈ 𝒫 X
In Proofgold the corresponding term root is f81ef2... and proposition id is 8336ff...
Axiom. (dneg) We take the following as an axiom:
∀P : prop, ¬ ¬ P → P
In Proofgold the corresponding term root is 852f34... and proposition id is b7cc63...
Axiom. (not_all_ex_demorgan_i) We take the following as an axiom:
∀P : set → prop, ¬ (∀x, P x) → ∃x, ¬ P x
In Proofgold the corresponding term root is 9bfa06... and proposition id is 4b1474...
Axiom. (eq_or_nand) We take the following as an axiom:
or = (λx y : prop ⇒ ¬ (¬ x ∧ ¬ y))
In Proofgold the corresponding term root is 24ac29... and proposition id is d212ef...
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...
Axiom. (exactly1of2_I1) We take the following as an axiom:
∀A B : prop, A → ¬ B → exactly1of2 A B
In Proofgold the corresponding term root is 8e1e45... and proposition id is 4f94fa...
Axiom. (exactly1of2_I2) We take the following as an axiom:
∀A B : prop, ¬ A → B → exactly1of2 A B
In Proofgold the corresponding term root is c9fd90... and proposition id is 6c1ad9...
Axiom. (exactly1of2_E) We take the following as an axiom:
∀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...
Axiom. (exactly1of2_or) We take the following as an axiom:
∀A B : prop, exactly1of2 A B → A ∨ B
In Proofgold the corresponding term root is 18af73... and proposition id is e092f6...
Axiom. (ReplI) We take the following as an axiom:
∀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...
Axiom. (ReplE) 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 311cdf... and proposition id is d07e78...
Axiom. (ReplE_impred) We take the following as an axiom:
∀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...
Axiom. (ReplE') We take the following as an axiom:
∀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...
Axiom. (Repl_Empty) We take the following as an axiom:
∀F : set → set, {F x|x ∈ Empty} = Empty
In Proofgold the corresponding term root is 2af2ac... and proposition id is 0835bc...
Axiom. (ReplEq_ext_sub) We take the following as an axiom:
∀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...
Axiom. (ReplEq_ext) We take the following as an axiom:
∀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...
Axiom. (Repl_inv_eq) We take the following as an axiom:
∀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...
Axiom. (Repl_invol_eq) We take the following as an axiom:
∀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...
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.
Axiom. (If_i_correct) We take the following as an axiom:
∀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...
Axiom. (If_i_0) We take the following as an axiom:
∀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...
Axiom. (If_i_1) We take the following as an axiom:
∀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...
Axiom. (If_i_or) We take the following as an axiom:
∀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...
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.
Axiom. (UPairE) We take the following as an axiom:
∀x y z : set, x ∈ {y,z} → x = y ∨ x = z
In Proofgold the corresponding term root is 5009cc... and proposition id is e67fc5...
Axiom. (UPairI1) We take the following as an axiom:
∀y z : set, y ∈ {y,z}
In Proofgold the corresponding term root is b1eea2... and proposition id is bf3649...
Axiom. (UPairI2) We take the following as an axiom:
∀y z : set, z ∈ {y,z}
In Proofgold the corresponding term root is 27455b... and proposition id is a0a5b8...
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.
Axiom. (SingI) We take the following as an axiom:
∀x : set, x ∈ {x}
In Proofgold the corresponding term root is 6591bd... and proposition id is 2f93be...
Axiom. (SingE) We take the following as an axiom:
∀x y : set, y ∈ {x} → y = x
In Proofgold the corresponding term root is 9341fe... and proposition id is 3b0dd8...
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.
Axiom. (binunionI1) We take the following as an axiom:
∀X Y z : set, z ∈ X → z ∈ X ∪ Y
In Proofgold the corresponding term root is 753b6e... and proposition id is e43c8d...
Axiom. (binunionI2) We take the following as an axiom:
∀X Y z : set, z ∈ Y → z ∈ X ∪ Y
In Proofgold the corresponding term root is b8821c... and proposition id is 959535...
Axiom. (binunionE) We take the following as an axiom:
∀X Y z : set, z ∈ X ∪ Y → z ∈ X ∨ z ∈ Y
In Proofgold the corresponding term root is 5a3195... and proposition id is 1ceeb0...
Axiom. (binunionE') We take the following as an axiom:
∀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...
Axiom. (binunion_asso) We take the following as an axiom:
∀X Y Z : set, X ∪ (Y ∪ Z) = (X ∪ Y) ∪ Z
In Proofgold the corresponding term root is e0f701... and proposition id is 61dfba...
Axiom. (binunion_com_Subq) We take the following as an axiom:
∀X Y : set, X ∪ Y ⊆ Y ∪ X
In Proofgold the corresponding term root is ee8f5a... and proposition id is d84076...
Axiom. (binunion_com) We take the following as an axiom:
∀X Y : set, X ∪ Y = Y ∪ X
In Proofgold the corresponding term root is e20f4f... and proposition id is bed33e...
Axiom. (binunion_idl) We take the following as an axiom:
∀X : set, Empty ∪ X = X
In Proofgold the corresponding term root is 8dc616... and proposition id is 52cd24...
Axiom. (binunion_idr) We take the following as an axiom:
∀X : set, X ∪ Empty = X
In Proofgold the corresponding term root is 67e82f... and proposition id is d5a005...
Axiom. (binunion_Subq_1) We take the following as an axiom:
∀X Y : set, X ⊆ X ∪ Y
In Proofgold the corresponding term root is b2c658... and proposition id is a9b3a8...
Axiom. (binunion_Subq_2) We take the following as an axiom:
∀X Y : set, Y ⊆ X ∪ Y
In Proofgold the corresponding term root is 3cf229... and proposition id is 1507ce...
Axiom. (binunion_Subq_min) We take the following as an axiom:
∀X Y Z : set, X ⊆ Z → Y ⊆ Z → X ∪ Y ⊆ Z
In Proofgold the corresponding term root is cc32a5... and proposition id is d64da4...
Axiom. (Subq_binunion_eq) We take the following as an axiom:
∀X Y, (X ⊆ Y) = (X ∪ Y = Y)
In Proofgold the corresponding term root is f8ee53... and proposition id is c2d393...
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.
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.
Axiom. (famunionI) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀x y : set, x ∈ X → y ∈ F x → y ∈ ⋃x ∈ XF x
In Proofgold the corresponding term root is 0c23d0... and proposition id is e4f490...
Axiom. (famunionE) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃x ∈ XF x) → ∃x ∈ X, y ∈ F x
In Proofgold the corresponding term root is 48683a... and proposition id is ede6e5...
Axiom. (famunionE_impred) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃x ∈ XF x) → ∀p : prop, (∀x, x ∈ X → y ∈ F x → p) → p
In Proofgold the corresponding term root is ab2266... and proposition id is 562023...
Axiom. (famunion_Empty) We take the following as an axiom:
∀F : set → set, (⋃x ∈ EmptyF x) = Empty
In Proofgold the corresponding term root is fc1bdd... and proposition id is 22bd10...
Axiom. (famunion_Subq) We take the following as an axiom:
∀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...
Axiom. (famunion_ext) We take the following as an axiom:
∀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...
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.
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).
Axiom. (SepI) We take the following as an axiom:
∀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...
Axiom. (SepE) We take the following as an axiom:
∀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...
Axiom. (SepE1) We take the following as an axiom:
∀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...
Axiom. (SepE2) We take the following as an axiom:
∀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...
Axiom. (Sep_Empty) We take the following as an axiom:
∀P : set → prop, {x ∈ Empty|P x} = Empty
In Proofgold the corresponding term root is f36949... and proposition id is e3473a...
Axiom. (Sep_Subq) We take the following as an axiom:
∀X : set, ∀P : set → prop, {x ∈ X|P x} ⊆ X
In Proofgold the corresponding term root is 97d080... and proposition id is c17d45...
Axiom. (Sep_In_Power) We take the following as an axiom:
∀X : set, ∀P : set → prop, {x ∈ X|P x} ∈ 𝒫 X
In Proofgold the corresponding term root is 612c94... and proposition id is fba53e...
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).
Axiom. (ReplSepI) We take the following as an axiom:
∀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...
Axiom. (ReplSepE) We take the following as an axiom:
∀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...
Axiom. (ReplSepE_impred) We take the following as an axiom:
∀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...
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.
Axiom. (binintersectI) We take the following as an axiom:
∀X Y z, z ∈ X → z ∈ Y → z ∈ X ∩ Y
In Proofgold the corresponding term root is fd656d... and proposition id is 9081a0...
Axiom. (binintersectE) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ X ∧ z ∈ Y
In Proofgold the corresponding term root is 463b5a... and proposition id is ca0636...
Axiom. (binintersectE1) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ X
In Proofgold the corresponding term root is b12123... and proposition id is 51005e...
Axiom. (binintersectE2) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ Y
In Proofgold the corresponding term root is 39656f... and proposition id is 599de4...
Axiom. (binintersect_Subq_1) We take the following as an axiom:
∀X Y : set, X ∩ Y ⊆ X
In Proofgold the corresponding term root is f296ad... and proposition id is 303833...
Axiom. (binintersect_Subq_2) We take the following as an axiom:
∀X Y : set, X ∩ Y ⊆ Y
In Proofgold the corresponding term root is fcd5f5... and proposition id is 8b9fd2...
Axiom. (binintersect_Subq_eq_1) We take the following as an axiom:
∀X Y, X ⊆ Y → X ∩ Y = X
In Proofgold the corresponding term root is 277eec... and proposition id is ec1cc3...
Axiom. (binintersect_Subq_max) We take the following as an axiom:
∀X Y Z : set, Z ⊆ X → Z ⊆ Y → Z ⊆ X ∩ Y
In Proofgold the corresponding term root is 95624d... and proposition id is 64636b...
Axiom. (binintersect_com_Subq) We take the following as an axiom:
∀X Y : set, X ∩ Y ⊆ Y ∩ X
In Proofgold the corresponding term root is 410255... and proposition id is 5977b8...
Axiom. (binintersect_com) We take the following as an axiom:
∀X Y : set, X ∩ Y = Y ∩ X
In Proofgold the corresponding term root is 1a2c6f... and proposition id is ea8a1c...
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.
Axiom. (setminusI) We take the following as an axiom:
∀X Y z, (z ∈ X) → (z ∉ Y) → z ∈ X ∖ Y
In Proofgold the corresponding term root is 0feeb8... and proposition id is 80db6a...
Axiom. (setminusE) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y) → z ∈ X ∧ z ∉ Y
In Proofgold the corresponding term root is 6774f4... and proposition id is 71763a...
Axiom. (setminusE1) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y) → z ∈ X
In Proofgold the corresponding term root is 064bd5... and proposition id is d74baf...
Axiom. (setminusE2) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y) → z ∉ Y
In Proofgold the corresponding term root is 3e6969... and proposition id is 36b273...
Axiom. (setminus_Subq) We take the following as an axiom:
∀X Y : set, X ∖ Y ⊆ X
In Proofgold the corresponding term root is 5a497a... and proposition id is 66f982...
Axiom. (setminus_In_Power) We take the following as an axiom:
∀A U, A ∖ U ∈ 𝒫 A
In Proofgold the corresponding term root is 062275... and proposition id is f503e1...
Axiom. (binunion_remove1_eq) We take the following as an axiom:
∀X, ∀x ∈ X, X = (X ∖ {x}) ∪ {x}
In Proofgold the corresponding term root is 20fce6... and proposition id is eb0c40...
Axiom. (In_irref) We take the following as an axiom:
∀x, x ∉ x
In Proofgold the corresponding term root is 12629a... and proposition id is 7bfd46...
Axiom. (In_no2cycle) We take the following as an axiom:
∀x y, x ∈ y → y ∈ x → False
In Proofgold the corresponding term root is 6d0cb3... and proposition id is 344f30...
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...
Axiom. (ordsuccI1) We take the following as an axiom:
∀x : set, x ⊆ ordsucc x
In Proofgold the corresponding term root is 5a2f15... and proposition id is 367d80...
Axiom. (ordsuccI2) We take the following as an axiom:
∀x : set, x ∈ ordsucc x
In Proofgold the corresponding term root is 2f6efd... and proposition id is 2be6be...
Axiom. (ordsuccE) We take the following as an axiom:
∀x y : set, y ∈ ordsucc x → y ∈ x ∨ y = x
In Proofgold the corresponding term root is 01c4ee... and proposition id is 3849f5...
Notation. Natural numbers 0,1,2,... are notation for the terms formed using Empty as 0 and forming successors with ordsucc.
Axiom. (neq_0_ordsucc) We take the following as an axiom:
∀a : set, 0 ≠ ordsucc a
In Proofgold the corresponding term root is 1b20cb... and proposition id is 04c410...
Axiom. (neq_ordsucc_0) We take the following as an axiom:
∀a : set, ordsucc a ≠ 0
In Proofgold the corresponding term root is 9b391e... and proposition id is 346ee0...
Axiom. (ordsucc_inj) We take the following as an axiom:
∀a b : set, ordsucc a = ordsucc b → a = b
In Proofgold the corresponding term root is 40cad6... and proposition id is 4869a1...
Axiom. (In_0_1) We take the following as an axiom:
0 ∈ 1
In Proofgold the corresponding term root is e984b0... and proposition id is 3be80a...
Axiom. (In_0_2) We take the following as an axiom:
0 ∈ 2
In Proofgold the corresponding term root is 56dc2c... and proposition id is 5a202e...
Axiom. (In_1_2) We take the following as an axiom:
1 ∈ 2
In Proofgold the corresponding term root is 8704b3... and proposition id is 431e9e...
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...
Axiom. (nat_0) We take the following as an axiom:
nat_p 0
In Proofgold the corresponding term root is 1617bc... and proposition id is 457a72...
Axiom. (nat_ordsucc) We take the following as an axiom:
∀n : set, nat_p n → nat_p (ordsucc n)
In Proofgold the corresponding term root is 87f001... and proposition id is 57e940...
Axiom. (nat_1) We take the following as an axiom:
nat_p 1
In Proofgold the corresponding term root is 2f83fa... and proposition id is 672d0d...
Axiom. (nat_2) We take the following as an axiom:
nat_p 2
In Proofgold the corresponding term root is a8be15... and proposition id is 9112e9...
Axiom. (nat_0_in_ordsucc) We take the following as an axiom:
∀n, nat_p n → 0 ∈ ordsucc n
In Proofgold the corresponding term root is 9b50b9... and proposition id is 251f3d...
Axiom. (nat_ordsucc_in_ordsucc) We take the following as an axiom:
∀n, nat_p n → ∀m ∈ n, ordsucc m ∈ ordsucc n
In Proofgold the corresponding term root is 819399... and proposition id is 4c2c95...
Axiom. (nat_ind) We take the following as an axiom:
∀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...
Axiom. (nat_complete_ind) We take the following as an axiom:
∀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...
Axiom. (nat_inv_impred) We take the following as an axiom:
∀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...
Axiom. (nat_inv) We take the following as an axiom:
∀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...
Axiom. (nat_p_trans) We take the following as an axiom:
∀n, nat_p n → ∀m ∈ n, nat_p m
In Proofgold the corresponding term root is e88449... and proposition id is 03b874...
Axiom. (nat_trans) We take the following as an axiom:
∀n, nat_p n → ∀m ∈ n, m ⊆ n
In Proofgold the corresponding term root is 6bc6e1... and proposition id is cad6fe...
Axiom. (nat_ordsucc_trans) We take the following as an axiom:
∀n, nat_p n → ∀m ∈ ordsucc n, m ⊆ n
In Proofgold the corresponding term root is e42e58... and proposition id is bc868d...
Definition. We define surj to be λX Y f ⇒ (∀u ∈ X, f u ∈ Y) ∧ (∀w ∈ Y, ∃u ∈ X, f u = w) of type set → set → (set → set) → prop.
In Proofgold the corresponding term root is 4b68e4... and object id is f022f9...
Axiom. (form100_63_surjCantor) We take the following as an axiom:
∀A : set, ∀f : set → set, ¬ surj A (𝒫 A) f
In Proofgold the corresponding term root is eb4dfa... and proposition id is feecd4...
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...
Axiom. (form100_63_injCantor) We take the following as an axiom:
∀A : set, ∀f : set → set, ¬ inj (𝒫 A) A f
In Proofgold the corresponding term root is 4f3dc8... and proposition id is 2f2854...
Axiom. (injI) We take the following as an axiom:
∀X Y, ∀f : set → set, (∀x ∈ X, f x ∈ Y) → (∀x z ∈ X, f x = f z → x = z) → inj X Y f
In Proofgold the corresponding term root is 8739d9... and proposition id is 71c936...
Axiom. (inj_comp) We take the following as an axiom:
∀X Y Z : set, ∀f g : set → set, inj X Y f → inj Y Z g → inj X Z (λx ⇒ g (f x))
In Proofgold the corresponding term root is 649bd9... and proposition id is 05a66c...
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...
Axiom. (bijI) We take the following as an axiom:
∀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...
Axiom. (bijE) We take the following as an axiom:
∀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...
Axiom. (bij_inj) We take the following as an axiom:
∀X Y, ∀f : set → set, bij X Y f → inj X Y f
In Proofgold the corresponding term root is e3635e... and proposition id is 00097c...
Axiom. (bij_id) We take the following as an axiom:
∀X, bij X X (λx ⇒ x)
In Proofgold the corresponding term root is a8cefb... and proposition id is 707f37...
Axiom. (bij_comp) We take the following as an axiom:
∀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...
Axiom. (bij_surj) We take the following as an axiom:
∀X Y, ∀f : set → set, bij X Y f → surj X Y f
In Proofgold the corresponding term root is e7a049... and proposition id is 7fa9a5...
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...
Axiom. (surj_rinv) We take the following as an axiom:
∀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...
Axiom. (inj_linv) We take the following as an axiom:
∀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...
Axiom. (bij_inv) We take the following as an axiom:
∀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...
Definition. We define atleastp to be λX Y : set ⇒ ∃f : set → set, inj X Y f of type set → set → prop.
In Proofgold the corresponding term root is 9bb9c2... and object id is 13545c...
Axiom. (atleastp_tra) We take the following as an axiom:
∀X Y Z, atleastp X Y → atleastp Y Z → atleastp X Z
In Proofgold the corresponding term root is 0e83bf... and proposition id is c412bf...
Axiom. (Subq_atleastp) We take the following as an axiom:
∀X Y, X ⊆ Y → atleastp X Y
In Proofgold the corresponding term root is 507ac6... and proposition id is 3a427f...
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...
Axiom. (equip_atleastp) We take the following as an axiom:
∀X Y, equip X Y → atleastp X Y
In Proofgold the corresponding term root is c9d4bd... and proposition id is 9a412a...
Axiom. (equip_ref) We take the following as an axiom:
∀X, equip X X
In Proofgold the corresponding term root is cc7e80... and proposition id is c41fb1...
Axiom. (equip_sym) We take the following as an axiom:
∀X Y, equip X Y → equip Y X
In Proofgold the corresponding term root is f28954... and proposition id is 272f04...
Axiom. (equip_tra) We take the following as an axiom:
∀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...
Axiom. (equip_0_Empty) We take the following as an axiom:
∀X, equip X 0 → X = 0
In Proofgold the corresponding term root is 83ab2f... and proposition id is 4c101c...
Axiom. (equip_adjoin_ordsucc) We take the following as an axiom:
∀N X y, y ∉ X → equip N X → equip (ordsucc N) (X ∪ {y})
In Proofgold the corresponding term root is eab190... and proposition id is e8bc03...
Axiom. (equip_ordsucc_remove1) We take the following as an axiom:
∀X N, ∀x ∈ X, equip X (ordsucc N) → equip (X ∖ {x}) N
In Proofgold the corresponding term root is 997b32... and proposition id is 9c2236...
Beginning of Section SchroederBernstein
Axiom. (KnasterTarski_set) We take the following as an axiom:
∀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...
Axiom. (image_In_Power) We take the following as an axiom:
∀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...
Axiom. (image_monotone) We take the following as an axiom:
∀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...
Axiom. (setminus_antimonotone) We take the following as an axiom:
∀A U V, U ⊆ V → A ∖ V ⊆ A ∖ U
In Proofgold the corresponding term root is 67bd0e... and proposition id is f9b735...
Axiom. (SchroederBernstein) We take the following as an axiom:
∀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...
Axiom. (atleastp_antisym_equip) We take the following as an axiom:
∀A B, atleastp A B → atleastp B A → equip A B
In Proofgold the corresponding term root is e218ed... and proposition id is 2c48a8...
End of Section SchroederBernstein
Beginning of Section PigeonHole
Axiom. (PigeonHole_nat) We take the following as an axiom:
∀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...
Axiom. (Pigeonhole_not_atleastp_ordsucc) We take the following as an axiom:
∀n, nat_p n → ¬ atleastp (ordsucc n) n
In Proofgold the corresponding term root is 8a6bdc... and proposition id is 4fb58b...
End of Section PigeonHole
Axiom. (Union_ordsucc_eq) We take the following as an axiom:
∀n, nat_p n → ⋃ (ordsucc n) = n
In Proofgold the corresponding term root is 87308c... and proposition id is e8cdeb...
Axiom. (cases_1) We take the following as an axiom:
∀i ∈ 1, ∀p : set → prop, p 0 → p i
In Proofgold the corresponding term root is 706605... and proposition id is c6f0c0...
Axiom. (cases_2) We take the following as an axiom:
∀i ∈ 2, ∀p : set → prop, p 0 → p 1 → p i
In Proofgold the corresponding term root is 4693b2... and proposition id is 74563a...
Axiom. (neq_0_1) We take the following as an axiom:
0 ≠ 1
In Proofgold the corresponding term root is 9630fd... and proposition id is 74867a...
Axiom. (neq_1_0) We take the following as an axiom:
1 ≠ 0
In Proofgold the corresponding term root is 3a0478... and proposition id is 952fed...
Axiom. (neq_0_2) We take the following as an axiom:
0 ≠ 2
In Proofgold the corresponding term root is 055580... and proposition id is 9c9a3f...
Axiom. (neq_2_0) We take the following as an axiom:
2 ≠ 0
In Proofgold the corresponding term root is 4d54d8... and proposition id is 00b357...
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...
Axiom. (ordinal_TransSet) We take the following as an axiom:
∀alpha : set, ordinal alpha → TransSet alpha
In Proofgold the corresponding term root is 0dbaa3... and proposition id is c9e708...
Axiom. (ordinal_Empty) We take the following as an axiom:
ordinal Empty
In Proofgold the corresponding term root is ce6bea... and proposition id is 7d95d1...
Axiom. (ordinal_Hered) We take the following as an axiom:
∀alpha : set, ordinal alpha → ∀beta ∈ alpha, ordinal beta
In Proofgold the corresponding term root is a7e78b... and proposition id is 43b0f3...
Axiom. (TransSet_ordsucc) We take the following as an axiom:
∀X : set, TransSet X → TransSet (ordsucc X)
In Proofgold the corresponding term root is fc2157... and proposition id is ebf9e3...
Axiom. (ordinal_ordsucc) We take the following as an axiom:
∀alpha : set, ordinal alpha → ordinal (ordsucc alpha)
In Proofgold the corresponding term root is 0ba97f... and proposition id is ab0f7f...
Axiom. (nat_p_ordinal) We take the following as an axiom:
∀n : set, nat_p n → ordinal n
In Proofgold the corresponding term root is 274fc4... and proposition id is 47cd49...
Axiom. (ordinal_1) We take the following as an axiom:
ordinal 1
In Proofgold the corresponding term root is c94d41... and proposition id is e325a5...
Axiom. (ordinal_2) We take the following as an axiom:
ordinal 2
In Proofgold the corresponding term root is a57075... and proposition id is e64a0d...
Axiom. (TransSet_ordsucc_In_Subq) We take the following as an axiom:
∀X : set, TransSet X → ∀x ∈ X, ordsucc x ⊆ X
In Proofgold the corresponding term root is d5d882... and proposition id is 3c2e45...
Axiom. (ordinal_ordsucc_In_Subq) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta ∈ alpha, ordsucc beta ⊆ alpha
In Proofgold the corresponding term root is 57345e... and proposition id is b00304...
Axiom. (ordinal_trichotomy_or) We take the following as an axiom:
∀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...
Axiom. (ordinal_trichotomy_or_impred) We take the following as an axiom:
∀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...
Axiom. (ordinal_In_Or_Subq) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha ∈ beta ∨ beta ⊆ alpha
In Proofgold the corresponding term root is 70fe0d... and proposition id is 7b99b0...
Axiom. (ordinal_linear) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta ∨ beta ⊆ alpha
In Proofgold the corresponding term root is 3f30a5... and proposition id is 3b1fce...
Axiom. (ordinal_ordsucc_In_eq) We take the following as an axiom:
∀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...
Axiom. (ordinal_lim_or_succ) We take the following as an axiom:
∀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...
Axiom. (ordinal_ordsucc_In) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta ∈ alpha, ordsucc beta ∈ ordsucc alpha
In Proofgold the corresponding term root is f4b1ed... and proposition id is 8ab1dc...
Axiom. (ordinal_famunion) We take the following as an axiom:
∀X, ∀F : set → set, (∀x ∈ X, ordinal (F x)) → ordinal (⋃x ∈ XF x)
In Proofgold the corresponding term root is fc0359... and proposition id is b3f1e1...
Axiom. (ordinal_binintersect) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → ordinal (alpha ∩ beta)
In Proofgold the corresponding term root is 43d507... and proposition id is 025328...
Axiom. (ordinal_binunion) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → ordinal (alpha ∪ beta)
In Proofgold the corresponding term root is 861ae3... and proposition id is b24989...
Axiom. (ordinal_ind) We take the following as an axiom:
∀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...
Axiom. (least_ordinal_ex) We take the following as an axiom:
∀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...
Axiom. (equip_Sing_1) We take the following as an axiom:
∀x, equip {x} 1
In Proofgold the corresponding term root is be1ab2... and proposition id is 5169f4...
Axiom. (TransSet_In_ordsucc_Subq) We take the following as an axiom:
∀x y, TransSet y → x ∈ ordsucc y → x ⊆ y
In Proofgold the corresponding term root is f80c6e... and proposition id is 341993...
Axiom. (exandE_i) We take the following as an axiom:
∀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...
Axiom. (exandE_ii) We take the following as an axiom:
∀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...
Axiom. (exandE_iii) We take the following as an axiom:
∀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...
Axiom. (exandE_iiii) We take the following as an axiom:
∀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...
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.
In Proofgold the corresponding term root is 3bae39... and object id is 3a4ad2...
Hypothesis Pex : ∃f : set → set, P f
Hypothesis Puniq : ∀f g : set → set, P f → P g → f = g
Axiom. (Descr_ii_prop) We take the following as an axiom:
P Descr_ii
In Proofgold the corresponding term root is 45bfc0... and proposition id is e705d1...
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.
In Proofgold the corresponding term root is ca5fc1... and object id is 877e40...
Hypothesis Pex : ∃f : set → set → set, P f
Hypothesis Puniq : ∀f g : set → set → set, P f → P g → f = g
Axiom. (Descr_iii_prop) We take the following as an axiom:
P Descr_iii
In Proofgold the corresponding term root is 261c3d... and proposition id is 160421...
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.
In Proofgold the corresponding term root is 615c0a... and object id is a4ecdd...
Hypothesis Pex : ∃f : Vo 1, P f
Hypothesis Puniq : ∀f g : Vo 1, P f → P g → f = g
Axiom. (Descr_Vo1_prop) We take the following as an axiom:
P Descr_Vo1
In Proofgold the corresponding term root is f550ef... and proposition id is 2213e2...
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.
In Proofgold the corresponding term root is 17057f... and object id is e29015...
Axiom. (If_ii_1) We take the following as an axiom:
p → If_ii = f
In Proofgold the corresponding term root is 31521e... and proposition id is 342a1f...
Axiom. (If_ii_0) We take the following as an axiom:
¬ p → If_ii = g
In Proofgold the corresponding term root is 6acab0... and proposition id is 36418b...
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.
In Proofgold the corresponding term root is 331476... and object id is dd7e2b...
Axiom. (If_iii_1) We take the following as an axiom:
p → If_iii = f
In Proofgold the corresponding term root is 2d62ee... and proposition id is 48bc10...
Axiom. (If_iii_0) We take the following as an axiom:
¬ p → If_iii = g
In Proofgold the corresponding term root is 9b77d9... and proposition id is d11201...
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.
In Proofgold the corresponding term root is fde509... and object id is a81e18...
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...
Axiom. (In_rec_i_G_c) We take the following as an axiom:
∀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...
Axiom. (In_rec_i_G_inv) We take the following as an axiom:
∀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...
Hypothesis Fr : ∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h
Axiom. (In_rec_i_G_f) We take the following as an axiom:
∀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...
Axiom. (In_rec_i_G_In_rec_i) We take the following as an axiom:
∀X : set, In_rec_i_G X (In_rec_i X)
In Proofgold the corresponding term root is 095407... and proposition id is dc2359...
Axiom. (In_rec_i_G_In_rec_i_d) We take the following as an axiom:
∀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...
Axiom. (In_rec_i_eq) We take the following as an axiom:
∀X : set, In_rec_i X = F X In_rec_i
In Proofgold the corresponding term root is 110653... and proposition id is e8653b...
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.
In Proofgold the corresponding term root is 6edba9... and object id is b31dbf...
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...
Axiom. (In_rec_G_ii_c) We take the following as an axiom:
∀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...
Axiom. (In_rec_G_ii_inv) We take the following as an axiom:
∀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...
Hypothesis Fr : ∀X : set, ∀g h : set → (set → set), (∀x ∈ X, g x = h x) → F X g = F X h
Axiom. (In_rec_G_ii_f) We take the following as an axiom:
∀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...
Axiom. (In_rec_G_ii_In_rec_ii) We take the following as an axiom:
∀X : set, In_rec_G_ii X (In_rec_ii X)
In Proofgold the corresponding term root is b2f81f... and proposition id is 2893f4...
Axiom. (In_rec_G_ii_In_rec_ii_d) We take the following as an axiom:
∀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...
Axiom. (In_rec_ii_eq) We take the following as an axiom:
∀X : set, In_rec_ii X = F X In_rec_ii
In Proofgold the corresponding term root is f7aff6... and proposition id is 7bb1e9...
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.
In Proofgold the corresponding term root is 533cc7... and object id is 7a2f6b...
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...
Axiom. (In_rec_G_iii_c) We take the following as an axiom:
∀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...
Axiom. (In_rec_G_iii_inv) We take the following as an axiom:
∀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...
Hypothesis Fr : ∀X : set, ∀g h : set → (set → set → set), (∀x ∈ X, g x = h x) → F X g = F X h
Axiom. (In_rec_G_iii_f) We take the following as an axiom:
∀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...
Axiom. (In_rec_G_iii_In_rec_iii) We take the following as an axiom:
∀X : set, In_rec_G_iii X (In_rec_iii X)
In Proofgold the corresponding term root is d8c3ba... and proposition id is 37f9a7...
Axiom. (In_rec_G_iii_In_rec_iii_d) We take the following as an axiom:
∀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...
Axiom. (In_rec_iii_eq) We take the following as an axiom:
∀X : set, In_rec_iii X = F X In_rec_iii
In Proofgold the corresponding term root is 5f0574... and proposition id is a0709d...
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.
In Proofgold the corresponding term root is 3be1c5... and object id is 1a64d5...
Axiom. (nat_primrec_r) We take the following as an axiom:
∀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...
Axiom. (nat_primrec_0) We take the following as an axiom:
nat_primrec 0 = z
In Proofgold the corresponding term root is 416eaf... and proposition id is be11a2...
Axiom. (nat_primrec_S) We take the following as an axiom:
∀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...
End of Section NatRec
Beginning of Section NatAdd
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.
Axiom. (add_nat_0R) We take the following as an axiom:
∀n : set, n + 0 = n
In Proofgold the corresponding term root is 402bcb... and proposition id is 23277f...
Axiom. (add_nat_SR) We take the following as an axiom:
∀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...
Axiom. (add_nat_p) We take the following as an axiom:
∀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...
Axiom. (add_nat_1_1_2) We take the following as an axiom:
1 + 1 = 2
In Proofgold the corresponding term root is 174b87... and proposition id is 77f23f...
Axiom. (add_nat_asso) We take the following as an axiom:
∀n : set, nat_p n → ∀m : set, nat_p m → ∀k : set, nat_p k → (n + m) + k = n + (m + k)
In Proofgold the corresponding term root is c81c09... and proposition id is eec294...
Axiom. (add_nat_0L) We take the following as an axiom:
∀m : set, nat_p m → 0 + m = m
In Proofgold the corresponding term root is 8ceeb9... and proposition id is 84fbe4...
Axiom. (add_nat_SL) We take the following as an axiom:
∀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...
Axiom. (add_nat_com) We take the following as an axiom:
∀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...
Axiom. (add_nat_In_R) We take the following as an axiom:
∀m, nat_p m → ∀k ∈ m, ∀n, nat_p n → k + n ∈ m + n
In Proofgold the corresponding term root is eeaa55... and proposition id is 85b3ac...
Axiom. (add_nat_In_L) We take the following as an axiom:
∀n, nat_p n → ∀m, nat_p m → ∀k ∈ m, n + k ∈ n + m
In Proofgold the corresponding term root is 0572fd... and proposition id is eaa26c...
Axiom. (add_nat_Subq_R) We take the following as an axiom:
∀k, nat_p k → ∀m, nat_p m → k ⊆ m → ∀n, nat_p n → k + n ⊆ m + n
In Proofgold the corresponding term root is 0d6a07... and proposition id is d59a02...
Axiom. (add_nat_Subq_L) We take the following as an axiom:
∀n, nat_p n → ∀k, nat_p k → ∀m, nat_p m → k ⊆ m → n + k ⊆ n + m
In Proofgold the corresponding term root is b7d52c... and proposition id is 586cfc...
Axiom. (add_nat_Subq_R') We take the following as an axiom:
∀m, nat_p m → ∀n, nat_p n → m ⊆ m + n
In Proofgold the corresponding term root is ed3e7e... and proposition id is cff680...
Axiom. (nat_Subq_add_ex) We take the following as an axiom:
∀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...
Axiom. (add_nat_cancel_R) We take the following as an axiom:
∀k, nat_p k → ∀m, nat_p m → ∀n, nat_p n → k + n = m + n → k = m
In Proofgold the corresponding term root is acfe90... and proposition id is 1c3ee5...
End of Section NatAdd
Beginning of Section NatMul
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
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.
Axiom. (mul_nat_0R) We take the following as an axiom:
∀n : set, n * 0 = 0
In Proofgold the corresponding term root is b2f56c... and proposition id is 1e5b2c...
Axiom. (mul_nat_SR) We take the following as an axiom:
∀n m, nat_p m → n * ordsucc m = n + n * m
In Proofgold the corresponding term root is 37df54... and proposition id is 6dd6fc...
Axiom. (mul_nat_1R) We take the following as an axiom:
∀n, n * 1 = n
In Proofgold the corresponding term root is cab8eb... and proposition id is a3051d...
Axiom. (mul_nat_p) We take the following as an axiom:
∀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...
Axiom. (mul_nat_0L) We take the following as an axiom:
∀m : set, nat_p m → 0 * m = 0
In Proofgold the corresponding term root is db8a35... and proposition id is 6a2dd6...
Axiom. (mul_nat_SL) We take the following as an axiom:
∀n : set, nat_p n → ∀m : set, nat_p m → ordsucc n * m = n * m + m
In Proofgold the corresponding term root is 5cf7ec... and proposition id is 24e4eb...
Axiom. (mul_nat_com) We take the following as an axiom:
∀n : set, nat_p n → ∀m : set, nat_p m → n * m = m * n
In Proofgold the corresponding term root is 4525ef... and proposition id is 5d6ce4...
Axiom. (mul_add_nat_distrL) We take the following as an axiom:
∀n : set, nat_p n → ∀m : set, nat_p m → ∀k : set, nat_p k → n * (m + k) = n * m + n * k
In Proofgold the corresponding term root is 7758f1... and proposition id is d57b02...
Axiom. (mul_nat_asso) We take the following as an axiom:
∀n : set, nat_p n → ∀m : set, nat_p m → ∀k : set, nat_p k → (n * m) * k = n * (m * k)
In Proofgold the corresponding term root is 564886... and proposition id is 229d2c...
Axiom. (mul_nat_Subq_R) We take the following as an axiom:
∀m n, nat_p m → nat_p n → m ⊆ n → ∀k, nat_p k → m * k ⊆ n * k
In Proofgold the corresponding term root is d99b10... and proposition id is 4324d1...
Axiom. (mul_nat_Subq_L) We take the following as an axiom:
∀m n, nat_p m → nat_p n → m ⊆ n → ∀k, nat_p k → k * m ⊆ k * n
In Proofgold the corresponding term root is 929864... and proposition id is df9ccb...
Axiom. (mul_nat_0_or_Subq) We take the following as an axiom:
∀m, nat_p m → ∀n, nat_p n → n = 0 ∨ m ⊆ m * n
In Proofgold the corresponding term root is bdf0eb... and proposition id is 2bbf0e...
Axiom. (mul_nat_0_inv) We take the following as an axiom:
∀m, nat_p m → ∀n, nat_p n → m * n = 0 → m = 0 ∨ n = 0
In Proofgold the corresponding term root is 2da221... and proposition id is f3fbb4...
Axiom. (mul_nat_0m_1n_In) We take the following as an axiom:
∀m, nat_p m → ∀n, nat_p n → 0 ∈ m → 1 ∈ n → m ∈ m * n
In Proofgold the corresponding term root is 611f85... and proposition id is 5d96a9...
Axiom. (nat_le1_cases) We take the following as an axiom:
∀m, nat_p m → m ⊆ 1 → m = 0 ∨ m = 1
In Proofgold the corresponding term root is 591dbf... and proposition id is 5d5690...
Definition. We define Pi_nat to be λf n ⇒ nat_primrec 1 (λi r ⇒ r * f i) n of type (set → set) → set → set.
In Proofgold the corresponding term root is a0b865... and object id is 70d0e8...
Axiom. (Pi_nat_0) We take the following as an axiom:
∀f : set → set, Pi_nat f 0 = 1
In Proofgold the corresponding term root is 6af04c... and proposition id is b7ebea...
Axiom. (Pi_nat_S) We take the following as an axiom:
∀f : set → set, ∀n, nat_p n → Pi_nat f (ordsucc n) = Pi_nat f n * f n
In Proofgold the corresponding term root is 15f21a... and proposition id is b5fbbf...
Axiom. (Pi_nat_p) We take the following as an axiom:
∀f : set → set, ∀n, nat_p n → (∀i ∈ n, nat_p (f i)) → nat_p (Pi_nat f n)
In Proofgold the corresponding term root is 1e8072... and proposition id is 58005c...
Axiom. (Pi_nat_0_inv) We take the following as an axiom:
∀f : set → set, ∀n, nat_p n → (∀i ∈ n, nat_p (f i)) → Pi_nat f n = 0 → (∃i ∈ n, f i = 0)
In Proofgold the corresponding term root is 688c96... and proposition id is 98d7e0...
End of Section NatMul
Axiom. (ZF_closed_E) We take the following as an axiom:
∀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...
Axiom. (ZF_Union_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀X ∈ U, ⋃ X ∈ U
In Proofgold the corresponding term root is a7cdf1... and proposition id is 250496...
Axiom. (ZF_Power_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀X ∈ U, 𝒫 X ∈ U
In Proofgold the corresponding term root is 5d781f... and proposition id is 7411dd...
Axiom. (ZF_Repl_closed) We take the following as an axiom:
∀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...
Axiom. (ZF_UPair_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀x y ∈ U, {x,y} ∈ U
In Proofgold the corresponding term root is 54256a... and proposition id is ef42d3...
Axiom. (ZF_Sing_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀x ∈ U, {x} ∈ U
In Proofgold the corresponding term root is 5d8a83... and proposition id is d02d66...
Axiom. (ZF_binunion_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀X Y ∈ U, (X ∪ Y) ∈ U
In Proofgold the corresponding term root is 8a6240... and proposition id is 1bacfd...
Axiom. (ZF_ordsucc_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀x ∈ U, ordsucc x ∈ U
In Proofgold the corresponding term root is 68a6ba... and proposition id is 946e61...
Axiom. (nat_p_UnivOf_Empty) We take the following as an axiom:
∀n : set, nat_p n → n ∈ UnivOf Empty
In Proofgold the corresponding term root is c885b4... and proposition id is 645aee...
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...
Axiom. (omega_nat_p) We take the following as an axiom:
∀n ∈ ω, nat_p n
In Proofgold the corresponding term root is f44a30... and proposition id is c2c61b...
Axiom. (nat_p_omega) We take the following as an axiom:
∀n : set, nat_p n → n ∈ ω
In Proofgold the corresponding term root is 6a1b44... and proposition id is d5080f...
Axiom. (omega_ordsucc) We take the following as an axiom:
∀n ∈ ω, ordsucc n ∈ ω
In Proofgold the corresponding term root is 246d63... and proposition id is 17fb64...
Axiom. (form100_22_v2) We take the following as an axiom:
∀f : set → set, ¬ inj (𝒫 ω) ω f
In Proofgold the corresponding term root is eabc14... and proposition id is 5eb9bd...
Axiom. (form100_22_v3) We take the following as an axiom:
∀g : set → set, ¬ surj ω (𝒫 ω) g
In Proofgold the corresponding term root is 4de6f8... and proposition id is b20e6a...
Axiom. (form100_22_v1) We take the following as an axiom:
¬ equip ω (𝒫 ω)
In Proofgold the corresponding term root is 7ab652... and proposition id is a76888...
Axiom. (omega_TransSet) We take the following as an axiom:
TransSet ω
In Proofgold the corresponding term root is 8e89e6... and proposition id is c79e75...
Axiom. (omega_ordinal) We take the following as an axiom:
ordinal ω
In Proofgold the corresponding term root is 3d621a... and proposition id is 177484...
Axiom. (ordsucc_omega_ordinal) We take the following as an axiom:
ordinal (ordsucc ω)
In Proofgold the corresponding term root is 66659c... and proposition id is ecfad7...
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...
Axiom. (nat_finite) We take the following as an axiom:
∀n, nat_p n → finite n
In Proofgold the corresponding term root is a27dbe... and proposition id is 9b83bf...
Axiom. (finite_ind) We take the following as an axiom:
∀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...
Axiom. (finite_Empty) We take the following as an axiom:
finite 0
In Proofgold the corresponding term root is c073c6... and proposition id is ec2c27...
Axiom. (Sing_finite) We take the following as an axiom:
∀x, finite {x}
In Proofgold the corresponding term root is f7016a... and proposition id is 281486...
Axiom. (adjoin_finite) We take the following as an axiom:
∀X y, finite X → finite (X ∪ {y})
In Proofgold the corresponding term root is def317... and proposition id is e6aa6d...
Axiom. (binunion_finite) We take the following as an axiom:
∀X, finite X → ∀Y, finite Y → finite (X ∪ Y)
In Proofgold the corresponding term root is fc26bb... and proposition id is 3365a6...
Axiom. (famunion_nat_finite) We take the following as an axiom:
∀X : set → set, ∀n, nat_p n → (∀i ∈ n, finite (X i)) → finite (⋃i ∈ nX i)
In Proofgold the corresponding term root is 7f709a... and proposition id is f84ed0...
Axiom. (Subq_finite) We take the following as an axiom:
∀X, finite X → ∀Y, Y ⊆ X → finite Y
In Proofgold the corresponding term root is 6b062c... and proposition id is e4e3ee...
Definition. We define infinite to be λA ⇒ ¬ finite A of type set → prop.
In Proofgold the corresponding term root is 313e7b... and object id is fad8ea...
Beginning of Section InfinitePrimes
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.
Definition. We define divides_nat to be λm n ⇒ m ∈ ω ∧ n ∈ ω ∧ ∃k ∈ ω, m * k = n of type set → set → prop.
In Proofgold the corresponding term root is 1b17d5... and object id is 355928...
Axiom. (divides_nat_ref) We take the following as an axiom:
∀n, nat_p n → divides_nat n n
In Proofgold the corresponding term root is 98e754... and proposition id is 913818...
Axiom. (divides_nat_tra) We take the following as an axiom:
∀k m n, divides_nat k m → divides_nat m n → divides_nat k n
In Proofgold the corresponding term root is f799b9... and proposition id is e4e38e...
Definition. We define prime_nat to be λn ⇒ n ∈ ω ∧ 1 ∈ n ∧ ∀k ∈ ω, divides_nat k n → k = 1 ∨ k = n of type set → prop.
In Proofgold the corresponding term root is 729ee8... and object id is a54ca4...
Axiom. (divides_nat_mulR) We take the following as an axiom:
∀m n ∈ ω, divides_nat m (m * n)
In Proofgold the corresponding term root is eec687... and proposition id is ceb239...
Axiom. (divides_nat_mulL) We take the following as an axiom:
∀m n ∈ ω, divides_nat n (m * n)
In Proofgold the corresponding term root is cc5e38... and proposition id is d5d991...
Axiom. (Pi_nat_divides) We take the following as an axiom:
∀f : set → set, ∀n, nat_p n → (∀i ∈ n, nat_p (f i)) → (∀i ∈ n, divides_nat (f i) (Pi_nat f n))
In Proofgold the corresponding term root is 5e46a8... and proposition id is 2325b8...
Definition. We define composite_nat to be λn ⇒ n ∈ ω ∧ ∃k m ∈ ω, 1 ∈ k ∧ 1 ∈ m ∧ k * m = n of type set → prop.
In Proofgold the corresponding term root is 38d880... and object id is 3dafd8...
Axiom. (prime_nat_or_composite_nat) We take the following as an axiom:
∀n ∈ ω, 1 ∈ n → prime_nat n ∨ composite_nat n
In Proofgold the corresponding term root is a8970f... and proposition id is a1c7fc...
Axiom. (prime_nat_divisor_ex) We take the following as an axiom:
∀n, nat_p n → 1 ∈ n → ∃p, prime_nat p ∧ divides_nat p n
In Proofgold the corresponding term root is 2a24d5... and proposition id is 979fd7...
Axiom. (nat_1In_not_divides_ordsucc) We take the following as an axiom:
∀m n, 1 ∈ m → divides_nat m n → ¬ divides_nat m (ordsucc n)
In Proofgold the corresponding term root is 96fffb... and proposition id is 8d635d...
Definition. We define primes to be {n ∈ ω|prime_nat n} of type set.
In Proofgold the corresponding term root is f3caf8... and object id is 98dde1...
Axiom. (form100_11_infinite_primes) We take the following as an axiom:
infinite primes
In Proofgold the corresponding term root is 34eb3c... and proposition id is 13f23d...
End of Section InfinitePrimes
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...
Axiom. (Inj1_eq) We take the following as an axiom:
∀X : set, Inj1 X = {0} ∪ {Inj1 x|x ∈ X}
In Proofgold the corresponding term root is 73d189... and proposition id is b80457...
Axiom. (Inj1I1) We take the following as an axiom:
∀X : set, 0 ∈ Inj1 X
In Proofgold the corresponding term root is 3c2cc4... and proposition id is 4ccac3...
Axiom. (Inj1I2) We take the following as an axiom:
∀X x : set, x ∈ X → Inj1 x ∈ Inj1 X
In Proofgold the corresponding term root is b6f23b... and proposition id is 086475...
Axiom. (Inj1E) We take the following as an axiom:
∀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...
Axiom. (Inj1NE1) We take the following as an axiom:
∀x : set, Inj1 x ≠ 0
In Proofgold the corresponding term root is 5e3197... and proposition id is 09bd10...
Axiom. (Inj1NE2) We take the following as an axiom:
∀x : set, Inj1 x ∉ {0}
In Proofgold the corresponding term root is 9e94b1... and proposition id is 3c4dd0...
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...
Axiom. (Inj0I) We take the following as an axiom:
∀X x : set, x ∈ X → Inj1 x ∈ Inj0 X
In Proofgold the corresponding term root is 7fc2e9... and proposition id is 565378...
Axiom. (Inj0E) We take the following as an axiom:
∀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...
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...
Axiom. (Unj_eq) We take the following as an axiom:
∀X : set, Unj X = {Unj x|x ∈ X ∖ {0}}
In Proofgold the corresponding term root is 3b1aa6... and proposition id is b4c852...
Axiom. (Unj_Inj1_eq) We take the following as an axiom:
∀X : set, Unj (Inj1 X) = X
In Proofgold the corresponding term root is e2cdfc... and proposition id is ae00e1...
Axiom. (Inj1_inj) We take the following as an axiom:
∀X Y : set, Inj1 X = Inj1 Y → X = Y
In Proofgold the corresponding term root is ce8b66... and proposition id is 3e918a...
Axiom. (Unj_Inj0_eq) We take the following as an axiom:
∀X : set, Unj (Inj0 X) = X
In Proofgold the corresponding term root is f3e39c... and proposition id is 3808ad...
Axiom. (Inj0_inj) We take the following as an axiom:
∀X Y : set, Inj0 X = Inj0 Y → X = Y
In Proofgold the corresponding term root is 662f53... and proposition id is 29f945...
Axiom. (Inj0_0) We take the following as an axiom:
Inj0 0 = 0
In Proofgold the corresponding term root is 171f47... and proposition id is 57f5af...
Axiom. (Inj0_Inj1_neq) We take the following as an axiom:
∀X Y : set, Inj0 X ≠ Inj1 Y
In Proofgold the corresponding term root is 21bb03... and proposition id is 2b14d8...
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.
Axiom. (Inj0_setsum) We take the following as an axiom:
∀X Y x : set, x ∈ X → Inj0 x ∈ X + Y
In Proofgold the corresponding term root is 1c6408... and proposition id is 246ac5...
Axiom. (Inj1_setsum) We take the following as an axiom:
∀X Y y : set, y ∈ Y → Inj1 y ∈ X + Y
In Proofgold the corresponding term root is d47a0f... and proposition id is 2b4f94...
Axiom. (setsum_Inj_inv) We take the following as an axiom:
∀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...
Axiom. (Inj0_setsum_0L) We take the following as an axiom:
∀X : set, 0 + X = Inj0 X
In Proofgold the corresponding term root is 0be1e7... and proposition id is 36fabd...
Axiom. (Inj1_setsum_1L) We take the following as an axiom:
∀X : set, 1 + X = Inj1 X
In Proofgold the corresponding term root is f8d721... and proposition id is 45b1c8...
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.
In Proofgold the corresponding term root is 21a488... and object id is 9c5e4e...
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...
Axiom. (Inj0_pair_0_eq) We take the following as an axiom:
Inj0 = pair 0
In Proofgold the corresponding term root is 0fe601... and proposition id is 490c2a...
Axiom. (Inj1_pair_1_eq) We take the following as an axiom:
Inj1 = pair 1
In Proofgold the corresponding term root is 0bbde8... and proposition id is 8272d7...
Axiom. (pairI0) We take the following as an axiom:
∀X Y x, x ∈ X → pair 0 x ∈ pair X Y
In Proofgold the corresponding term root is 21a414... and proposition id is 34813b...
Axiom. (pairI1) We take the following as an axiom:
∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y
In Proofgold the corresponding term root is bdaab5... and proposition id is b5248b...
Axiom. (pairE) We take the following as an axiom:
∀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...
Axiom. (pairE0) We take the following as an axiom:
∀X Y x, pair 0 x ∈ pair X Y → x ∈ X
In Proofgold the corresponding term root is 042f30... and proposition id is f50b25...
Axiom. (pairE1) We take the following as an axiom:
∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y
In Proofgold the corresponding term root is 505cfc... and proposition id is 30a181...
Axiom. (proj0I) We take the following as an axiom:
∀w u : set, pair 0 u ∈ w → u ∈ proj0 w
In Proofgold the corresponding term root is be55b9... and proposition id is 840c8d...
Axiom. (proj0E) We take the following as an axiom:
∀w u : set, u ∈ proj0 w → pair 0 u ∈ w
In Proofgold the corresponding term root is b9afa9... and proposition id is 5b7f58...
Axiom. (proj1I) We take the following as an axiom:
∀w u : set, pair 1 u ∈ w → u ∈ proj1 w
In Proofgold the corresponding term root is fbddb7... and proposition id is 595b3c...
Axiom. (proj1E) We take the following as an axiom:
∀w u : set, u ∈ proj1 w → pair 1 u ∈ w
In Proofgold the corresponding term root is 06e32e... and proposition id is c3c3e6...
Axiom. (proj0_pair_eq) We take the following as an axiom:
∀X Y : set, proj0 (pair X Y) = X
In Proofgold the corresponding term root is d546f3... and proposition id is 0c12fb...
Axiom. (proj1_pair_eq) We take the following as an axiom:
∀X Y : set, proj1 (pair X Y) = Y
In Proofgold the corresponding term root is 9f98a8... and proposition id is e0cb0f...
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.
Axiom. (Sigma_eta_proj0_proj1) We take the following as an axiom:
∀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...
Axiom. (proj0_Sigma) We take the following as an axiom:
∀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...
Axiom. (proj1_Sigma) We take the following as an axiom:
∀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...
Axiom. (pair_Sigma) We take the following as an axiom:
∀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...
Axiom. (pair_Sigma_E1) We take the following as an axiom:
∀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...
Axiom. (Sigma_E) We take the following as an axiom:
∀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...
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.
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.
In Proofgold the corresponding term root is c7aaa6... and object id is a4d82c...
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 (a0,...,an-1) for n ≥ 2 for λ i ∈ n . if i = 0 then a0 else ... if i = n-2 then an-2 else an-1.
Axiom. (lamI) We take the following as an axiom:
∀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...
Axiom. (lamE) We take the following as an axiom:
∀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...
Axiom. (apI) We take the following as an axiom:
∀f x y, pair x y ∈ f → y ∈ f x
In Proofgold the corresponding term root is 64667c... and proposition id is 770816...
Axiom. (apE) We take the following as an axiom:
∀f x y, y ∈ f x → pair x y ∈ f
In Proofgold the corresponding term root is 85693a... and proposition id is c08565...
Axiom. (beta) We take the following as an axiom:
∀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...
Axiom. (proj0_ap_0) We take the following as an axiom:
∀u, proj0 u = u 0
In Proofgold the corresponding term root is 588f37... and proposition id is d4f351...
Axiom. (proj1_ap_1) We take the following as an axiom:
∀u, proj1 u = u 1
In Proofgold the corresponding term root is d116b3... and proposition id is 2328b0...
Axiom. (pair_ap_0) We take the following as an axiom:
∀x y : set, (pair x y) 0 = x
In Proofgold the corresponding term root is ac34b9... and proposition id is bb0477...
Axiom. (pair_ap_1) We take the following as an axiom:
∀x y : set, (pair x y) 1 = y
In Proofgold the corresponding term root is 2274fc... and proposition id is cce3d2...
Axiom. (ap0_Sigma) We take the following as an axiom:
∀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...
Axiom. (ap1_Sigma) We take the following as an axiom:
∀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...
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...
Axiom. (pair_p_I) We take the following as an axiom:
∀x y, pair_p (pair x y)
In Proofgold the corresponding term root is 06d9a2... and proposition id is 8f2fde...
Axiom. (Subq_2_UPair01) We take the following as an axiom:
2 ⊆ {0,1}
In Proofgold the corresponding term root is d90884... and proposition id is 94203e...
Axiom. (tuple_pair) We take the following as an axiom:
∀x y : set, pair x y = (x,y)
In Proofgold the corresponding term root is c122f6... and proposition id is 18198e...
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.
Axiom. (PiI) We take the following as an axiom:
∀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...
Axiom. (lam_Pi) We take the following as an axiom:
∀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...
Axiom. (ap_Pi) We take the following as an axiom:
∀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...
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.
Axiom. (pair_tuple_fun) We take the following as an axiom:
pair = (λx y ⇒ (x,y))
In Proofgold the corresponding term root is b02dfa... and proposition id is ed37d0...
Beginning of Section Tuples
Variable x0 x1 : set
Axiom. (tuple_2_0_eq) We take the following as an axiom:
(x0,x1) 0 = x0
In Proofgold the corresponding term root is 42d452... and proposition id is ad9037...
Axiom. (tuple_2_1_eq) We take the following as an axiom:
(x0,x1) 1 = x1
In Proofgold the corresponding term root is 596569... and proposition id is 2c0ad1...
End of Section Tuples
Axiom. (ReplEq_setprod_ext) We take the following as an axiom:
∀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...
Axiom. (lamI2) We take the following as an axiom:
∀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...
Axiom. (tuple_2_Sigma) We take the following as an axiom:
∀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...
Axiom. (tuple_2_setprod) We take the following as an axiom:
∀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...
End of Section pair_setsum
Notation. We use ∑ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Sigma.
Notation. We use ⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.
Notation. We use ∏ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Pi.
Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.
Definition. We define DescrR_i_io_1 to be λR ⇒ Eps_i (λx ⇒ (∃y : set → prop, R x y) ∧ (∀y z : set → prop, R x y → R x z → y = z)) of type (set → (set → prop) → prop) → set.
In Proofgold the corresponding term root is 1d3fd4... and object id is 82aecc...
Definition. We define DescrR_i_io_2 to be λR ⇒ Descr_Vo1 (λy ⇒ R (DescrR_i_io_1 R) y) of type (set → (set → prop) → prop) → set → prop.
In Proofgold the corresponding term root is 768eb2... and object id is 3f82bc...
Axiom. (DescrR_i_io_12) We take the following as an axiom:
∀R : set → (set → prop) → prop, (∃x, (∃y : set → prop, R x y) ∧ (∀y z : set → prop, R x y → R x z → y = z)) → R (DescrR_i_io_1 R) (DescrR_i_io_2 R)
In Proofgold the corresponding term root is a4fae2... and proposition id is da4f02...
Definition. We define PNoEq_ to be λalpha p q ⇒ ∀beta ∈ alpha, p beta ↔ q beta of type set → (set → prop) → (set → prop) → prop.
In Proofgold the corresponding term root is d7d959... and object id is 144b65...
Axiom. (PNoEq_ref_) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoEq_ alpha p p
In Proofgold the corresponding term root is c27ebb... and proposition id is df4cf6...
Axiom. (PNoEq_sym_) We take the following as an axiom:
∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoEq_ alpha q p
In Proofgold the corresponding term root is b813f3... and proposition id is bfda0b...
Axiom. (PNoEq_tra_) We take the following as an axiom:
∀alpha, ∀p q r : set → prop, PNoEq_ alpha p q → PNoEq_ alpha q r → PNoEq_ alpha p r
In Proofgold the corresponding term root is dded4c... and proposition id is fc92f3...
Axiom. (PNoEq_antimon_) We take the following as an axiom:
∀p q : set → prop, ∀alpha, ordinal alpha → ∀beta ∈ alpha, PNoEq_ alpha p q → PNoEq_ beta p q
In Proofgold the corresponding term root is 8868e6... and proposition id is 094ae2...
Definition. We define PNoLt_ to be λalpha p q ⇒ ∃beta ∈ alpha, PNoEq_ beta p q ∧ ¬ p beta ∧ q beta of type set → (set → prop) → (set → prop) → prop.
In Proofgold the corresponding term root is 34de68... and object id is c95964...
Axiom. (PNoLt_E_) We take the following as an axiom:
∀alpha, ∀p q : set → prop, PNoLt_ alpha p q → ∀R : prop, (∀beta, beta ∈ alpha → PNoEq_ beta p q → ¬ p beta → q beta → R) → R
In Proofgold the corresponding term root is 9ba543... and proposition id is 45aec8...
Axiom. (PNoLt_irref_) We take the following as an axiom:
∀alpha, ∀p : set → prop, ¬ PNoLt_ alpha p p
In Proofgold the corresponding term root is fcb502... and proposition id is 987dff...
Axiom. (PNoLt_mon_) We take the following as an axiom:
∀p q : set → prop, ∀alpha, ordinal alpha → ∀beta ∈ alpha, PNoLt_ beta p q → PNoLt_ alpha p q
In Proofgold the corresponding term root is b1c3cf... and proposition id is d8d0f0...
Axiom. (PNoLt_trichotomy_or_) We take the following as an axiom:
∀p q : set → prop, ∀alpha, ordinal alpha → PNoLt_ alpha p q ∨ PNoEq_ alpha p q ∨ PNoLt_ alpha q p
In Proofgold the corresponding term root is 664408... and proposition id is 8d3824...
Definition. We define PNoLt to be λalpha p beta q ⇒ PNoLt_ (alpha ∩ beta) p q ∨ alpha ∈ beta ∧ PNoEq_ alpha p q ∧ q alpha ∨ beta ∈ alpha ∧ PNoEq_ beta p q ∧ ¬ p beta of type set → (set → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 8f57a0... and object id is f2094c...
Axiom. (PNoLtI1) We take the following as an axiom:
∀alpha beta, ∀p q : set → prop, PNoLt_ (alpha ∩ beta) p q → PNoLt alpha p beta q
In Proofgold the corresponding term root is c5735c... and proposition id is ecbc71...
Axiom. (PNoLtI2) We take the following as an axiom:
∀alpha beta, ∀p q : set → prop, alpha ∈ beta → PNoEq_ alpha p q → q alpha → PNoLt alpha p beta q
In Proofgold the corresponding term root is 419b53... and proposition id is 030093...
Axiom. (PNoLtI3) We take the following as an axiom:
∀alpha beta, ∀p q : set → prop, beta ∈ alpha → PNoEq_ beta p q → ¬ p beta → PNoLt alpha p beta q
In Proofgold the corresponding term root is c392cb... and proposition id is 410442...
Axiom. (PNoLtE) We take the following as an axiom:
∀alpha beta, ∀p q : set → prop, PNoLt alpha p beta q → ∀R : prop, (PNoLt_ (alpha ∩ beta) p q → R) → (alpha ∈ beta → PNoEq_ alpha p q → q alpha → R) → (beta ∈ alpha → PNoEq_ beta p q → ¬ p beta → R) → R
In Proofgold the corresponding term root is f7e6e3... and proposition id is af36ce...
Axiom. (PNoLt_irref) We take the following as an axiom:
∀alpha, ∀p : set → prop, ¬ PNoLt alpha p alpha p
In Proofgold the corresponding term root is ff1a80... and proposition id is d4c379...
Axiom. (PNoLt_trichotomy_or) We take the following as an axiom:
∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q ∨ PNoLt beta q alpha p
In Proofgold the corresponding term root is 4f39e4... and proposition id is 90b387...
Axiom. (PNoLtEq_tra) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → ∀p q r : set → prop, PNoLt alpha p beta q → PNoEq_ beta q r → PNoLt alpha p beta r
In Proofgold the corresponding term root is 2e082a... and proposition id is 2f2a82...
Axiom. (PNoEqLt_tra) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → ∀p q r : set → prop, PNoEq_ alpha p q → PNoLt alpha q beta r → PNoLt alpha p beta r
In Proofgold the corresponding term root is fe144b... and proposition id is f07654...
Axiom. (PNoLt_tra) We take the following as an axiom:
∀alpha beta gamma, ordinal alpha → ordinal beta → ordinal gamma → ∀p q r : set → prop, PNoLt alpha p beta q → PNoLt beta q gamma r → PNoLt alpha p gamma r
In Proofgold the corresponding term root is b72127... and proposition id is 8eff85...
Definition. We define PNoLe to be λalpha p beta q ⇒ PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q of type set → (set → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is ac6311... and object id is 770cf7...
Axiom. (PNoLeI1) We take the following as an axiom:
∀alpha beta, ∀p q : set → prop, PNoLt alpha p beta q → PNoLe alpha p beta q
In Proofgold the corresponding term root is 1f0528... and proposition id is 674a2c...
Axiom. (PNoLeI2) We take the following as an axiom:
∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoLe alpha p alpha q
In Proofgold the corresponding term root is b45332... and proposition id is 0b2157...
Axiom. (PNoLe_ref) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoLe alpha p alpha p
In Proofgold the corresponding term root is 1b91bd... and proposition id is 613386...
Axiom. (PNoLe_antisym) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → ∀p q : set → prop, PNoLe alpha p beta q → PNoLe beta q alpha p → alpha = beta ∧ PNoEq_ alpha p q
In Proofgold the corresponding term root is 934d7a... and proposition id is 4e3594...
Axiom. (PNoLtLe_tra) We take the following as an axiom:
∀alpha beta gamma, ordinal alpha → ordinal beta → ordinal gamma → ∀p q r : set → prop, PNoLt alpha p beta q → PNoLe beta q gamma r → PNoLt alpha p gamma r
In Proofgold the corresponding term root is 156586... and proposition id is 09246b...
Axiom. (PNoLeLt_tra) We take the following as an axiom:
∀alpha beta gamma, ordinal alpha → ordinal beta → ordinal gamma → ∀p q r : set → prop, PNoLe alpha p beta q → PNoLt beta q gamma r → PNoLt alpha p gamma r
In Proofgold the corresponding term root is a260ca... and proposition id is ad6971...
Axiom. (PNoEqLe_tra) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → ∀p q r : set → prop, PNoEq_ alpha p q → PNoLe alpha q beta r → PNoLe alpha p beta r
In Proofgold the corresponding term root is 7d3ff8... and proposition id is 002ebf...
Axiom. (PNoLe_tra) We take the following as an axiom:
∀alpha beta gamma, ordinal alpha → ordinal beta → ordinal gamma → ∀p q r : set → prop, PNoLe alpha p beta q → PNoLe beta q gamma r → PNoLe alpha p gamma r
In Proofgold the corresponding term root is 70b92b... and proposition id is 4b557d...
Definition. We define PNo_downc to be λL alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop, L beta q ∧ PNoLe alpha p beta q of type (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 93dab1... and object id is f6c962...
Definition. We define PNo_upc to be λR alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop, R beta q ∧ PNoLe beta q alpha p of type (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 543712... and object id is b97935...
Axiom. (PNoLe_downc) We take the following as an axiom:
∀L : set → (set → prop) → prop, ∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PNo_downc L alpha p → PNoLe beta q alpha p → PNo_downc L beta q
In Proofgold the corresponding term root is 6b1f0d... and proposition id is cd130e...
Axiom. (PNo_downc_ref) We take the following as an axiom:
∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, L alpha p → PNo_downc L alpha p
In Proofgold the corresponding term root is 347aa9... and proposition id is 69dfcb...
Axiom. (PNo_upc_ref) We take the following as an axiom:
∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, R alpha p → PNo_upc R alpha p
In Proofgold the corresponding term root is 403942... and proposition id is c4bf71...
Axiom. (PNoLe_upc) We take the following as an axiom:
∀R : set → (set → prop) → prop, ∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PNo_upc R alpha p → PNoLe alpha p beta q → PNo_upc R beta q
In Proofgold the corresponding term root is 111b74... and proposition id is eb9ed5...
Definition. We define PNoLt_pwise to be λL R ⇒ ∀gamma, ordinal gamma → ∀p : set → prop, L gamma p → ∀delta, ordinal delta → ∀q : set → prop, R delta q → PNoLt gamma p delta q of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → prop.
In Proofgold the corresponding term root is ae448b... and object id is 123808...
Axiom. (PNoLt_pwise_downc_upc) We take the following as an axiom:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → PNoLt_pwise (PNo_downc L) (PNo_upc R)
In Proofgold the corresponding term root is 2b8e3b... and proposition id is 2f244c...
Definition. We define PNo_rel_strict_upperbd to be λL alpha p ⇒ ∀beta ∈ alpha, ∀q : set → prop, PNo_downc L beta q → PNoLt beta q alpha p of type (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is dc1665... and object id is 3e1663...
Definition. We define PNo_rel_strict_lowerbd to be λR alpha p ⇒ ∀beta ∈ alpha, ∀q : set → prop, PNo_upc R beta q → PNoLt alpha p beta q of type (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is e5a4b6... and object id is ff3150...
Definition. We define PNo_rel_strict_imv to be λL R alpha p ⇒ PNo_rel_strict_upperbd L alpha p ∧ PNo_rel_strict_lowerbd R alpha p of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 64ce99... and object id is 5b35fb...
Axiom. (PNoEq_rel_strict_upperbd) We take the following as an axiom:
∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_rel_strict_upperbd L alpha p → PNo_rel_strict_upperbd L alpha q
In Proofgold the corresponding term root is bb65cf... and proposition id is db4b82...
Axiom. (PNo_rel_strict_upperbd_antimon) We take the following as an axiom:
∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, ∀beta ∈ alpha, PNo_rel_strict_upperbd L alpha p → PNo_rel_strict_upperbd L beta p
In Proofgold the corresponding term root is 9986af... and proposition id is ed53da...
Axiom. (PNoEq_rel_strict_lowerbd) We take the following as an axiom:
∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_rel_strict_lowerbd R alpha p → PNo_rel_strict_lowerbd R alpha q
In Proofgold the corresponding term root is 76080e... and proposition id is 614e58...
Axiom. (PNo_rel_strict_lowerbd_antimon) We take the following as an axiom:
∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, ∀beta ∈ alpha, PNo_rel_strict_lowerbd R alpha p → PNo_rel_strict_lowerbd R beta p
In Proofgold the corresponding term root is 27f253... and proposition id is 344b63...
Axiom. (PNoEq_rel_strict_imv) We take the following as an axiom:
∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_rel_strict_imv L R alpha p → PNo_rel_strict_imv L R alpha q
In Proofgold the corresponding term root is e3f251... and proposition id is 7ae13d...
Axiom. (PNo_rel_strict_imv_antimon) We take the following as an axiom:
∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, ∀beta ∈ alpha, PNo_rel_strict_imv L R alpha p → PNo_rel_strict_imv L R beta p
In Proofgold the corresponding term root is 2434dc... and proposition id is 87e0ce...
Definition. We define PNo_rel_strict_uniq_imv to be λL R alpha p ⇒ PNo_rel_strict_imv L R alpha p ∧ ∀q : set → prop, PNo_rel_strict_imv L R alpha q → PNoEq_ alpha p q of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 23c9d9... and object id is 56ed1b...
Definition. We define PNo_rel_strict_split_imv to be λL R alpha p ⇒ PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∧ delta ≠ alpha) ∧ PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∨ delta = alpha) of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 217d17... and object id is dd9cee...
Axiom. (PNo_extend0_eq) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta ∧ delta ≠ alpha)
In Proofgold the corresponding term root is 2d441e... and proposition id is 5ed08e...
Axiom. (PNo_extend1_eq) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta ∨ delta = alpha)
In Proofgold the corresponding term root is 8eb99c... and proposition id is 4cac1a...
Axiom. (PNo_rel_imv_ex) We take the following as an axiom:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → (∃p : set → prop, PNo_rel_strict_uniq_imv L R alpha p) ∨ (∃tau ∈ alpha, ∃p : set → prop, PNo_rel_strict_split_imv L R tau p)
In Proofgold the corresponding term root is 3e3224... and proposition id is 749b63...
Definition. We define PNo_lenbdd to be λalpha L ⇒ ∀beta, ∀p : set → prop, L beta p → beta ∈ alpha of type set → (set → (set → prop) → prop) → prop.
In Proofgold the corresponding term root is 009fa7... and object id is a452a6...
Axiom. (PNo_lenbdd_strict_imv_extend0) We take the following as an axiom:
∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∀p : set → prop, PNo_rel_strict_imv L R alpha p → PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∧ delta ≠ alpha)
In Proofgold the corresponding term root is 17a114... and proposition id is 69327e...
Axiom. (PNo_lenbdd_strict_imv_extend1) We take the following as an axiom:
∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∀p : set → prop, PNo_rel_strict_imv L R alpha p → PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∨ delta = alpha)
In Proofgold the corresponding term root is ad69ec... and proposition id is 5ff993...
Axiom. (PNo_lenbdd_strict_imv_split) We take the following as an axiom:
∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∀p : set → prop, PNo_rel_strict_imv L R alpha p → PNo_rel_strict_split_imv L R alpha p
In Proofgold the corresponding term root is 76ae4f... and proposition id is f98998...
Axiom. (PNo_rel_imv_bdd_ex) We take the following as an axiom:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∃beta ∈ ordsucc alpha, ∃p : set → prop, PNo_rel_strict_split_imv L R beta p
In Proofgold the corresponding term root is 9a98e4... and proposition id is 25bcd2...
Definition. We define PNo_strict_upperbd to be λL alpha p ⇒ ∀beta, ordinal beta → ∀q : set → prop, L beta q → PNoLt beta q alpha p of type (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 6913bd... and object id is 3723ab...
Definition. We define PNo_strict_lowerbd to be λR alpha p ⇒ ∀beta, ordinal beta → ∀q : set → prop, R beta q → PNoLt alpha p beta q of type (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 87fac4... and object id is 3606d4...
Definition. We define PNo_strict_imv to be λL R alpha p ⇒ PNo_strict_upperbd L alpha p ∧ PNo_strict_lowerbd R alpha p of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is ee97f6... and object id is bc6c55...
Axiom. (PNoEq_strict_upperbd) We take the following as an axiom:
∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_strict_upperbd L alpha p → PNo_strict_upperbd L alpha q
In Proofgold the corresponding term root is 9b7b8e... and proposition id is f28b04...
Axiom. (PNoEq_strict_lowerbd) We take the following as an axiom:
∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_strict_lowerbd R alpha p → PNo_strict_lowerbd R alpha q
In Proofgold the corresponding term root is 4db3f9... and proposition id is 67fa73...
Axiom. (PNoEq_strict_imv) We take the following as an axiom:
∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_strict_imv L R alpha p → PNo_strict_imv L R alpha q
In Proofgold the corresponding term root is 1ec352... and proposition id is 5f582f...
Axiom. (PNo_strict_upperbd_imp_rel_strict_upperbd) We take the following as an axiom:
∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀beta ∈ ordsucc alpha, ∀p : set → prop, PNo_strict_upperbd L alpha p → PNo_rel_strict_upperbd L beta p
In Proofgold the corresponding term root is 2898f0... and proposition id is 3cdd3b...
Axiom. (PNo_strict_lowerbd_imp_rel_strict_lowerbd) We take the following as an axiom:
∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀beta ∈ ordsucc alpha, ∀p : set → prop, PNo_strict_lowerbd R alpha p → PNo_rel_strict_lowerbd R beta p
In Proofgold the corresponding term root is 442af5... and proposition id is 04acc2...
Axiom. (PNo_strict_imv_imp_rel_strict_imv) We take the following as an axiom:
∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀beta ∈ ordsucc alpha, ∀p : set → prop, PNo_strict_imv L R alpha p → PNo_rel_strict_imv L R beta p
In Proofgold the corresponding term root is f4fc71... and proposition id is 46a6aa...
Axiom. (PNo_rel_split_imv_imp_strict_imv) We take the following as an axiom:
∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, PNo_rel_strict_split_imv L R alpha p → PNo_strict_imv L R alpha p
In Proofgold the corresponding term root is 72be36... and proposition id is adfdb0...
Axiom. (PNo_lenbdd_strict_imv_ex) We take the following as an axiom:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∃beta ∈ ordsucc alpha, ∃p : set → prop, PNo_strict_imv L R beta p
In Proofgold the corresponding term root is 9485d6... and proposition id is a864a5...
Definition. We define PNo_least_rep to be λL R beta p ⇒ ordinal beta ∧ PNo_strict_imv L R beta p ∧ ∀gamma ∈ beta, ∀q : set → prop, ¬ PNo_strict_imv L R gamma q of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 0711e2... and object id is e4c707...
Definition. We define PNo_least_rep2 to be λL R beta p ⇒ PNo_least_rep L R beta p ∧ ∀x, x ∉ beta → ¬ p x of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 1f6dc5... and object id is 09d320...
Axiom. (PNo_strict_imv_pred_eq) We take the following as an axiom:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → ∀p q : set → prop, PNo_least_rep L R alpha p → PNo_strict_imv L R alpha q → ∀beta ∈ alpha, p beta ↔ q beta
In Proofgold the corresponding term root is 5e7822... and proposition id is 72e14d...
Axiom. (PNo_lenbdd_least_rep2_exuniq2) We take the following as an axiom:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∃beta, (∃p : set → prop, PNo_least_rep2 L R beta p) ∧ (∀p q : set → prop, PNo_least_rep2 L R beta p → PNo_least_rep2 L R beta q → p = q)
In Proofgold the corresponding term root is 5060a9... and proposition id is 8b62c5...
Definition. We define PNo_bd to be λL R ⇒ DescrR_i_io_1 (PNo_least_rep2 L R) of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set.
In Proofgold the corresponding term root is ed76e7... and object id is aa75ef...
Definition. We define PNo_pred to be λL R ⇒ DescrR_i_io_2 (PNo_least_rep2 L R) of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → prop.
In Proofgold the corresponding term root is b2d51d... and object id is 2efd18...
Axiom. (PNo_bd_pred_lem) We take the following as an axiom:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → PNo_least_rep2 L R (PNo_bd L R) (PNo_pred L R)
In Proofgold the corresponding term root is 749b8f... and proposition id is 5de4a3...
Axiom. (PNo_bd_pred) We take the following as an axiom:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → PNo_least_rep L R (PNo_bd L R) (PNo_pred L R)
In Proofgold the corresponding term root is 42224b... and proposition id is 3309f6...
Axiom. (PNo_bd_In) We take the following as an axiom:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → PNo_bd L R ∈ ordsucc alpha
In Proofgold the corresponding term root is ad857b... and proposition id is 4719e1...
Beginning of Section TaggedSets
Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
Axiom. (not_TransSet_Sing1) We take the following as an axiom:
¬ TransSet {1}
In Proofgold the corresponding term root is 8f2d67... and proposition id is be9a70...
Axiom. (not_ordinal_Sing1) We take the following as an axiom:
¬ ordinal {1}
In Proofgold the corresponding term root is 99a3f6... and proposition id is db7977...
Axiom. (tagged_not_ordinal) We take the following as an axiom:
∀y, ¬ ordinal (y ')
In Proofgold the corresponding term root is f9488c... and proposition id is aaf6e4...
Axiom. (tagged_notin_ordinal) We take the following as an axiom:
∀alpha y, ordinal alpha → (y ') ∉ alpha
In Proofgold the corresponding term root is b603ba... and proposition id is c0e2c3...
Axiom. (tagged_eqE_Subq) We take the following as an axiom:
∀alpha beta, ordinal alpha → alpha ' = beta ' → alpha ⊆ beta
In Proofgold the corresponding term root is cf032f... and proposition id is ef37f5...
Axiom. (tagged_eqE_eq) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha ' = beta ' → alpha = beta
In Proofgold the corresponding term root is 1f7dc9... and proposition id is ec1608...
Axiom. (tagged_ReplE) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → beta ' ∈ {gamma '|gamma ∈ alpha} → beta ∈ alpha
In Proofgold the corresponding term root is a1d43c... and proposition id is 70c250...
Axiom. (ordinal_notin_tagged_Repl) We take the following as an axiom:
∀alpha Y, ordinal alpha → alpha ∉ {y '|y ∈ Y}
In Proofgold the corresponding term root is 7f35b5... and proposition id is e7ff3b...
Definition. We define SNoElts_ to be λalpha ⇒ alpha ∪ {beta '|beta ∈ alpha} of type set → set.
In Proofgold the corresponding term root is c0ec73... and object id is 6f0c36...
Axiom. (SNoElts_mon) We take the following as an axiom:
∀alpha beta, alpha ⊆ beta → SNoElts_ alpha ⊆ SNoElts_ beta
In Proofgold the corresponding term root is 49a08e... and proposition id is 859611...
Definition. We define SNo_ to be λalpha x ⇒ x ⊆ SNoElts_ alpha ∧ ∀beta ∈ alpha, exactly1of2 (beta ' ∈ x) (beta ∈ x) of type set → set → prop.
In Proofgold the corresponding term root is 4ab7e4... and object id is c16a73...
Definition. We define PSNo to be λalpha p ⇒ {beta ∈ alpha|p beta} ∪ {beta '|beta ∈ alpha, ¬ p beta} of type set → (set → prop) → set.
In Proofgold the corresponding term root is 3657ae... and object id is 0a8351...
Axiom. (PNoEq_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha → ∀p : set → prop, PNoEq_ alpha (λbeta ⇒ beta ∈ PSNo alpha p) p
In Proofgold the corresponding term root is c12e02... and proposition id is 688518...
Axiom. (SNo_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha → ∀p : set → prop, SNo_ alpha (PSNo alpha p)
In Proofgold the corresponding term root is 96e4e2... and proposition id is f03db0...
Axiom. (SNo_PSNo_eta_) We take the following as an axiom:
∀alpha x, ordinal alpha → SNo_ alpha x → x = PSNo alpha (λbeta ⇒ beta ∈ x)
In Proofgold the corresponding term root is 1642af... and proposition id is 630119...
Definition. We define SNo to be λx ⇒ ∃alpha, ordinal alpha ∧ SNo_ alpha x of type set → prop.
In Proofgold the corresponding term root is 11faa7... and object id is 116b76...
Axiom. (SNo_SNo) We take the following as an axiom:
∀alpha, ordinal alpha → ∀z, SNo_ alpha z → SNo z
In Proofgold the corresponding term root is 929b7a... and proposition id is a59341...
Definition. We define SNoLev to be λx ⇒ Eps_i (λalpha ⇒ ordinal alpha ∧ SNo_ alpha x) of type set → set.
In Proofgold the corresponding term root is 293b77... and object id is 83dce3...
Axiom. (SNoLev_uniq_Subq) We take the following as an axiom:
∀x alpha beta, ordinal alpha → ordinal beta → SNo_ alpha x → SNo_ beta x → alpha ⊆ beta
In Proofgold the corresponding term root is 2ca114... and proposition id is 65843d...
Axiom. (SNoLev_uniq) We take the following as an axiom:
∀x alpha beta, ordinal alpha → ordinal beta → SNo_ alpha x → SNo_ beta x → alpha = beta
In Proofgold the corresponding term root is 68f71d... and proposition id is 5d96d4...
Axiom. (SNoLev_prop) We take the following as an axiom:
∀x, SNo x → ordinal (SNoLev x) ∧ SNo_ (SNoLev x) x
In Proofgold the corresponding term root is a8afcc... and proposition id is 21761c...
Axiom. (SNoLev_ordinal) We take the following as an axiom:
∀x, SNo x → ordinal (SNoLev x)
In Proofgold the corresponding term root is 7cacc5... and proposition id is f0e9f7...
Axiom. (SNoLev_) We take the following as an axiom:
∀x, SNo x → SNo_ (SNoLev x) x
In Proofgold the corresponding term root is 4a1033... and proposition id is 49cd5a...
Axiom. (SNo_PSNo_eta) We take the following as an axiom:
∀x, SNo x → x = PSNo (SNoLev x) (λbeta ⇒ beta ∈ x)
In Proofgold the corresponding term root is 6ffefe... and proposition id is 8c7870...
Axiom. (SNoLev_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha → ∀p : set → prop, SNoLev (PSNo alpha p) = alpha
In Proofgold the corresponding term root is 07f1eb... and proposition id is 9c4890...
Axiom. (SNo_Subq) We take the following as an axiom:
∀x y, SNo x → SNo y → SNoLev x ⊆ SNoLev y → (∀alpha ∈ SNoLev x, alpha ∈ x ↔ alpha ∈ y) → x ⊆ y
In Proofgold the corresponding term root is a244d7... and proposition id is a428af...
Definition. We define SNoEq_ to be λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ y) of type set → set → set → prop.
In Proofgold the corresponding term root is 5f11e2... and object id is 12b5f6...
Axiom. (SNoEq_I) We take the following as an axiom:
∀alpha x y, (∀beta ∈ alpha, beta ∈ x ↔ beta ∈ y) → SNoEq_ alpha x y
In Proofgold the corresponding term root is a718b1... and proposition id is fdcb78...
Axiom. (SNo_eq) We take the following as an axiom:
∀x y, SNo x → SNo y → SNoLev x = SNoLev y → SNoEq_ (SNoLev x) x y → x = y
In Proofgold the corresponding term root is b08bdc... and proposition id is bf4ac3...
End of Section TaggedSets
Definition. We define SNoLt to be λx y ⇒ PNoLt (SNoLev x) (λbeta ⇒ beta ∈ x) (SNoLev y) (λbeta ⇒ beta ∈ y) of type set → set → prop.
In Proofgold the corresponding term root is 46e7ed... and object id is 8c8aa9...
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Definition. We define SNoLe to be λx y ⇒ PNoLe (SNoLev x) (λbeta ⇒ beta ∈ x) (SNoLev y) (λbeta ⇒ beta ∈ y) of type set → set → prop.
In Proofgold the corresponding term root is ddf7d3... and object id is 54f405...
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Axiom. (SNoLtLe) We take the following as an axiom:
∀x y, x < y → x ≤ y
In Proofgold the corresponding term root is c0fef1... and proposition id is f09833...
Axiom. (SNoLeE) We take the following as an axiom:
∀x y, SNo x → SNo y → x ≤ y → x < y ∨ x = y
In Proofgold the corresponding term root is 1c9c62... and proposition id is 23cc47...
Axiom. (SNoEq_sym_) We take the following as an axiom:
∀alpha x y, SNoEq_ alpha x y → SNoEq_ alpha y x
In Proofgold the corresponding term root is f8c61d... and proposition id is f756d2...
Axiom. (SNoEq_tra_) We take the following as an axiom:
∀alpha x y z, SNoEq_ alpha x y → SNoEq_ alpha y z → SNoEq_ alpha x z
In Proofgold the corresponding term root is 0fff96... and proposition id is 246d04...
Axiom. (SNoLtE) We take the following as an axiom:
∀x y, SNo x → SNo y → x < y → ∀p : prop, (∀z, SNo z → SNoLev z ∈ SNoLev x ∩ SNoLev y → SNoEq_ (SNoLev z) z x → SNoEq_ (SNoLev z) z y → x < z → z < y → SNoLev z ∉ x → SNoLev z ∈ y → p) → (SNoLev x ∈ SNoLev y → SNoEq_ (SNoLev x) x y → SNoLev x ∈ y → p) → (SNoLev y ∈ SNoLev x → SNoEq_ (SNoLev y) x y → SNoLev y ∉ x → p) → p
In Proofgold the corresponding term root is 958711... and proposition id is d12fc6...
Axiom. (SNoLtI2) We take the following as an axiom:
∀x y, SNoLev x ∈ SNoLev y → SNoEq_ (SNoLev x) x y → SNoLev x ∈ y → x < y
In Proofgold the corresponding term root is 282b01... and proposition id is 82b82c...
Axiom. (SNoLtI3) We take the following as an axiom:
∀x y, SNoLev y ∈ SNoLev x → SNoEq_ (SNoLev y) x y → SNoLev y ∉ x → x < y
In Proofgold the corresponding term root is 006afc... and proposition id is 938f67...
Axiom. (SNoLt_irref) We take the following as an axiom:
∀x, ¬ SNoLt x x
In Proofgold the corresponding term root is d5ecf9... and proposition id is 06fac5...
Axiom. (SNoLt_trichotomy_or) We take the following as an axiom:
∀x y, SNo x → SNo y → x < y ∨ x = y ∨ y < x
In Proofgold the corresponding term root is 35a4c8... and proposition id is 8ad056...
Axiom. (SNoLt_trichotomy_or_impred) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀p : prop, (x < y → p) → (x = y → p) → (y < x → p) → p
In Proofgold the corresponding term root is ba04ef... and proposition id is 7588e3...
Axiom. (SNoLt_tra) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x < y → y < z → x < z
In Proofgold the corresponding term root is ac0e24... and proposition id is ccfdf7...
Axiom. (SNoLe_ref) We take the following as an axiom:
∀x, SNoLe x x
In Proofgold the corresponding term root is c940c8... and proposition id is 83bd2d...
Axiom. (SNoLe_antisym) We take the following as an axiom:
∀x y, SNo x → SNo y → x ≤ y → y ≤ x → x = y
In Proofgold the corresponding term root is f9f757... and proposition id is 3abee4...
Axiom. (SNoLtLe_tra) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x < y → y ≤ z → x < z
In Proofgold the corresponding term root is 3bc661... and proposition id is ba8545...
Axiom. (SNoLeLt_tra) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x ≤ y → y < z → x < z
In Proofgold the corresponding term root is b2178f... and proposition id is 4a77a2...
Axiom. (SNoLe_tra) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x ≤ y → y ≤ z → x ≤ z
In Proofgold the corresponding term root is a0c5c6... and proposition id is 031989...
Axiom. (SNoLtLe_or) We take the following as an axiom:
∀x y, SNo x → SNo y → x < y ∨ y ≤ x
In Proofgold the corresponding term root is f595ac... and proposition id is 8965d2...
Axiom. (SNoLt_PSNo_PNoLt) We take the following as an axiom:
∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PSNo alpha p < PSNo beta q → PNoLt alpha p beta q
In Proofgold the corresponding term root is 6e122d... and proposition id is 535161...
Axiom. (PNoLt_SNoLt_PSNo) We take the following as an axiom:
∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PNoLt alpha p beta q → PSNo alpha p < PSNo beta q
In Proofgold the corresponding term root is 11b6ed... and proposition id is 6196d9...
Definition. We define SNoCut to be λL R ⇒ PSNo (PNo_bd (λalpha p ⇒ ordinal alpha ∧ PSNo alpha p ∈ L) (λalpha p ⇒ ordinal alpha ∧ PSNo alpha p ∈ R)) (PNo_pred (λalpha p ⇒ ordinal alpha ∧ PSNo alpha p ∈ L) (λalpha p ⇒ ordinal alpha ∧ PSNo alpha p ∈ R)) of type set → set → set.
In Proofgold the corresponding term root is ec849e... and object id is 295bc4...
Definition. We define SNoCutP to be λL R ⇒ (∀x ∈ L, SNo x) ∧ (∀y ∈ R, SNo y) ∧ (∀x ∈ L, ∀y ∈ R, x < y) of type set → set → prop.
In Proofgold the corresponding term root is c083d8... and object id is 775127...
Axiom. (SNoCutP_SNoCut) We take the following as an axiom:
∀L R, SNoCutP L R → SNo (SNoCut L R) ∧ SNoLev (SNoCut L R) ∈ ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))) ∧ (∀x ∈ L, x < SNoCut L R) ∧ (∀y ∈ R, SNoCut L R < y) ∧ (∀z, SNo z → (∀x ∈ L, x < z) → (∀y ∈ R, z < y) → SNoLev (SNoCut L R) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z)
In Proofgold the corresponding term root is 9398b7... and proposition id is 66456c...
Axiom. (SNoCutP_SNoCut_impred) We take the following as an axiom:
∀L R, SNoCutP L R → ∀p : prop, (SNo (SNoCut L R) → SNoLev (SNoCut L R) ∈ ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))) → (∀x ∈ L, x < SNoCut L R) → (∀y ∈ R, SNoCut L R < y) → (∀z, SNo z → (∀x ∈ L, x < z) → (∀y ∈ R, z < y) → SNoLev (SNoCut L R) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z) → p) → p
In Proofgold the corresponding term root is 02c4ae... and proposition id is 5bcc8f...
Axiom. (SNoCutP_L_0) We take the following as an axiom:
∀L, (∀x ∈ L, SNo x) → SNoCutP L 0
In Proofgold the corresponding term root is 47329c... and proposition id is ba61e1...
Axiom. (SNoCutP_0_0) We take the following as an axiom:
SNoCutP 0 0
In Proofgold the corresponding term root is 3b144e... and proposition id is a5144d...
Definition. We define SNoS_ to be λalpha ⇒ {x ∈ 𝒫 (SNoElts_ alpha)|∃beta ∈ alpha, SNo_ beta x} of type set → set.
In Proofgold the corresponding term root is d5069a... and object id is 4680ce...
Axiom. (SNoS_E) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, ∃beta ∈ alpha, SNo_ beta x
In Proofgold the corresponding term root is 970ce2... and proposition id is bb731c...
Beginning of Section TaggedSets2
Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
Axiom. (SNoS_I) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x, ∀beta ∈ alpha, SNo_ beta x → x ∈ SNoS_ alpha
In Proofgold the corresponding term root is f5227d... and proposition id is 04f24b...
Axiom. (SNoS_I2) We take the following as an axiom:
∀x y, SNo x → SNo y → SNoLev x ∈ SNoLev y → x ∈ SNoS_ (SNoLev y)
In Proofgold the corresponding term root is 7a14c7... and proposition id is b4042d...
Axiom. (SNoS_Subq) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta → SNoS_ alpha ⊆ SNoS_ beta
In Proofgold the corresponding term root is 6828e7... and proposition id is d928b8...
Axiom. (SNoLev_uniq2) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x, SNo_ alpha x → SNoLev x = alpha
In Proofgold the corresponding term root is fbb461... and proposition id is f48d47...
Axiom. (SNoS_E2) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, ∀p : prop, (SNoLev x ∈ alpha → ordinal (SNoLev x) → SNo x → SNo_ (SNoLev x) x → p) → p
In Proofgold the corresponding term root is deb031... and proposition id is 62b490...
Axiom. (SNoS_In_neq) We take the following as an axiom:
∀w, SNo w → ∀x ∈ SNoS_ (SNoLev w), x ≠ w
In Proofgold the corresponding term root is ab85fd... and proposition id is d5dbd7...
Axiom. (SNoS_SNoLev) We take the following as an axiom:
∀z, SNo z → z ∈ SNoS_ (ordsucc (SNoLev z))
In Proofgold the corresponding term root is a9ba1f... and proposition id is 8efb88...
Definition. We define SNoL to be λz ⇒ {x ∈ SNoS_ (SNoLev z)|x < z} of type set → set.
In Proofgold the corresponding term root is 8cd812... and object id is 48bcf8...
Definition. We define SNoR to be λz ⇒ {y ∈ SNoS_ (SNoLev z)|z < y} of type set → set.
In Proofgold the corresponding term root is 73b2b9... and object id is 0cfe87...
Axiom. (SNoCutP_SNoL_SNoR) We take the following as an axiom:
∀z, SNo z → SNoCutP (SNoL z) (SNoR z)
In Proofgold the corresponding term root is 524866... and proposition id is 7aba57...
Axiom. (SNoL_E) We take the following as an axiom:
∀x, SNo x → ∀w ∈ SNoL x, ∀p : prop, (SNo w → SNoLev w ∈ SNoLev x → w < x → p) → p
In Proofgold the corresponding term root is cead4f... and proposition id is 7ccd8b...
Axiom. (SNoR_E) We take the following as an axiom:
∀x, SNo x → ∀z ∈ SNoR x, ∀p : prop, (SNo z → SNoLev z ∈ SNoLev x → x < z → p) → p
In Proofgold the corresponding term root is efca05... and proposition id is 7dca04...
Axiom. (SNoL_SNoS_) We take the following as an axiom:
∀z, SNoL z ⊆ SNoS_ (SNoLev z)
In Proofgold the corresponding term root is 73f5b2... and proposition id is 409713...
Axiom. (SNoR_SNoS_) We take the following as an axiom:
∀z, SNoR z ⊆ SNoS_ (SNoLev z)
In Proofgold the corresponding term root is 16bdfc... and proposition id is 2fe1c0...
Axiom. (SNoL_SNoS) We take the following as an axiom:
∀x, SNo x → ∀w ∈ SNoL x, w ∈ SNoS_ (SNoLev x)
In Proofgold the corresponding term root is 6e3a22... and proposition id is ded78a...
Axiom. (SNoR_SNoS) We take the following as an axiom:
∀x, SNo x → ∀z ∈ SNoR x, z ∈ SNoS_ (SNoLev x)
In Proofgold the corresponding term root is 98051c... and proposition id is e13f49...
Axiom. (SNoL_I) We take the following as an axiom:
∀z, SNo z → ∀x, SNo x → SNoLev x ∈ SNoLev z → x < z → x ∈ SNoL z
In Proofgold the corresponding term root is ddd91b... and proposition id is 4f3d04...
Axiom. (SNoR_I) We take the following as an axiom:
∀z, SNo z → ∀y, SNo y → SNoLev y ∈ SNoLev z → z < y → y ∈ SNoR z
In Proofgold the corresponding term root is 97693c... and proposition id is 383e88...
Axiom. (SNo_eta) We take the following as an axiom:
∀z, SNo z → z = SNoCut (SNoL z) (SNoR z)
In Proofgold the corresponding term root is 3cc369... and proposition id is dc9273...
Axiom. (SNoCutP_SNo_SNoCut) We take the following as an axiom:
∀L R, SNoCutP L R → SNo (SNoCut L R)
In Proofgold the corresponding term root is 9621aa... and proposition id is ae46e8...
Axiom. (SNoCutP_SNoCut_L) We take the following as an axiom:
∀L R, SNoCutP L R → ∀x ∈ L, x < SNoCut L R
In Proofgold the corresponding term root is 984a30... and proposition id is 4bca14...
Axiom. (SNoCutP_SNoCut_R) We take the following as an axiom:
∀L R, SNoCutP L R → ∀y ∈ R, SNoCut L R < y
In Proofgold the corresponding term root is 9161db... and proposition id is 7c3d12...
Axiom. (SNoCutP_SNoCut_fst) We take the following as an axiom:
∀L R, SNoCutP L R → ∀z, SNo z → (∀x ∈ L, x < z) → (∀y ∈ R, z < y) → SNoLev (SNoCut L R) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z
In Proofgold the corresponding term root is b52eb7... and proposition id is 8362f8...
Axiom. (SNoCut_Le) We take the following as an axiom:
∀L1 R1 L2 R2, SNoCutP L1 R1 → SNoCutP L2 R2 → (∀w ∈ L1, w < SNoCut L2 R2) → (∀z ∈ R2, SNoCut L1 R1 < z) → SNoCut L1 R1 ≤ SNoCut L2 R2
In Proofgold the corresponding term root is bb8cdc... and proposition id is 423731...
Axiom. (SNoCut_ext) We take the following as an axiom:
∀L1 R1 L2 R2, SNoCutP L1 R1 → SNoCutP L2 R2 → (∀w ∈ L1, w < SNoCut L2 R2) → (∀z ∈ R1, SNoCut L2 R2 < z) → (∀w ∈ L2, w < SNoCut L1 R1) → (∀z ∈ R2, SNoCut L1 R1 < z) → SNoCut L1 R1 = SNoCut L2 R2
In Proofgold the corresponding term root is c1078e... and proposition id is f66618...
Axiom. (SNoLt_SNoL_or_SNoR_impred) We take the following as an axiom:
∀x y, SNo x → SNo y → x < y → ∀p : prop, (∀z ∈ SNoL y, z ∈ SNoR x → p) → (x ∈ SNoL y → p) → (y ∈ SNoR x → p) → p
In Proofgold the corresponding term root is f3b15a... and proposition id is ffc0bf...
Axiom. (SNoL_or_SNoR_impred) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀p : prop, (x = y → p) → (∀z ∈ SNoL y, z ∈ SNoR x → p) → (x ∈ SNoL y → p) → (y ∈ SNoR x → p) → (∀z ∈ SNoR y, z ∈ SNoL x → p) → (x ∈ SNoR y → p) → (y ∈ SNoL x → p) → p
In Proofgold the corresponding term root is f8a5e2... and proposition id is 68ba98...
Axiom. (SNoL_SNoCutP_ex) We take the following as an axiom:
∀L R, SNoCutP L R → ∀w ∈ SNoL (SNoCut L R), ∃w' ∈ L, w ≤ w'
In Proofgold the corresponding term root is 3b4695... and proposition id is 6d8af6...
Axiom. (SNoR_SNoCutP_ex) We take the following as an axiom:
∀L R, SNoCutP L R → ∀z ∈ SNoR (SNoCut L R), ∃z' ∈ R, z' ≤ z
In Proofgold the corresponding term root is ca7be2... and proposition id is bb0b53...
Axiom. (ordinal_SNo_) We take the following as an axiom:
∀alpha, ordinal alpha → SNo_ alpha alpha
In Proofgold the corresponding term root is 4731fd... and proposition id is 7754e5...
Axiom. (ordinal_SNo) We take the following as an axiom:
∀alpha, ordinal alpha → SNo alpha
In Proofgold the corresponding term root is ac39bc... and proposition id is 1eea33...
Axiom. (ordinal_SNoLev) We take the following as an axiom:
∀alpha, ordinal alpha → SNoLev alpha = alpha
In Proofgold the corresponding term root is 56f8b0... and proposition id is fea5fc...
Axiom. (ordinal_SNoLev_max) We take the following as an axiom:
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ alpha → z < alpha
In Proofgold the corresponding term root is 945794... and proposition id is 51ee47...
Axiom. (ordinal_SNoL) We take the following as an axiom:
∀alpha, ordinal alpha → SNoL alpha = SNoS_ alpha
In Proofgold the corresponding term root is fef608... and proposition id is 95823e...
Axiom. (ordinal_SNoR) We take the following as an axiom:
∀alpha, ordinal alpha → SNoR alpha = Empty
In Proofgold the corresponding term root is 07c69a... and proposition id is f853d9...
Axiom. (nat_p_SNo) We take the following as an axiom:
∀n, nat_p n → SNo n
In Proofgold the corresponding term root is 0644f3... and proposition id is 5fd930...
Axiom. (omega_SNo) We take the following as an axiom:
∀n ∈ ω, SNo n
In Proofgold the corresponding term root is d32269... and proposition id is d0f9c6...
Axiom. (omega_SNoS_omega) We take the following as an axiom:
ω ⊆ SNoS_ ω
In Proofgold the corresponding term root is 4ba265... and proposition id is 2ccf7a...
Axiom. (ordinal_In_SNoLt) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta ∈ alpha, beta < alpha
In Proofgold the corresponding term root is e37d00... and proposition id is ced78e...
Axiom. (ordinal_SNoLev_max_2) We take the following as an axiom:
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ ordsucc alpha → z ≤ alpha
In Proofgold the corresponding term root is 72c5eb... and proposition id is c9a731...
Axiom. (ordinal_Subq_SNoLe) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta → alpha ≤ beta
In Proofgold the corresponding term root is 7558ba... and proposition id is 15c58a...
Axiom. (ordinal_SNoLt_In) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha < beta → alpha ∈ beta
In Proofgold the corresponding term root is d6f066... and proposition id is de775b...
Axiom. (omega_nonneg) We take the following as an axiom:
∀m ∈ ω, 0 ≤ m
In Proofgold the corresponding term root is ee67c9... and proposition id is eaf06b...
Axiom. (SNo_0) We take the following as an axiom:
SNo 0
In Proofgold the corresponding term root is c8204b... and proposition id is 94a310...
Axiom. (SNo_1) We take the following as an axiom:
SNo 1
In Proofgold the corresponding term root is ac50d7... and proposition id is 9a733a...
Axiom. (SNo_2) We take the following as an axiom:
SNo 2
In Proofgold the corresponding term root is 487591... and proposition id is c524a4...
Axiom. (SNoLev_0) We take the following as an axiom:
SNoLev 0 = 0
In Proofgold the corresponding term root is 45a0f7... and proposition id is 3527a4...
Axiom. (SNoCut_0_0) We take the following as an axiom:
SNoCut 0 0 = 0
In Proofgold the corresponding term root is 6a1f81... and proposition id is abbffb...
Axiom. (SNoL_0) We take the following as an axiom:
SNoL 0 = 0
In Proofgold the corresponding term root is c01c2b... and proposition id is fdaa69...
Axiom. (SNoR_0) We take the following as an axiom:
SNoR 0 = 0
In Proofgold the corresponding term root is 7329c7... and proposition id is 510751...
Axiom. (SNoL_1) We take the following as an axiom:
SNoL 1 = 1
In Proofgold the corresponding term root is 84d688... and proposition id is 15aa79...
Axiom. (SNoR_1) We take the following as an axiom:
SNoR 1 = 0
In Proofgold the corresponding term root is e6a83a... and proposition id is 8da427...
Axiom. (SNo_max_SNoLev) We take the following as an axiom:
∀x, SNo x → (∀y ∈ SNoS_ (SNoLev x), y < x) → SNoLev x = x
In Proofgold the corresponding term root is ff019e... and proposition id is 3be246...
Axiom. (SNo_max_ordinal) We take the following as an axiom:
∀x, SNo x → (∀y ∈ SNoS_ (SNoLev x), y < x) → ordinal x
In Proofgold the corresponding term root is 0b230c... and proposition id is f28b9a...
Axiom. (pos_low_eq_one) We take the following as an axiom:
∀x, SNo x → 0 < x → SNoLev x ⊆ 1 → x = 1
In Proofgold the corresponding term root is 7c84ef... and proposition id is db40ad...
Definition. We define SNo_extend0 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta ∈ x ∧ delta ≠ SNoLev x) of type set → set.
In Proofgold the corresponding term root is 997d91... and object id is ff4161...
Definition. We define SNo_extend1 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta ∈ x ∨ delta = SNoLev x) of type set → set.
In Proofgold the corresponding term root is 464e47... and object id is 8c551b...
Axiom. (SNo_extend0_SNo_) We take the following as an axiom:
∀x, SNo x → SNo_ (ordsucc (SNoLev x)) (SNo_extend0 x)
In Proofgold the corresponding term root is d41d3e... and proposition id is c8f8ea...
Axiom. (SNo_extend1_SNo_) We take the following as an axiom:
∀x, SNo x → SNo_ (ordsucc (SNoLev x)) (SNo_extend1 x)
In Proofgold the corresponding term root is b7b866... and proposition id is 73bbf2...
Axiom. (SNo_extend0_SNo) We take the following as an axiom:
∀x, SNo x → SNo (SNo_extend0 x)
In Proofgold the corresponding term root is b353a2... and proposition id is 76562c...
Axiom. (SNo_extend1_SNo) We take the following as an axiom:
∀x, SNo x → SNo (SNo_extend1 x)
In Proofgold the corresponding term root is fa323a... and proposition id is 5345a7...
Axiom. (SNo_extend0_SNoLev) We take the following as an axiom:
∀x, SNo x → SNoLev (SNo_extend0 x) = ordsucc (SNoLev x)
In Proofgold the corresponding term root is 26efcd... and proposition id is 5aa0af...
Axiom. (SNo_extend1_SNoLev) We take the following as an axiom:
∀x, SNo x → SNoLev (SNo_extend1 x) = ordsucc (SNoLev x)
In Proofgold the corresponding term root is 33cf60... and proposition id is 529347...
Axiom. (SNo_extend0_nIn) We take the following as an axiom:
∀x, SNo x → SNoLev x ∉ SNo_extend0 x
In Proofgold the corresponding term root is 217cff... and proposition id is 0dfd17...
Axiom. (SNo_extend1_In) We take the following as an axiom:
∀x, SNo x → SNoLev x ∈ SNo_extend1 x
In Proofgold the corresponding term root is ac9570... and proposition id is 8ca372...
Axiom. (SNo_extend0_SNoEq) We take the following as an axiom:
∀x, SNo x → SNoEq_ (SNoLev x) (SNo_extend0 x) x
In Proofgold the corresponding term root is bd4a27... and proposition id is 129986...
Axiom. (SNo_extend1_SNoEq) We take the following as an axiom:
∀x, SNo x → SNoEq_ (SNoLev x) (SNo_extend1 x) x
In Proofgold the corresponding term root is ba974f... and proposition id is d6f8bb...
Axiom. (SNoLev_0_eq_0) We take the following as an axiom:
∀x, SNo x → SNoLev x = 0 → x = 0
In Proofgold the corresponding term root is fe0bc4... and proposition id is dfcf39...
End of Section TaggedSets2
Axiom. (SNo_etaE) We take the following as an axiom:
∀z, SNo z → ∀p : prop, (∀L R, SNoCutP L R → (∀x ∈ L, SNoLev x ∈ SNoLev z) → (∀y ∈ R, SNoLev y ∈ SNoLev z) → z = SNoCut L R → p) → p
In Proofgold the corresponding term root is c24473... and proposition id is 109f1d...
Axiom. (SNo_ind) We take the following as an axiom:
∀P : set → prop, (∀L R, SNoCutP L R → (∀x ∈ L, P x) → (∀y ∈ R, P y) → P (SNoCut L R)) → ∀z, SNo z → P z
In Proofgold the corresponding term root is 5b4c39... and proposition id is 94cbe6...
Beginning of Section SurrealRecI
Variable F : set → (set → set) → set
Let default : set ≝ Eps_i (λ_ ⇒ True)
Let G : set → (set → set → set) → set → set ≝ λalpha g ⇒ If_ii (ordinal alpha) (λz : set ⇒ if z ∈ SNoS_ (ordsucc alpha) then F z (λw ⇒ g (SNoLev w) w) else default) (λz : set ⇒ default)
Definition. We define SNo_rec_i to be λz ⇒ In_rec_ii G (SNoLev z) z of type set → set.
In Proofgold the corresponding term root is be45df... and object id is 230ba8...
Hypothesis Fr : ∀z, SNo z → ∀g h : set → set, (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h
Axiom. (SNo_rec_i_eq) We take the following as an axiom:
∀z, SNo z → SNo_rec_i z = F z SNo_rec_i
In Proofgold the corresponding term root is d5ffa8... and proposition id is f547c8...
End of Section SurrealRecI
Beginning of Section SurrealRecII
Variable F : set → (set → (set → set)) → (set → set)
Let default : (set → set) ≝ Descr_ii (λ_ ⇒ True)
Let G : set → (set → set → (set → set)) → set → (set → set) ≝ λalpha g ⇒ If_iii (ordinal alpha) (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ g (SNoLev w) w)) default) (λz : set ⇒ default)
Definition. We define SNo_rec_ii to be λz ⇒ In_rec_iii G (SNoLev z) z of type set → (set → set).
In Proofgold the corresponding term root is e148e6... and object id is c3f218...
Hypothesis Fr : ∀z, SNo z → ∀g h : set → (set → set), (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h
Axiom. (SNo_rec_ii_eq) We take the following as an axiom:
∀z, SNo z → SNo_rec_ii z = F z SNo_rec_ii
In Proofgold the corresponding term root is 39e866... and proposition id is 1c5373...
End of Section SurrealRecII
Beginning of Section SurrealRec2
Variable F : set → set → (set → set → set) → set
Let G : set → (set → set → set) → set → (set → set) → set ≝ λw f z g ⇒ F w z (λx y ⇒ if x = w then g y else f x y)
Let H : set → (set → set → set) → set → set ≝ λw f z ⇒ if SNo z then SNo_rec_i (G w f) z else Empty
Definition. We define SNo_rec2 to be SNo_rec_ii H of type set → set → set.
In Proofgold the corresponding term root is 7d10ab... and object id is 951110...
Hypothesis Fr : ∀w, SNo w → ∀z, SNo z → ∀g h : set → set → set, (∀x ∈ SNoS_ (SNoLev w), ∀y, SNo y → g x y = h x y) → (∀y ∈ SNoS_ (SNoLev z), g w y = h w y) → F w z g = F w z h
Axiom. (SNo_rec2_G_prop) We take the following as an axiom:
∀w, SNo w → ∀f k : set → set → set, (∀x ∈ SNoS_ (SNoLev w), f x = k x) → ∀z, SNo z → ∀g h : set → set, (∀u ∈ SNoS_ (SNoLev z), g u = h u) → G w f z g = G w k z h
In Proofgold the corresponding term root is 0f875d... and proposition id is de8737...
Axiom. (SNo_rec2_eq_1) We take the following as an axiom:
∀w, SNo w → ∀f : set → set → set, ∀z, SNo z → SNo_rec_i (G w f) z = G w f z (SNo_rec_i (G w f))
In Proofgold the corresponding term root is 12a51a... and proposition id is 0dc50e...
Axiom. (SNo_rec2_eq) We take the following as an axiom:
∀w, SNo w → ∀z, SNo z → SNo_rec2 w z = F w z SNo_rec2
In Proofgold the corresponding term root is e9ea41... and proposition id is ac9f2b...
End of Section SurrealRec2
Axiom. (SNo_ordinal_ind) We take the following as an axiom:
∀P : set → prop, (∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, P x) → (∀x, SNo x → P x)
In Proofgold the corresponding term root is 5b75fb... and proposition id is dc2c6d...
Axiom. (SNo_ordinal_ind2) We take the following as an axiom:
∀P : set → set → prop, (∀alpha, ordinal alpha → ∀beta, ordinal beta → ∀x ∈ SNoS_ alpha, ∀y ∈ SNoS_ beta, P x y) → (∀x y, SNo x → SNo y → P x y)
In Proofgold the corresponding term root is ba3315... and proposition id is 4cd5ac...
Axiom. (SNo_ordinal_ind3) We take the following as an axiom:
∀P : set → set → set → prop, (∀alpha, ordinal alpha → ∀beta, ordinal beta → ∀gamma, ordinal gamma → ∀x ∈ SNoS_ alpha, ∀y ∈ SNoS_ beta, ∀z ∈ SNoS_ gamma, P x y z) → (∀x y z, SNo x → SNo y → SNo z → P x y z)
In Proofgold the corresponding term root is fccdb6... and proposition id is dece8c...
Axiom. (SNoLev_ind) We take the following as an axiom:
∀P : set → prop, (∀x, SNo x → (∀w ∈ SNoS_ (SNoLev x), P w) → P x) → (∀x, SNo x → P x)
In Proofgold the corresponding term root is 8b2b42... and proposition id is 851a88...
Axiom. (SNoLev_ind2) We take the following as an axiom:
∀P : set → set → prop, (∀x y, SNo x → SNo y → (∀w ∈ SNoS_ (SNoLev x), P w y) → (∀z ∈ SNoS_ (SNoLev y), P x z) → (∀w ∈ SNoS_ (SNoLev x), ∀z ∈ SNoS_ (SNoLev y), P w z) → P x y) → ∀x y, SNo x → SNo y → P x y
In Proofgold the corresponding term root is 87eb9a... and proposition id is 800d4c...
Axiom. (SNoLev_ind3) We take the following as an axiom:
∀P : set → set → set → prop, (∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x), P u y z) → (∀v ∈ SNoS_ (SNoLev y), P x v z) → (∀w ∈ SNoS_ (SNoLev z), P x y w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), P u v z) → (∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), P u y w) → (∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), P x v w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), P u v w) → P x y z) → ∀x y z, SNo x → SNo y → SNo z → P x y z
In Proofgold the corresponding term root is f1d779... and proposition id is ee16b9...
Axiom. (SNo_omega) We take the following as an axiom:
SNo ω
In Proofgold the corresponding term root is f65848... and proposition id is db7b5f...
Axiom. (SNoLt_0_1) We take the following as an axiom:
0 < 1
In Proofgold the corresponding term root is dd6047... and proposition id is cb6392...
Axiom. (SNoLt_0_2) We take the following as an axiom:
0 < 2
In Proofgold the corresponding term root is 7be36f... and proposition id is f46934...
Axiom. (SNoLt_1_2) We take the following as an axiom:
1 < 2
In Proofgold the corresponding term root is cc44e8... and proposition id is 19d5e1...
Beginning of Section SurrealMinus
Definition. We define minus_SNo to be SNo_rec_i (λx m ⇒ SNoCut {m z|z ∈ SNoR x} {m w|w ∈ SNoL x}) of type set → set.
In Proofgold the corresponding term root is 268a6c... and object id is 8a6d85...
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Axiom. (minus_SNo_eq) We take the following as an axiom:
∀x, SNo x → - x = SNoCut {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
In Proofgold the corresponding term root is c9793e... and proposition id is 570cba...
Axiom. (minus_SNo_prop1) We take the following as an axiom:
∀x, SNo x → SNo (- x) ∧ (∀u ∈ SNoL x, - x < - u) ∧ (∀u ∈ SNoR x, - u < - x) ∧ SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
In Proofgold the corresponding term root is 7c0e82... and proposition id is f0b75f...
Axiom. (SNo_minus_SNo) We take the following as an axiom:
∀x, SNo x → SNo (- x)
In Proofgold the corresponding term root is 5cf7d9... and proposition id is 744cc2...
Axiom. (minus_SNo_Lt_contra) We take the following as an axiom:
∀x y, SNo x → SNo y → x < y → - y < - x
In Proofgold the corresponding term root is 5ce52d... and proposition id is 3ebf6e...
Axiom. (minus_SNo_Le_contra) We take the following as an axiom:
∀x y, SNo x → SNo y → x ≤ y → - y ≤ - x
In Proofgold the corresponding term root is c1b225... and proposition id is f8c896...
Axiom. (minus_SNo_SNoCutP) We take the following as an axiom:
∀x, SNo x → SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
In Proofgold the corresponding term root is 99c6fc... and proposition id is 5ad5e4...
Axiom. (minus_SNo_SNoCutP_gen) We take the following as an axiom:
∀L R, SNoCutP L R → SNoCutP {- z|z ∈ R} {- w|w ∈ L}
In Proofgold the corresponding term root is e7650d... and proposition id is 687fea...
Axiom. (minus_SNo_Lev_lem1) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, SNoLev (- x) ⊆ SNoLev x
In Proofgold the corresponding term root is 14986a... and proposition id is afc115...
Axiom. (minus_SNo_Lev_lem2) We take the following as an axiom:
∀x, SNo x → SNoLev (- x) ⊆ SNoLev x
In Proofgold the corresponding term root is 879020... and proposition id is 19cf80...
Axiom. (minus_SNo_invol) We take the following as an axiom:
∀x, SNo x → - - x = x
In Proofgold the corresponding term root is 44bfe8... and proposition id is cc64ee...
Axiom. (minus_SNo_Lev) We take the following as an axiom:
∀x, SNo x → SNoLev (- x) = SNoLev x
In Proofgold the corresponding term root is f65499... and proposition id is 476ae5...
Axiom. (minus_SNo_SNo_) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x, SNo_ alpha x → SNo_ alpha (- x)
In Proofgold the corresponding term root is 84605f... and proposition id is 14bd6d...
Axiom. (minus_SNo_SNoS_) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x, x ∈ SNoS_ alpha → - x ∈ SNoS_ alpha
In Proofgold the corresponding term root is 12f1a5... and proposition id is e10c92...
Axiom. (minus_SNoCut_eq_lem) We take the following as an axiom:
∀v, SNo v → ∀L R, SNoCutP L R → v = SNoCut L R → - v = SNoCut {- z|z ∈ R} {- w|w ∈ L}
In Proofgold the corresponding term root is 29069a... and proposition id is 11eb03...
Axiom. (minus_SNoCut_eq) We take the following as an axiom:
∀L R, SNoCutP L R → - SNoCut L R = SNoCut {- z|z ∈ R} {- w|w ∈ L}
In Proofgold the corresponding term root is 083ffe... and proposition id is 54736f...
Axiom. (minus_SNo_Lt_contra1) We take the following as an axiom:
∀x y, SNo x → SNo y → - x < y → - y < x
In Proofgold the corresponding term root is 226757... and proposition id is 298729...
Axiom. (minus_SNo_Lt_contra2) We take the following as an axiom:
∀x y, SNo x → SNo y → x < - y → y < - x
In Proofgold the corresponding term root is c6f2da... and proposition id is f41968...
Axiom. (mordinal_SNoLev_min_2) We take the following as an axiom:
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ ordsucc alpha → - alpha ≤ z
In Proofgold the corresponding term root is 2766c7... and proposition id is a96d68...
Axiom. (minus_SNo_SNoS_omega) We take the following as an axiom:
∀x ∈ SNoS_ ω, - x ∈ SNoS_ ω
In Proofgold the corresponding term root is daeba5... and proposition id is 0c19f5...
Axiom. (SNoL_minus_SNoR) We take the following as an axiom:
∀x, SNo x → SNoL (- x) = {- w|w ∈ SNoR x}
In Proofgold the corresponding term root is 084b2d... and proposition id is 8b2b92...
End of Section SurrealMinus
Beginning of Section SurrealAdd
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Definition. We define add_SNo to be SNo_rec2 (λx y a ⇒ SNoCut ({a w y|w ∈ SNoL x} ∪ {a x w|w ∈ SNoL y}) ({a z y|z ∈ SNoR x} ∪ {a x z|z ∈ SNoR y})) of type set → set → set.
In Proofgold the corresponding term root is 127d04... and object id is f62f9a...
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Axiom. (add_SNo_eq) We take the following as an axiom:
∀x, SNo x → ∀y, SNo y → x + y = SNoCut ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y})
In Proofgold the corresponding term root is 0c1128... and proposition id is 437a9c...
Axiom. (add_SNo_prop1) We take the following as an axiom:
∀x y, SNo x → SNo y → SNo (x + y) ∧ (∀u ∈ SNoL x, u + y < x + y) ∧ (∀u ∈ SNoR x, x + y < u + y) ∧ (∀u ∈ SNoL y, x + u < x + y) ∧ (∀u ∈ SNoR y, x + y < x + u) ∧ SNoCutP ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y})
In Proofgold the corresponding term root is f3ece7... and proposition id is 5a879f...
Axiom. (SNo_add_SNo) We take the following as an axiom:
∀x y, SNo x → SNo y → SNo (x + y)
In Proofgold the corresponding term root is c4a9a6... and proposition id is a57095...
Axiom. (SNo_add_SNo_3) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → SNo (x + y + z)
In Proofgold the corresponding term root is f6ef07... and proposition id is f2d78c...
Axiom. (SNo_add_SNo_3c) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → SNo (x + y + - z)
In Proofgold the corresponding term root is 104eb9... and proposition id is 833be8...
Axiom. (add_SNo_Lt1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x < z → x + y < z + y
In Proofgold the corresponding term root is 92232f... and proposition id is cb0738...
Axiom. (add_SNo_Le1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x ≤ z → x + y ≤ z + y
In Proofgold the corresponding term root is d8f37e... and proposition id is abcf72...
Axiom. (add_SNo_Lt2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → y < z → x + y < x + z
In Proofgold the corresponding term root is 6ad464... and proposition id is 6f0941...
Axiom. (add_SNo_Le2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → y ≤ z → x + y ≤ x + z
In Proofgold the corresponding term root is 14975e... and proposition id is 3f52ba...
Axiom. (add_SNo_Lt3a) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x < z → y ≤ w → x + y < z + w
In Proofgold the corresponding term root is b2215f... and proposition id is 18ff91...
Axiom. (add_SNo_Lt3b) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x ≤ z → y < w → x + y < z + w
In Proofgold the corresponding term root is 5b4f92... and proposition id is 8fe0d9...
Axiom. (add_SNo_Lt3) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x < z → y < w → x + y < z + w
In Proofgold the corresponding term root is 7141a8... and proposition id is 55bdab...
Axiom. (add_SNo_Le3) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x ≤ z → y ≤ w → x + y ≤ z + w
In Proofgold the corresponding term root is 0be637... and proposition id is be66ca...
Axiom. (add_SNo_SNoCutP) We take the following as an axiom:
∀x y, SNo x → SNo y → SNoCutP ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y})
In Proofgold the corresponding term root is e2b7d7... and proposition id is f86b1a...
Axiom. (add_SNo_com) We take the following as an axiom:
∀x y, SNo x → SNo y → x + y = y + x
In Proofgold the corresponding term root is 548814... and proposition id is f017e5...
Axiom. (add_SNo_0L) We take the following as an axiom:
∀x, SNo x → 0 + x = x
In Proofgold the corresponding term root is 107598... and proposition id is 446bad...
Axiom. (add_SNo_0R) We take the following as an axiom:
∀x, SNo x → x + 0 = x
In Proofgold the corresponding term root is d8a186... and proposition id is 1a7fa1...
Axiom. (add_SNo_minus_SNo_linv) We take the following as an axiom:
∀x, SNo x → - x + x = 0
In Proofgold the corresponding term root is 424719... and proposition id is 44e251...
Axiom. (add_SNo_minus_SNo_rinv) We take the following as an axiom:
∀x, SNo x → x + - x = 0
In Proofgold the corresponding term root is 9e8c44... and proposition id is b2f9cf...
Axiom. (add_SNo_ordinal_SNoCutP) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → SNoCutP ({x + beta|x ∈ SNoS_ alpha} ∪ {alpha + x|x ∈ SNoS_ beta}) Empty
In Proofgold the corresponding term root is 2823e4... and proposition id is 507eab...
Axiom. (add_SNo_ordinal_eq) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → alpha + beta = SNoCut ({x + beta|x ∈ SNoS_ alpha} ∪ {alpha + x|x ∈ SNoS_ beta}) Empty
In Proofgold the corresponding term root is cfe1f5... and proposition id is ee8e7c...
Axiom. (add_SNo_ordinal_ordinal) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → ordinal (alpha + beta)
In Proofgold the corresponding term root is e9309a... and proposition id is ee9c23...
Axiom. (add_SNo_ordinal_SL) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → ordsucc alpha + beta = ordsucc (alpha + beta)
In Proofgold the corresponding term root is d55bd8... and proposition id is 61ae57...
Axiom. (add_SNo_ordinal_SR) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → alpha + ordsucc beta = ordsucc (alpha + beta)
In Proofgold the corresponding term root is e7378a... and proposition id is 0c1a6d...
Axiom. (add_SNo_ordinal_InL) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → ∀gamma ∈ alpha, gamma + beta ∈ alpha + beta
In Proofgold the corresponding term root is 09a829... and proposition id is 5acda8...
Axiom. (add_SNo_ordinal_InR) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → ∀gamma ∈ beta, alpha + gamma ∈ alpha + beta
In Proofgold the corresponding term root is d291f4... and proposition id is 0f42b5...
Axiom. (add_nat_add_SNo) We take the following as an axiom:
∀n m ∈ ω, add_nat n m = n + m
In Proofgold the corresponding term root is 1701fc... and proposition id is 9df659...
Axiom. (add_SNo_In_omega) We take the following as an axiom:
∀n m ∈ ω, n + m ∈ ω
In Proofgold the corresponding term root is f45cbb... and proposition id is eb6375...
Axiom. (add_SNo_1_1_2) We take the following as an axiom:
1 + 1 = 2
In Proofgold the corresponding term root is bbc448... and proposition id is 2b8298...
Axiom. (add_SNo_SNoL_interpolate) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀u ∈ SNoL (x + y), (∃v ∈ SNoL x, u ≤ v + y) ∨ (∃v ∈ SNoL y, u ≤ x + v)
In Proofgold the corresponding term root is 971363... and proposition id is 3cafc1...
Axiom. (add_SNo_SNoR_interpolate) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀u ∈ SNoR (x + y), (∃v ∈ SNoR x, v + y ≤ u) ∨ (∃v ∈ SNoR y, x + v ≤ u)
In Proofgold the corresponding term root is 928f71... and proposition id is 31fa94...
Axiom. (add_SNo_assoc) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + (y + z) = (x + y) + z
In Proofgold the corresponding term root is 39b331... and proposition id is bc15ad...
Axiom. (add_SNo_minus_R2) We take the following as an axiom:
∀x y, SNo x → SNo y → (x + y) + - y = x
In Proofgold the corresponding term root is 3e7b33... and proposition id is 91f4ef...
Axiom. (add_SNo_minus_R2') We take the following as an axiom:
∀x y, SNo x → SNo y → (x + - y) + y = x
In Proofgold the corresponding term root is 4f9468... and proposition id is 43b4d1...
Axiom. (add_SNo_minus_L2) We take the following as an axiom:
∀x y, SNo x → SNo y → - x + (x + y) = y
In Proofgold the corresponding term root is 2cd65e... and proposition id is 598ee6...
Axiom. (add_SNo_minus_L2') We take the following as an axiom:
∀x y, SNo x → SNo y → x + (- x + y) = y
In Proofgold the corresponding term root is 632a4d... and proposition id is a8450d...
Axiom. (add_SNo_cancel_L) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y = x + z → y = z
In Proofgold the corresponding term root is 014096... and proposition id is 781256...
Axiom. (add_SNo_cancel_R) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y = z + y → x = z
In Proofgold the corresponding term root is 3de43c... and proposition id is e62801...
Axiom. (minus_SNo_0) We take the following as an axiom:
- 0 = 0
In Proofgold the corresponding term root is 77bc67... and proposition id is 3fcc57...
Axiom. (minus_add_SNo_distr) We take the following as an axiom:
∀x y, SNo x → SNo y → - (x + y) = (- x) + (- y)
In Proofgold the corresponding term root is 57ec9d... and proposition id is da8d5a...
Axiom. (add_SNo_Lev_bd) We take the following as an axiom:
∀x y, SNo x → SNo y → SNoLev (x + y) ⊆ SNoLev x + SNoLev y
In Proofgold the corresponding term root is 0f257c... and proposition id is 0680ef...
Axiom. (add_SNo_SNoS_omega) We take the following as an axiom:
∀x y ∈ SNoS_ ω, x + y ∈ SNoS_ ω
In Proofgold the corresponding term root is 931103... and proposition id is 6d16aa...
Axiom. (add_SNo_Lt1_cancel) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y < z + y → x < z
In Proofgold the corresponding term root is e5c11e... and proposition id is 2ec8ae...
Axiom. (add_SNo_Lt2_cancel) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y < x + z → y < z
In Proofgold the corresponding term root is 9ecfc8... and proposition id is d4afbd...
Axiom. (add_SNo_Le1_cancel) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y ≤ z + y → x ≤ z
In Proofgold the corresponding term root is 01a9b8... and proposition id is 8bfac1...
Axiom. (add_SNo_assoc_4) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y + z + w = (x + y + z) + w
In Proofgold the corresponding term root is b9919a... and proposition id is f2ec8c...
Axiom. (add_SNo_com_3_0_1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y + z = y + x + z
In Proofgold the corresponding term root is 53adb5... and proposition id is 3c9cc8...
Axiom. (add_SNo_com_3b_1_2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → (x + y) + z = (x + z) + y
In Proofgold the corresponding term root is 2ccf2b... and proposition id is f2dd80...
Axiom. (add_SNo_com_4_inner_mid) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y) + (z + w) = (x + z) + (y + w)
In Proofgold the corresponding term root is 635cb7... and proposition id is e25ee6...
Axiom. (add_SNo_minus_SNo_prop2) We take the following as an axiom:
∀x y, SNo x → SNo y → x + - x + y = y
In Proofgold the corresponding term root is 632a4d... and proposition id is a8450d...
Axiom. (add_SNo_minus_Lt1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + - y < z → x < z + y
In Proofgold the corresponding term root is 643876... and proposition id is 4033dc...
Axiom. (add_SNo_minus_Lt2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → z < x + - y → z + y < x
In Proofgold the corresponding term root is 76c543... and proposition id is 362145...
Axiom. (add_SNo_minus_Lt1b) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x < z + y → x + - y < z
In Proofgold the corresponding term root is 5012b1... and proposition id is 0b5cca...
Axiom. (add_SNo_minus_Lt2b) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → z + y < x → z < x + - y
In Proofgold the corresponding term root is 24d1a6... and proposition id is 684192...
Axiom. (add_SNo_minus_Le2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → z ≤ x + - y → z + y ≤ x
In Proofgold the corresponding term root is 85af84... and proposition id is 86b40b...
Axiom. (add_SNo_minus_Le2b) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → z + y ≤ x → z ≤ x + - y
In Proofgold the corresponding term root is 688ef9... and proposition id is d815dd...
Axiom. (ordinal_ordsucc_SNo_eq) We take the following as an axiom:
∀alpha, ordinal alpha → ordsucc alpha = 1 + alpha
In Proofgold the corresponding term root is f0596d... and proposition id is 36bf6d...
Axiom. (add_SNo_1_ordsucc) We take the following as an axiom:
∀n ∈ ω, n + 1 = ordsucc n
In Proofgold the corresponding term root is ec6cad... and proposition id is 85f670...
End of Section SurrealAdd
Beginning of Section SurrealMul
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Definition. We define mul_SNo to be SNo_rec2 (λx y m ⇒ SNoCut ({m (w 0) y + m x (w 1) + - m (w 0) (w 1)|w ∈ SNoL x ⨯ SNoL y} ∪ {m (z 0) y + m x (z 1) + - m (z 0) (z 1)|z ∈ SNoR x ⨯ SNoR y}) ({m (w 0) y + m x (w 1) + - m (w 0) (w 1)|w ∈ SNoL x ⨯ SNoR y} ∪ {m (z 0) y + m x (z 1) + - m (z 0) (z 1)|z ∈ SNoR x ⨯ SNoL y})) of type set → set → set.
In Proofgold the corresponding term root is 48d054... and object id is b14730...
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Axiom. (mul_SNo_eq) We take the following as an axiom:
∀x, SNo x → ∀y, SNo y → x * y = SNoCut ({(w 0) * y + x * (w 1) + - (w 0) * (w 1)|w ∈ SNoL x ⨯ SNoL y} ∪ {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|z ∈ SNoR x ⨯ SNoR y}) ({(w 0) * y + x * (w 1) + - (w 0) * (w 1)|w ∈ SNoL x ⨯ SNoR y} ∪ {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|z ∈ SNoR x ⨯ SNoL y})
In Proofgold the corresponding term root is 726bd9... and proposition id is 3525c5...
Axiom. (mul_SNo_eq_2) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀p : prop, (∀L R, (∀u, u ∈ L → (∀q : prop, (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, u = w0 * y + x * w1 + - w0 * w1 → q) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, u = z0 * y + x * z1 + - z0 * z1 → q) → q)) → (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, w0 * y + x * w1 + - w0 * w1 ∈ L) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, z0 * y + x * z1 + - z0 * z1 ∈ L) → (∀u, u ∈ R → (∀q : prop, (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, u = w0 * y + x * z1 + - w0 * z1 → q) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, u = z0 * y + x * w1 + - z0 * w1 → q) → q)) → (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, w0 * y + x * z1 + - w0 * z1 ∈ R) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, z0 * y + x * w1 + - z0 * w1 ∈ R) → x * y = SNoCut L R → p) → p
In Proofgold the corresponding term root is 97f72a... and proposition id is d69cc6...
Axiom. (mul_SNo_prop_1) We take the following as an axiom:
∀x, SNo x → ∀y, SNo y → ∀p : prop, (SNo (x * y) → (∀u ∈ SNoL x, ∀v ∈ SNoL y, u * y + x * v < x * y + u * v) → (∀u ∈ SNoR x, ∀v ∈ SNoR y, u * y + x * v < x * y + u * v) → (∀u ∈ SNoL x, ∀v ∈ SNoR y, x * y + u * v < u * y + x * v) → (∀u ∈ SNoR x, ∀v ∈ SNoL y, x * y + u * v < u * y + x * v) → p) → p
In Proofgold the corresponding term root is 3018e4... and proposition id is 5e4d16...
Axiom. (SNo_mul_SNo) We take the following as an axiom:
∀x y, SNo x → SNo y → SNo (x * y)
In Proofgold the corresponding term root is 7fa2e2... and proposition id is 9fd082...
Axiom. (SNo_mul_SNo_lem) We take the following as an axiom:
∀x y u v, SNo x → SNo y → SNo u → SNo v → SNo (u * y + x * v + - (u * v))
In Proofgold the corresponding term root is 632e95... and proposition id is 3a9abb...
Axiom. (mul_SNo_Lt) We take the following as an axiom:
∀x y u v, SNo x → SNo y → SNo u → SNo v → u < x → v < y → u * y + x * v < x * y + u * v
In Proofgold the corresponding term root is 428b35... and proposition id is c23201...
Axiom. (mul_SNo_Le) We take the following as an axiom:
∀x y u v, SNo x → SNo y → SNo u → SNo v → u ≤ x → v ≤ y → u * y + x * v ≤ x * y + u * v
In Proofgold the corresponding term root is d9a12c... and proposition id is acb620...
Axiom. (mul_SNo_SNoL_interpolate) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀u ∈ SNoL (x * y), (∃v ∈ SNoL x, ∃w ∈ SNoL y, u + v * w ≤ v * y + x * w) ∨ (∃v ∈ SNoR x, ∃w ∈ SNoR y, u + v * w ≤ v * y + x * w)
In Proofgold the corresponding term root is 7d1b52... and proposition id is f460fc...
Axiom. (mul_SNo_SNoL_interpolate_impred) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀u ∈ SNoL (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoL y, u + v * w ≤ v * y + x * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoR y, u + v * w ≤ v * y + x * w → p) → p
In Proofgold the corresponding term root is 395b74... and proposition id is ad6f96...
Axiom. (mul_SNo_SNoR_interpolate) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀u ∈ SNoR (x * y), (∃v ∈ SNoL x, ∃w ∈ SNoR y, v * y + x * w ≤ u + v * w) ∨ (∃v ∈ SNoR x, ∃w ∈ SNoL y, v * y + x * w ≤ u + v * w)
In Proofgold the corresponding term root is e15949... and proposition id is b67a35...
Axiom. (mul_SNo_SNoR_interpolate_impred) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀u ∈ SNoR (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoR y, v * y + x * w ≤ u + v * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoL y, v * y + x * w ≤ u + v * w → p) → p
In Proofgold the corresponding term root is e5cae5... and proposition id is d1fff1...
Axiom. (nonpos_nonneg_0) We take the following as an axiom:
∀m n ∈ ω, m = - n → m = 0 ∧ n = 0
In Proofgold the corresponding term root is 94b9ef... and proposition id is bac05d...
Axiom. (mul_minus_SNo_distrR) We take the following as an axiom:
∀x y, SNo x → SNo y → x * (- y) = - (x * y)
In Proofgold the corresponding term root is ab775a... and proposition id is 2e7475...
End of Section SurrealMul
Beginning of Section Int
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Definition. We define int to be ω ∪ {- n|n ∈ ω} of type set.
In Proofgold the corresponding term root is 90ee85... and object id is 331669...
Axiom. (int_SNo_cases) We take the following as an axiom:
∀p : set → prop, (∀n ∈ ω, p n) → (∀n ∈ ω, p (- n)) → ∀x ∈ int, p x
In Proofgold the corresponding term root is 60107a... and proposition id is 14278d...
Axiom. (int_3_cases) We take the following as an axiom:
∀n ∈ int, ∀p : prop, (∀m ∈ ω, n = - ordsucc m → p) → (n = 0 → p) → (∀m ∈ ω, n = ordsucc m → p) → p
In Proofgold the corresponding term root is 67b16d... and proposition id is 5c24db...
Axiom. (int_SNo) We take the following as an axiom:
∀x ∈ int, SNo x
In Proofgold the corresponding term root is 19fdd2... and proposition id is 6089ec...
Axiom. (Subq_omega_int) We take the following as an axiom:
ω ⊆ int
In Proofgold the corresponding term root is 405dda... and proposition id is b1bb2b...
Axiom. (int_minus_SNo_omega) We take the following as an axiom:
∀n ∈ ω, - n ∈ int
In Proofgold the corresponding term root is 869503... and proposition id is 3a2593...
Axiom. (int_add_SNo_lem) We take the following as an axiom:
∀n ∈ ω, ∀m, nat_p m → - n + m ∈ int
In Proofgold the corresponding term root is 8f0047... and proposition id is aab9d5...
Axiom. (int_add_SNo) We take the following as an axiom:
∀x y ∈ int, x + y ∈ int
In Proofgold the corresponding term root is d66975... and proposition id is 1036d9...
Axiom. (int_minus_SNo) We take the following as an axiom:
∀x ∈ int, - x ∈ int
In Proofgold the corresponding term root is 00e714... and proposition id is b2c591...
Axiom. (int_mul_SNo) We take the following as an axiom:
∀x y ∈ int, x * y ∈ int
In Proofgold the corresponding term root is a7bc92... and proposition id is f40564...
Axiom. (nonneg_int_nat_p) We take the following as an axiom:
∀n ∈ int, 0 ≤ n → nat_p n
In Proofgold the corresponding term root is 17e526... and proposition id is aa7e89...
End of Section Int
Beginning of Section SurrealExp
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Definition. We define exp_SNo_nat to be λn m : set ⇒ nat_primrec 1 (λ_ r ⇒ n * r) m of type set → set → set.
In Proofgold the corresponding term root is cc5143... and object id is ea8104...
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Axiom. (exp_SNo_nat_0) We take the following as an axiom:
∀x, SNo x → x ^ 0 = 1
In Proofgold the corresponding term root is c266f2... and proposition id is fe30fb...
Axiom. (exp_SNo_nat_S) We take the following as an axiom:
∀x, SNo x → ∀n, nat_p n → x ^ (ordsucc n) = x * x ^ n
In Proofgold the corresponding term root is 6b5ef9... and proposition id is ae55b7...
Axiom. (exp_SNo_nat_1) We take the following as an axiom:
∀x, SNo x → x ^ 1 = x
In Proofgold the corresponding term root is 9a6103... and proposition id is d52b56...
Axiom. (SNo_exp_SNo_nat) We take the following as an axiom:
∀x, SNo x → ∀n, nat_p n → SNo (x ^ n)
In Proofgold the corresponding term root is 7a77b4... and proposition id is f317bf...
Axiom. (nat_exp_SNo_nat) We take the following as an axiom:
∀x, nat_p x → ∀n, nat_p n → nat_p (x ^ n)
In Proofgold the corresponding term root is 14de73... and proposition id is 39327e...
End of Section SurrealExp