Unary Minus on Surreal Numbers

From Parts 1 - 3

Object. The name Eps_i is a term of type (set → prop) → set.
Axiom. (Eps_i_ax) We take the following as an axiom:
∀P : set → prop, ∀x : set, P x → P (Eps_i P)
Definition. We define True to be ∀p : prop, p → p of type prop.
Definition. We define False to be ∀p : prop, p of type prop.
Definition. We define not to be λA : prop ⇒ A → False of type prop → prop.
Notation. We use ¬ as a prefix operator with priority 700 corresponding to applying term not.
Definition. We define and to be λA B : prop ⇒ ∀p : prop, (A → B → p) → p of type prop → prop → prop.
Notation. We use ∧ as an infix operator with priority 780 and which associates to the left corresponding to applying term and.
Definition. We define or to be λA B : prop ⇒ ∀p : prop, (A → p) → (B → p) → p of type prop → prop → prop.
Notation. We use ∨ as an infix operator with priority 785 and which associates to the left corresponding to applying term or.
Definition. We define iff to be λA B : prop ⇒ and (A → B) (B → A) of type prop → prop → prop.
Notation. We use ↔ as an infix operator with priority 805 and no associativity corresponding to applying term iff.
Beginning of Section Eq
Variable A : SType
Definition. We define eq to be λx y : A ⇒ ∀Q : A → A → prop, Q x y → Q y x of type A → A → prop.
Definition. We define neq to be λx y : A ⇒ ¬ eq x y of type A → A → prop.
End of Section Eq
Notation. We use = as an infix operator with priority 502 and no associativity corresponding to applying term eq.
Notation. We use ≠ as an infix operator with priority 502 and no associativity corresponding to applying term neq.
Beginning of Section FE
Variable A B : SType
Axiom. (func_ext) We take the following as an axiom:
∀f g : A → B, (∀x : A, f x = g x) → f = g
End of Section FE
Beginning of Section Ex
Variable A : SType
Definition. We define ex to be λQ : A → prop ⇒ ∀P : prop, (∀x : A, Q x → P) → P of type (A → prop) → prop.
End of Section Ex
Notation. We use ∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex.
Axiom. (prop_ext) We take the following as an axiom:
∀p q : prop, iff p q → p = q
Object. The name In is a term of type set → set → prop.
Notation. We use ∈ as an infix operator with priority 500 and no associativity corresponding to applying term In. Furthermore, we may write ∀ x ∈ A, B to mean ∀ x : set, x ∈ A → B.
Definition. We define Subq to be λA B ⇒ ∀x ∈ A, x ∈ B of type set → set → prop.
Notation. We use ⊆ as an infix operator with priority 500 and no associativity corresponding to applying term Subq. Furthermore, we may write ∀ x ⊆ A, B to mean ∀ x : set, x ⊆ A → B.
Axiom. (set_ext) We take the following as an axiom:
∀X Y : set, X ⊆ Y → Y ⊆ X → X = Y
Axiom. (In_ind) We take the following as an axiom:
∀P : set → prop, (∀X : set, (∀x ∈ X, P x) → P X) → ∀X : set, P X
Notation. We use ∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex and handling ∈ or ⊆ ascriptions using and.
Object. The name Empty is a term of type set.
Axiom. (EmptyAx) We take the following as an axiom:
¬ ∃x : set, x ∈ Empty
Object. The name ⋃ is a term of type set → set.
Axiom. (UnionEq) We take the following as an axiom:
∀X x, x ∈ ⋃ X ↔ ∃Y, x ∈ Y ∧ Y ∈ X
Object. The name 𝒫 is a term of type set → set.
Axiom. (PowerEq) We take the following as an axiom:
∀X Y : set, Y ∈ 𝒫 X ↔ Y ⊆ X
Object. The name Repl is a term of type set → (set → set) → set.
Notation. {B| x ∈ A} is notation for Repl A (λ x . B).
Axiom. (ReplEq) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} ↔ ∃x ∈ A, y = F x
Definition. We define TransSet to be λU : set ⇒ ∀x ∈ U, x ⊆ U of type set → prop.
Definition. We define Union_closed to be λU : set ⇒ ∀X : set, X ∈ U → ⋃ X ∈ U of type set → prop.
Definition. We define Power_closed to be λU : set ⇒ ∀X : set, X ∈ U → 𝒫 X ∈ U of type set → prop.
Definition. We define Repl_closed to be λU : set ⇒ ∀X : set, X ∈ U → ∀F : set → set, (∀x : set, x ∈ X → F x ∈ U) → {F x|x ∈ X} ∈ U of type set → prop.
Definition. We define ZF_closed to be λU : set ⇒ Union_closed U ∧ Power_closed U ∧ Repl_closed U of type set → prop.
Object. The name UnivOf is a term of type set → set.
Axiom. (UnivOf_In) We take the following as an axiom:
∀N : set, N ∈ UnivOf N
Axiom. (UnivOf_TransSet) We take the following as an axiom:
∀N : set, TransSet (UnivOf N)
Axiom. (UnivOf_ZF_closed) We take the following as an axiom:
∀N : set, ZF_closed (UnivOf N)
Axiom. (UnivOf_Min) We take the following as an axiom:
∀N U : set, N ∈ U → TransSet U → ZF_closed U → UnivOf N ⊆ U
Axiom. (FalseE) We take the following as an axiom:
False → ∀p : prop, p
Axiom. (TrueI) We take the following as an axiom:
True
Axiom. (andI) We take the following as an axiom:
∀A B : prop, A → B → A ∧ B
Axiom. (andEL) We take the following as an axiom:
∀A B : prop, A ∧ B → A
Axiom. (andER) We take the following as an axiom:
∀A B : prop, A ∧ B → B
Axiom. (orIL) We take the following as an axiom:
∀A B : prop, A → A ∨ B
Axiom. (orIR) We take the following as an axiom:
∀A B : prop, B → A ∨ B
Beginning of Section PropN
Variable P1 P2 P3 : prop
Axiom. (and3I) We take the following as an axiom:
P1 → P2 → P3 → P1 ∧ P2 ∧ P3
Axiom. (and3E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 → (∀p : prop, (P1 → P2 → P3 → p) → p)
Axiom. (or3I1) We take the following as an axiom:
P1 → P1 ∨ P2 ∨ P3
Axiom. (or3I2) We take the following as an axiom:
P2 → P1 ∨ P2 ∨ P3
Axiom. (or3I3) We take the following as an axiom:
P3 → P1 ∨ P2 ∨ P3
Axiom. (or3E) We take the following as an axiom:
P1 ∨ P2 ∨ P3 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → p)
Variable P4 : prop
Axiom. (and4I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4
Variable P5 : prop
Axiom. (and5I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5
End of Section PropN
Axiom. (not_or_and_demorgan) We take the following as an axiom:
∀A B : prop, ¬ (A ∨ B) → ¬ A ∧ ¬ B
Axiom. (not_ex_all_demorgan_i) We take the following as an axiom:
∀P : set → prop, (¬ ∃x, P x) → ∀x, ¬ P x
Axiom. (iffI) We take the following as an axiom:
∀A B : prop, (A → B) → (B → A) → (A ↔ B)
Axiom. (iffEL) We take the following as an axiom:
∀A B : prop, (A ↔ B) → A → B
Axiom. (iffER) We take the following as an axiom:
∀A B : prop, (A ↔ B) → B → A
Axiom. (iff_refl) We take the following as an axiom:
∀A : prop, A ↔ A
Axiom. (iff_sym) We take the following as an axiom:
∀A B : prop, (A ↔ B) → (B ↔ A)
Axiom. (iff_trans) We take the following as an axiom:
∀A B C : prop, (A ↔ B) → (B ↔ C) → (A ↔ C)
Axiom. (eq_i_tra) We take the following as an axiom:
∀x y z, x = y → y = z → x = z
Axiom. (f_eq_i) We take the following as an axiom:
∀f : set → set, ∀x y, x = y → f x = f y
Axiom. (neq_i_sym) We take the following as an axiom:
∀x y, x ≠ y → y ≠ x
Definition. We define nIn to be λx X ⇒ ¬ In x X of type set → set → prop.
Notation. We use ∉ as an infix operator with priority 502 and no associativity corresponding to applying term nIn.
Axiom. (Eps_i_ex) We take the following as an axiom:
∀P : set → prop, (∃x, P x) → P (Eps_i P)
Axiom. (pred_ext) We take the following as an axiom:
∀P Q : set → prop, (∀x, P x ↔ Q x) → P = Q
Axiom. (prop_ext_2) We take the following as an axiom:
∀p q : prop, (p → q) → (q → p) → p = q
Axiom. (Subq_ref) We take the following as an axiom:
∀X : set, X ⊆ X
Axiom. (Subq_tra) We take the following as an axiom:
∀X Y Z : set, X ⊆ Y → Y ⊆ Z → X ⊆ Z
Axiom. (Subq_contra) We take the following as an axiom:
∀X Y z : set, X ⊆ Y → z ∉ Y → z ∉ X
Axiom. (EmptyE) We take the following as an axiom:
∀x : set, x ∉ Empty
Axiom. (Subq_Empty) We take the following as an axiom:
∀X : set, Empty ⊆ X
Axiom. (Empty_Subq_eq) We take the following as an axiom:
∀X : set, X ⊆ Empty → X = Empty
Axiom. (Empty_eq) We take the following as an axiom:
∀X : set, (∀x, x ∉ X) → X = Empty
Axiom. (UnionI) We take the following as an axiom:
∀X x Y : set, x ∈ Y → Y ∈ X → x ∈ ⋃ X
Axiom. (UnionE) We take the following as an axiom:
∀X x : set, x ∈ ⋃ X → ∃Y : set, x ∈ Y ∧ Y ∈ X
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
Axiom. (PowerI) We take the following as an axiom:
∀X Y : set, Y ⊆ X → Y ∈ 𝒫 X
Axiom. (PowerE) We take the following as an axiom:
∀X Y : set, Y ∈ 𝒫 X → Y ⊆ X
Axiom. (Empty_In_Power) We take the following as an axiom:
∀X : set, Empty ∈ 𝒫 X
Axiom. (Self_In_Power) We take the following as an axiom:
∀X : set, X ∈ 𝒫 X
Axiom. (xm) We take the following as an axiom:
∀P : prop, P ∨ ¬ P
Axiom. (dneg) We take the following as an axiom:
∀P : prop, ¬ ¬ P → P
Axiom. (not_all_ex_demorgan_i) We take the following as an axiom:
∀P : set → prop, ¬ (∀x, P x) → ∃x, ¬ P x
Axiom. (eq_or_nand) We take the following as an axiom:
or = (λx y : prop ⇒ ¬ (¬ x ∧ ¬ y))
Object. The name exactly1of2 is a term of type prop → prop → prop.
Axiom. (exactly1of2_I1) We take the following as an axiom:
∀A B : prop, A → ¬ B → exactly1of2 A B
Axiom. (exactly1of2_I2) We take the following as an axiom:
∀A B : prop, ¬ A → B → exactly1of2 A B
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
Axiom. (exactly1of2_or) We take the following as an axiom:
∀A B : prop, exactly1of2 A B → A ∨ B
Axiom. (ReplI) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀x : set, x ∈ A → F x ∈ {F x|x ∈ A}
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
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
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
Axiom. (Repl_Empty) We take the following as an axiom:
∀F : set → set, {F x|x ∈ Empty} = Empty
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}
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}
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
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
Object. The name If_i is a term of type prop → set → set → set.
Notation. if cond then T else E is notation corresponding to If_i type cond T E where type is the inferred type of T.
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
Axiom. (If_i_0) We take the following as an axiom:
∀p : prop, ∀x y : set, ¬ p → (if p then x else y) = y
Axiom. (If_i_1) We take the following as an axiom:
∀p : prop, ∀x y : set, p → (if p then x else y) = x
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
Object. The name UPair is a term of type set → set → set.
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
Axiom. (UPairI1) We take the following as an axiom:
∀y z : set, y ∈ {y,z}
Axiom. (UPairI2) We take the following as an axiom:
∀y z : set, z ∈ {y,z}
Object. The name Sing is a term of type set → set.
Notation. {x} is notation for Sing x.
Axiom. (SingI) We take the following as an axiom:
∀x : set, x ∈ {x}
Axiom. (SingE) We take the following as an axiom:
∀x y : set, y ∈ {x} → y = x
Object. The name binunion is a term of type set → set → set.
Notation. We use ∪ as an infix operator with priority 345 and which associates to the left corresponding to applying term binunion.
Axiom. (binunionI1) We take the following as an axiom:
∀X Y z : set, z ∈ X → z ∈ X ∪ Y
Axiom. (binunionI2) We take the following as an axiom:
∀X Y z : set, z ∈ Y → z ∈ X ∪ Y
Axiom. (binunionE) We take the following as an axiom:
∀X Y z : set, z ∈ X ∪ Y → z ∈ X ∨ z ∈ Y
Axiom. (binunionE') We take the following as an axiom:
∀X Y z, ∀p : prop, (z ∈ X → p) → (z ∈ Y → p) → (z ∈ X ∪ Y → p)
Axiom. (binunion_asso) We take the following as an axiom:
∀X Y Z : set, X ∪ (Y ∪ Z) = (X ∪ Y) ∪ Z
Axiom. (binunion_com_Subq) We take the following as an axiom:
∀X Y : set, X ∪ Y ⊆ Y ∪ X
Axiom. (binunion_com) We take the following as an axiom:
∀X Y : set, X ∪ Y = Y ∪ X
Axiom. (binunion_idl) We take the following as an axiom:
∀X : set, Empty ∪ X = X
Axiom. (binunion_idr) We take the following as an axiom:
∀X : set, X ∪ Empty = X
Axiom. (binunion_Subq_1) We take the following as an axiom:
∀X Y : set, X ⊆ X ∪ Y
Axiom. (binunion_Subq_2) We take the following as an axiom:
∀X Y : set, Y ⊆ X ∪ Y
Axiom. (binunion_Subq_min) We take the following as an axiom:
∀X Y Z : set, X ⊆ Z → Y ⊆ Z → X ∪ Y ⊆ Z
Axiom. (Subq_binunion_eq) We take the following as an axiom:
∀X Y, (X ⊆ Y) = (X ∪ Y = Y)
Definition. We define SetAdjoin to be λX y ⇒ X ∪ {y} of type set → set → set.
Notation. We now use the set enumeration notation {...,...,...} in general. If 0 elements are given, then Empty is used to form the corresponding term. If 1 element is given, then Sing is used to form the corresponding term. If 2 elements are given, then UPair is used to form the corresponding term. If more than elements are given, then SetAdjoin is used to reduce to the case with one fewer elements.
Object. The name famunion is a term of type set → (set → set) → set.
Notation. We use ⋃ x [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using famunion.
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
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
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
Axiom. (famunion_Empty) We take the following as an axiom:
∀F : set → set, (⋃x ∈ EmptyF x) = Empty
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
Object. The name Sep is a term of type set.
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}
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
Axiom. (SepE1) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X
Axiom. (SepE2) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → P x
Axiom. (Sep_Subq) We take the following as an axiom:
∀X : set, ∀P : set → prop, {x ∈ X|P x} ⊆ X
Axiom. (Sep_In_Power) We take the following as an axiom:
∀X : set, ∀P : set → prop, {x ∈ X|P x} ∈ 𝒫 X
Object. The name ReplSep is a term of type set → (set → prop) → (set → set) → set.
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}
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
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
Object. The name binintersect is a term of type set → set → set.
Notation. We use ∩ as an infix operator with priority 340 and which associates to the left corresponding to applying term binintersect.
Axiom. (binintersectI) We take the following as an axiom:
∀X Y z, z ∈ X → z ∈ Y → z ∈ X ∩ Y
Axiom. (binintersectE) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ X ∧ z ∈ Y
Axiom. (binintersectE1) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ X
Axiom. (binintersectE2) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ Y
Axiom. (binintersect_Subq_1) We take the following as an axiom:
∀X Y : set, X ∩ Y ⊆ X
Axiom. (binintersect_Subq_2) We take the following as an axiom:
∀X Y : set, X ∩ Y ⊆ Y
Axiom. (binintersect_Subq_eq_1) We take the following as an axiom:
∀X Y, X ⊆ Y → X ∩ Y = X
Axiom. (binintersect_Subq_max) We take the following as an axiom:
∀X Y Z : set, Z ⊆ X → Z ⊆ Y → Z ⊆ X ∩ Y
Axiom. (binintersect_com_Subq) We take the following as an axiom:
∀X Y : set, X ∩ Y ⊆ Y ∩ X
Axiom. (binintersect_com) We take the following as an axiom:
∀X Y : set, X ∩ Y = Y ∩ X
Object. The name setminus is a term of type set → set → set.
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
Axiom. (setminusE) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y) → z ∈ X ∧ z ∉ Y
Axiom. (setminusE1) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y) → z ∈ X
Axiom. (setminus_Subq) We take the following as an axiom:
∀X Y : set, X ∖ Y ⊆ X
Axiom. (setminus_Subq_contra) We take the following as an axiom:
∀X Y Z : set, Z ⊆ Y → X ∖ Y ⊆ X ∖ Z
Axiom. (setminus_In_Power) We take the following as an axiom:
∀A U, A ∖ U ∈ 𝒫 A
Axiom. (In_irref) We take the following as an axiom:
∀x, x ∉ x
Axiom. (In_no2cycle) We take the following as an axiom:
∀x y, x ∈ y → y ∈ x → False
Object. The name ordsucc is a term of type set → set.
Axiom. (ordsuccI1) We take the following as an axiom:
∀x : set, x ⊆ ordsucc x
Axiom. (ordsuccI2) We take the following as an axiom:
∀x : set, x ∈ ordsucc x
Axiom. (ordsuccE) We take the following as an axiom:
∀x y : set, y ∈ ordsucc x → y ∈ x ∨ y = x
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
Axiom. (neq_ordsucc_0) We take the following as an axiom:
∀a : set, ordsucc a ≠ 0
Axiom. (ordsucc_inj) We take the following as an axiom:
∀a b : set, ordsucc a = ordsucc b → a = b
Axiom. (ordsucc_inj_contra) We take the following as an axiom:
∀a b : set, a ≠ b → ordsucc a ≠ ordsucc b
Axiom. (In_0_1) We take the following as an axiom:
0 ∈ 1
Axiom. (In_0_2) We take the following as an axiom:
0 ∈ 2
Axiom. (In_1_2) We take the following as an axiom:
1 ∈ 2
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.
Axiom. (nat_0) We take the following as an axiom:
nat_p 0
Axiom. (nat_ordsucc) We take the following as an axiom:
∀n : set, nat_p n → nat_p (ordsucc n)
Axiom. (nat_1) We take the following as an axiom:
nat_p 1
Axiom. (nat_2) We take the following as an axiom:
nat_p 2
Axiom. (nat_0_in_ordsucc) We take the following as an axiom:
∀n, nat_p n → 0 ∈ ordsucc n
Axiom. (nat_ordsucc_in_ordsucc) We take the following as an axiom:
∀n, nat_p n → ∀m ∈ n, ordsucc m ∈ ordsucc n
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
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
Axiom. (nat_inv) We take the following as an axiom:
∀n, nat_p n → n = 0 ∨ ∃x, nat_p x ∧ n = ordsucc x
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
Axiom. (nat_p_trans) We take the following as an axiom:
∀n, nat_p n → ∀m ∈ n, nat_p m
Axiom. (nat_trans) We take the following as an axiom:
∀n, nat_p n → ∀m ∈ n, m ⊆ n
Axiom. (nat_ordsucc_trans) We take the following as an axiom:
∀n, nat_p n → ∀m ∈ ordsucc n, m ⊆ n
Axiom. (Union_ordsucc_eq) We take the following as an axiom:
∀n, nat_p n → ⋃ (ordsucc n) = n
Axiom. (cases_1) We take the following as an axiom:
∀i ∈ 1, ∀p : set → prop, p 0 → p i
Axiom. (cases_2) We take the following as an axiom:
∀i ∈ 2, ∀p : set → prop, p 0 → p 1 → p i
Axiom. (cases_3) We take the following as an axiom:
∀i ∈ 3, ∀p : set → prop, p 0 → p 1 → p 2 → p i
Axiom. (neq_0_1) We take the following as an axiom:
0 ≠ 1
Axiom. (neq_1_0) We take the following as an axiom:
1 ≠ 0
Axiom. (neq_0_2) We take the following as an axiom:
0 ≠ 2
Axiom. (neq_2_0) We take the following as an axiom:
2 ≠ 0
Axiom. (neq_1_2) We take the following as an axiom:
1 ≠ 2
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
Axiom. (ZF_Union_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀X ∈ U, ⋃ X ∈ U
Axiom. (ZF_Power_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀X ∈ U, 𝒫 X ∈ U
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
Axiom. (ZF_UPair_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀x y ∈ U, {x,y} ∈ U
Axiom. (ZF_Sing_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀x ∈ U, {x} ∈ U
Axiom. (ZF_binunion_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀X Y ∈ U, (X ∪ Y) ∈ U
Axiom. (ZF_ordsucc_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀x ∈ U, ordsucc x ∈ U
Axiom. (nat_p_UnivOf_Empty) We take the following as an axiom:
∀n : set, nat_p n → n ∈ UnivOf Empty
Object. The name ω is a term of type set.
Axiom. (omega_nat_p) We take the following as an axiom:
∀n ∈ ω, nat_p n
Axiom. (nat_p_omega) We take the following as an axiom:
∀n : set, nat_p n → n ∈ ω
Axiom. (omega_ordsucc) We take the following as an axiom:
∀n ∈ ω, ordsucc n ∈ ω
Definition. We define ordinal to be λalpha : set ⇒ TransSet alpha ∧ ∀beta ∈ alpha, TransSet beta of type set → prop.
Axiom. (ordinal_TransSet) We take the following as an axiom:
∀alpha : set, ordinal alpha → TransSet alpha
Axiom. (ordinal_Empty) We take the following as an axiom:
ordinal Empty
Axiom. (ordinal_Hered) We take the following as an axiom:
∀alpha : set, ordinal alpha → ∀beta ∈ alpha, ordinal beta
Axiom. (TransSet_ordsucc) We take the following as an axiom:
∀X : set, TransSet X → TransSet (ordsucc X)
Axiom. (ordinal_ordsucc) We take the following as an axiom:
∀alpha : set, ordinal alpha → ordinal (ordsucc alpha)
Axiom. (nat_p_ordinal) We take the following as an axiom:
∀n : set, nat_p n → ordinal n
Axiom. (ordinal_1) We take the following as an axiom:
ordinal 1
Axiom. (ordinal_2) We take the following as an axiom:
ordinal 2
Axiom. (omega_TransSet) We take the following as an axiom:
TransSet ω
Axiom. (omega_ordinal) We take the following as an axiom:
ordinal ω
Axiom. (ordsucc_omega_ordinal) We take the following as an axiom:
ordinal (ordsucc ω)
Axiom. (TransSet_ordsucc_In_Subq) We take the following as an axiom:
∀X : set, TransSet X → ∀x ∈ X, ordsucc x ⊆ X
Axiom. (ordinal_ordsucc_In_Subq) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta ∈ alpha, ordsucc beta ⊆ alpha
Axiom. (ordinal_trichotomy_or) We take the following as an axiom:
∀alpha beta : set, ordinal alpha → ordinal beta → alpha ∈ beta ∨ alpha = beta ∨ beta ∈ alpha
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
Axiom. (ordinal_In_Or_Subq) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha ∈ beta ∨ beta ⊆ alpha
Axiom. (ordinal_linear) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta ∨ beta ⊆ alpha
Axiom. (ordinal_ordsucc_In_eq) We take the following as an axiom:
∀alpha beta, ordinal alpha → beta ∈ alpha → ordsucc beta ∈ alpha ∨ alpha = ordsucc beta
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)
Axiom. (ordinal_ordsucc_In) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta ∈ alpha, ordsucc beta ∈ ordsucc alpha
Axiom. (ordinal_famunion) We take the following as an axiom:
∀X, ∀F : set → set, (∀x ∈ X, ordinal (F x)) → ordinal (⋃x ∈ XF x)
Axiom. (ordinal_binintersect) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → ordinal (alpha ∩ beta)
Axiom. (ordinal_binunion) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → ordinal (alpha ∪ beta)
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
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
Definition. We define inj to be λX Y f ⇒ (∀u ∈ X, f u ∈ Y) ∧ (∀u v ∈ X, f u = f v → u = v) of type set → set → (set → set) → prop.
Definition. We define bij to be λX Y f ⇒ (∀u ∈ X, f u ∈ Y) ∧ (∀u v ∈ X, f u = f v → u = v) ∧ (∀w ∈ Y, ∃u ∈ X, f u = w) of type set → set → (set → set) → prop.
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
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
Object. The name inv is a term of type set → (set → set) → set → set.
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
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
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)
Axiom. (bij_id) We take the following as an axiom:
∀X, bij X X (λx ⇒ x)
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))
Definition. We define equip to be λX Y : set ⇒ ∃f : set → set, bij X Y f of type set → set → prop.
Axiom. (equip_ref) We take the following as an axiom:
∀X, equip X X
Axiom. (equip_sym) We take the following as an axiom:
∀X Y, equip X Y → equip Y X
Axiom. (equip_tra) We take the following as an axiom:
∀X Y Z, equip X Y → equip Y Z → equip X Z
Axiom. (equip_0_Empty) We take the following as an axiom:
∀X, equip X 0 → X = 0
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
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
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}
Axiom. (setminus_antimonotone) We take the following as an axiom:
∀A U V, U ⊆ V → A ∖ V ⊆ A ∖ U
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
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)
Axiom. (PigeonHole_nat_bij) We take the following as an axiom:
∀n, nat_p n → ∀f : set → set, (∀i ∈ n, f i ∈ n) → (∀i j ∈ n, f i = f j → i = j) → bij n n f
End of Section PigeonHole
Definition. We define finite to be λX ⇒ ∃n ∈ ω, equip X n of type set → prop.
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
Axiom. (finite_Empty) We take the following as an axiom:
finite 0
Axiom. (adjoin_finite) We take the following as an axiom:
∀X y, finite X → finite (X ∪ {y})
Axiom. (binunion_finite) We take the following as an axiom:
∀X, finite X → ∀Y, finite Y → finite (X ∪ Y)
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)
Axiom. (Subq_finite) We take the following as an axiom:
∀X, finite X → ∀Y, Y ⊆ X → finite Y
Axiom. (TransSet_In_ordsucc_Subq) We take the following as an axiom:
∀x y, TransSet y → x ∈ ordsucc y → x ⊆ y
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
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
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
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
Beginning of Section Descr_ii
Variable P : (set → set) → prop
Object. The name Descr_ii is a term of type set → set.
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
End of Section Descr_ii
Beginning of Section Descr_iii
Variable P : (set → set → set) → prop
Object. The name Descr_iii is a term of type set → set → set.
Hypothesis Pex : ∃f : set → set → set, P f
Hypothesis Puniq : ∀f g : set → set → set, P f → P g → f = g
Axiom. (Descr_iii_prop) We take the following as an axiom:
P Descr_iii
End of Section Descr_iii
Beginning of Section Descr_Vo1
Variable P : Vo 1 → prop
Object. The name Descr_Vo1 is a term of type Vo 1.
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
End of Section Descr_Vo1
Beginning of Section If_ii
Variable p : prop
Variable f g : set → set
Object. The name If_ii is a term of type set → set.
Axiom. (If_ii_1) We take the following as an axiom:
p → If_ii = f
Axiom. (If_ii_0) We take the following as an axiom:
¬ p → If_ii = g
End of Section If_ii
Beginning of Section If_iii
Variable p : prop
Variable f g : set → set → set
Object. The name If_iii is a term of type set → set → set.
Axiom. (If_iii_1) We take the following as an axiom:
p → If_iii = f
Axiom. (If_iii_0) We take the following as an axiom:
¬ p → If_iii = g
End of Section If_iii
Beginning of Section EpsilonRec_i
Variable F : set → (set → set) → set
Object. The name In_rec_i is a term of type set → set.
Hypothesis Fr : ∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h
Axiom. (In_rec_i_eq) We take the following as an axiom:
∀X : set, In_rec_i X = F X In_rec_i
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
Variable F : set → (set → (set → set)) → (set → set)
Object. The name In_rec_ii is a term of type set → (set → set).
Hypothesis Fr : ∀X : set, ∀g h : set → (set → set), (∀x ∈ X, g x = h x) → F X g = F X h
Axiom. (In_rec_ii_eq) We take the following as an axiom:
∀X : set, In_rec_ii X = F X In_rec_ii
End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
Variable F : set → (set → (set → set → set)) → (set → set → set)
Object. The name In_rec_iii is a term of type set → (set → set → set).
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_iii_eq) We take the following as an axiom:
∀X : set, In_rec_iii X = F X In_rec_iii
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.
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
Axiom. (nat_primrec_0) We take the following as an axiom:
nat_primrec 0 = z
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)
End of Section NatRec
Beginning of Section NatArith
Definition. We define add_nat to be λn m : set ⇒ nat_primrec n (λ_ r ⇒ ordsucc r) m of type set → set → set.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
Axiom. (add_nat_0R) We take the following as an axiom:
∀n : set, n + 0 = n
Axiom. (add_nat_SR) We take the following as an axiom:
∀n m : set, nat_p m → n + ordsucc m = ordsucc (n + m)
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)
Axiom. (add_nat_1_1_2) We take the following as an axiom:
1 + 1 = 2
Definition. We define mul_nat to be λn m : set ⇒ nat_primrec 0 (λ_ r ⇒ n + r) m of type set → set → set.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.
Axiom. (mul_nat_0R) We take the following as an axiom:
∀n : set, n * 0 = 0
Axiom. (mul_nat_SR) We take the following as an axiom:
∀n m : set, nat_p m → n * ordsucc m = n + n * m
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)
End of Section NatArith
Definition. We define Inj1 to be In_rec_i (λX f ⇒ {0} ∪ {f x|x ∈ X}) of type set → set.
Axiom. (Inj1_eq) We take the following as an axiom:
∀X : set, Inj1 X = {0} ∪ {Inj1 x|x ∈ X}
Axiom. (Inj1I1) We take the following as an axiom:
∀X : set, 0 ∈ Inj1 X
Axiom. (Inj1I2) We take the following as an axiom:
∀X x : set, x ∈ X → Inj1 x ∈ Inj1 X
Axiom. (Inj1E) We take the following as an axiom:
∀X y : set, y ∈ Inj1 X → y = 0 ∨ ∃x ∈ X, y = Inj1 x
Axiom. (Inj1NE1) We take the following as an axiom:
∀x : set, Inj1 x ≠ 0
Axiom. (Inj1NE2) We take the following as an axiom:
∀x : set, Inj1 x ∉ {0}
Definition. We define Inj0 to be λX ⇒ {Inj1 x|x ∈ X} of type set → set.
Axiom. (Inj0I) We take the following as an axiom:
∀X x : set, x ∈ X → Inj1 x ∈ Inj0 X
Axiom. (Inj0E) We take the following as an axiom:
∀X y : set, y ∈ Inj0 X → ∃x : set, x ∈ X ∧ y = Inj1 x
Definition. We define Unj to be In_rec_i (λX f ⇒ {f x|x ∈ X ∖ {0}}) of type set → set.
Axiom. (Unj_eq) We take the following as an axiom:
∀X : set, Unj X = {Unj x|x ∈ X ∖ {0}}
Axiom. (Unj_Inj1_eq) We take the following as an axiom:
∀X : set, Unj (Inj1 X) = X
Axiom. (Inj1_inj) We take the following as an axiom:
∀X Y : set, Inj1 X = Inj1 Y → X = Y
Axiom. (Unj_Inj0_eq) We take the following as an axiom:
∀X : set, Unj (Inj0 X) = X
Axiom. (Inj0_inj) We take the following as an axiom:
∀X Y : set, Inj0 X = Inj0 Y → X = Y
Axiom. (Inj0_0) We take the following as an axiom:
Inj0 0 = 0
Axiom. (Inj0_Inj1_neq) We take the following as an axiom:
∀X Y : set, Inj0 X ≠ Inj1 Y
Definition. We define setsum to be λX Y ⇒ {Inj0 x|x ∈ X} ∪ {Inj1 y|y ∈ Y} of type set → set → set.
Notation. We use + as an infix operator with priority 450 and which associates to the left corresponding to applying term setsum.
Axiom. (Inj0_setsum) We take the following as an axiom:
∀X Y x : set, x ∈ X → Inj0 x ∈ X + Y
Axiom. (Inj1_setsum) We take the following as an axiom:
∀X Y y : set, y ∈ Y → Inj1 y ∈ X + Y
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)
Axiom. (Inj0_setsum_0L) We take the following as an axiom:
∀X : set, 0 + X = Inj0 X
Axiom. (Subq_1_Sing0) We take the following as an axiom:
1 ⊆ {0}
Axiom. (Inj1_setsum_1L) We take the following as an axiom:
∀X : set, 1 + X = Inj1 X
Axiom. (nat_setsum1_ordsucc) We take the following as an axiom:
∀n : set, nat_p n → 1 + n = ordsucc n
Axiom. (setsum_0_0) We take the following as an axiom:
0 + 0 = 0
Axiom. (setsum_1_0_1) We take the following as an axiom:
1 + 0 = 1
Axiom. (setsum_1_1_2) We take the following as an axiom:
1 + 1 = 2
Beginning of Section pair_setsum
Let pair ≝ setsum
Definition. We define proj0 to be λZ ⇒ {Unj z|z ∈ Z, ∃x : set, Inj0 x = z} of type set → set.
Definition. We define proj1 to be λZ ⇒ {Unj z|z ∈ Z, ∃y : set, Inj1 y = z} of type set → set.
Axiom. (Inj0_pair_0_eq) We take the following as an axiom:
Inj0 = pair 0
Axiom. (Inj1_pair_1_eq) We take the following as an axiom:
Inj1 = pair 1
Axiom. (pairI0) We take the following as an axiom:
∀X Y x, x ∈ X → pair 0 x ∈ pair X Y
Axiom. (pairI1) We take the following as an axiom:
∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y
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)
Axiom. (pairE0) We take the following as an axiom:
∀X Y x, pair 0 x ∈ pair X Y → x ∈ X
Axiom. (pairE1) We take the following as an axiom:
∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y
Axiom. (proj0I) We take the following as an axiom:
∀w u : set, pair 0 u ∈ w → u ∈ proj0 w
Axiom. (proj0E) We take the following as an axiom:
∀w u : set, u ∈ proj0 w → pair 0 u ∈ w
Axiom. (proj1I) We take the following as an axiom:
∀w u : set, pair 1 u ∈ w → u ∈ proj1 w
Axiom. (proj1E) We take the following as an axiom:
∀w u : set, u ∈ proj1 w → pair 1 u ∈ w
Axiom. (proj0_pair_eq) We take the following as an axiom:
∀X Y : set, proj0 (pair X Y) = X
Axiom. (proj1_pair_eq) We take the following as an axiom:
∀X Y : set, proj1 (pair X Y) = Y
Definition. We define Sigma to be λX Y ⇒ ⋃x ∈ X{pair x y|y ∈ Y x} of type set → (set → set) → set.
Notation. We use ∑ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Sigma.
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
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)
Axiom. (proj_Sigma_eta) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z ∈ (∑x ∈ X, Y x), pair (proj0 z) (proj1 z) = z
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
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)
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
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
Definition. We define setprod to be λX Y : set ⇒ ∑x ∈ X, Y of type set → set → set.
Notation. We use ⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.
Let lam : set → (set → set) → set ≝ Sigma
Definition. We define ap to be λf x ⇒ {proj1 z|z ∈ f, ∃y : set, z = pair x y} of type set → set → set.
Notation. When x is a set, a term x y is notation for ap x y.
Notation. λ x ∈ A ⇒ B is notation for the set Sigma A (λ x : set ⇒ B).
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
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
Axiom. (apI) We take the following as an axiom:
∀f x y, pair x y ∈ f → y ∈ f x
Axiom. (apE) We take the following as an axiom:
∀f x y, y ∈ f x → pair x y ∈ f
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
Axiom. (proj0_ap_0) We take the following as an axiom:
∀u, proj0 u = u 0
Axiom. (proj1_ap_1) We take the following as an axiom:
∀u, proj1 u = u 1
Axiom. (pair_ap_0) We take the following as an axiom:
∀x y : set, (pair x y) 0 = x
Axiom. (pair_ap_1) We take the following as an axiom:
∀x y : set, (pair x y) 1 = y
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
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))
Definition. We define pair_p to be λu : set ⇒ pair (u 0) (u 1) = u of type set → prop.
Axiom. (pair_p_I) We take the following as an axiom:
∀x y, pair_p (pair x y)
Axiom. (Subq_2_UPair01) We take the following as an axiom:
2 ⊆ {0,1}
Axiom. (tuple_pair) We take the following as an axiom:
∀x y : set, pair x y = (x,y)
Definition. We define Pi to be λX Y ⇒ {f ∈ 𝒫 (∑x ∈ X, ⋃ (Y x))|∀x ∈ X, f x ∈ Y x} of type set → (set → set) → set.
Notation. We use ∏ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Pi.
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
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)
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
Definition. We define setexp to be λX Y : set ⇒ ∏y ∈ Y, X of type set → set → set.
Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.
Axiom. (pair_tuple_fun) We take the following as an axiom:
pair = (λx y ⇒ (x,y))
Axiom. (lamI2) We take the following as an axiom:
∀X, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, (x,y) ∈ λx ∈ X ⇒ F x
Beginning of Section Tuples
Variable x0 x1 : set
Axiom. (tuple_2_0_eq) We take the following as an axiom:
(x0,x1) 0 = x0
Axiom. (tuple_2_1_eq) We take the following as an axiom:
(x0,x1) 1 = x1
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}
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
Axiom. (tuple_2_setprod) We take the following as an axiom:
∀X : set, ∀Y : set, ∀x ∈ X, ∀y ∈ Y, (x,y) ∈ X ⨯ Y
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.
Object. The name DescrR_i_io_1 is a term of type (set → (set → prop) → prop) → set.
Object. The name DescrR_i_io_2 is a term of type (set → (set → prop) → prop) → set → prop.
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)
Definition. We define PNoEq_ to be λalpha p q ⇒ ∀beta ∈ alpha, p beta ↔ q beta of type set → (set → prop) → (set → prop) → prop.
Axiom. (PNoEq_ref_) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoEq_ alpha p p
Axiom. (PNoEq_sym_) We take the following as an axiom:
∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoEq_ alpha q p
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
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
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.
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
Axiom. (PNoLt_irref_) We take the following as an axiom:
∀alpha, ∀p : set → prop, ¬ PNoLt_ alpha p p
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
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
Axiom. (PNoLt_tra_) We take the following as an axiom:
∀alpha, ordinal alpha → ∀p q r : set → prop, PNoLt_ alpha p q → PNoLt_ alpha q r → PNoLt_ alpha p r
Object. The name PNoLt is a term of type set → (set → prop) → set → (set → prop) → prop.
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
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
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
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
Axiom. (PNoLt_irref) We take the following as an axiom:
∀alpha, ∀p : set → prop, ¬ PNoLt alpha p alpha p
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
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
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
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
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.
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
Axiom. (PNoLeI2) We take the following as an axiom:
∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoLe alpha p alpha q
Axiom. (PNoLe_ref) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoLe alpha p alpha p
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
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
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
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
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
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.
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.
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
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
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
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
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.
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)
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.
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.
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.
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
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
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
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
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
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
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.
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.
Axiom. (PNo_extend0_eq) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta ∧ delta ≠ alpha)
Axiom. (PNo_extend1_eq) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta ∨ delta = alpha)
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)
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.
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)
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)
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
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
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.
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.
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.
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
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
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
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
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
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
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
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
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.
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.
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
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)
Object. The name PNo_bd is a term of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set.
Object. The name PNo_pred is a term of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → prop.
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)
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)
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
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}
Axiom. (not_ordinal_Sing1) We take the following as an axiom:
¬ ordinal {1}
Axiom. (tagged_not_ordinal) We take the following as an axiom:
∀y, ¬ ordinal (y ')
Axiom. (tagged_notin_ordinal) We take the following as an axiom:
∀alpha y, ordinal alpha → (y ') ∉ alpha
Axiom. (tagged_eqE_Subq) We take the following as an axiom:
∀alpha beta, ordinal alpha → alpha ' = beta ' → alpha ⊆ beta
Axiom. (tagged_eqE_eq) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha ' = beta ' → alpha = beta
Axiom. (tagged_ReplE) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → beta ' ∈ {gamma '|gamma ∈ alpha} → beta ∈ alpha
Axiom. (ordinal_notin_tagged_Repl) We take the following as an axiom:
∀alpha Y, ordinal alpha → alpha ∉ {y '|y ∈ Y}
Definition. We define SNoElts_ to be λalpha ⇒ alpha ∪ {beta '|beta ∈ alpha} of type set → set.
Axiom. (SNoElts_mon) We take the following as an axiom:
∀alpha beta, alpha ⊆ beta → SNoElts_ alpha ⊆ SNoElts_ beta
Definition. We define SNo_ to be λalpha x ⇒ x ⊆ SNoElts_ alpha ∧ ∀beta ∈ alpha, exactly1of2 (beta ' ∈ x) (beta ∈ x) of type set → set → prop.
Definition. We define PSNo to be λalpha p ⇒ {beta ∈ alpha|p beta} ∪ {beta '|beta ∈ alpha, ¬ p beta} of type set → (set → prop) → set.
Axiom. (PNoEq_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha → ∀p : set → prop, PNoEq_ alpha (λbeta ⇒ beta ∈ PSNo alpha p) p
Axiom. (SNo_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha → ∀p : set → prop, SNo_ alpha (PSNo alpha p)
Axiom. (SNo_PSNo_eta_) We take the following as an axiom:
∀alpha x, ordinal alpha → SNo_ alpha x → x = PSNo alpha (λbeta ⇒ beta ∈ x)
Object. The name SNo is a term of type set → prop.
Axiom. (SNo_SNo) We take the following as an axiom:
∀alpha, ordinal alpha → ∀z, SNo_ alpha z → SNo z
Object. The name SNoLev is a term of type set → set.
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
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
Axiom. (SNoLev_prop) We take the following as an axiom:
∀x, SNo x → ordinal (SNoLev x) ∧ SNo_ (SNoLev x) x
Axiom. (SNoLev_ordinal) We take the following as an axiom:
∀x, SNo x → ordinal (SNoLev x)
Axiom. (SNoLev_) We take the following as an axiom:
∀x, SNo x → SNo_ (SNoLev x) x
Axiom. (SNo_PSNo_eta) We take the following as an axiom:
∀x, SNo x → x = PSNo (SNoLev x) (λbeta ⇒ beta ∈ x)
Axiom. (SNoLev_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha → ∀p : set → prop, SNoLev (PSNo alpha p) = alpha
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
Definition. We define SNoEq_ to be λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ y) of type set → set → set → prop.
Axiom. (SNoEq_I) We take the following as an axiom:
∀alpha x y, (∀beta ∈ alpha, beta ∈ x ↔ beta ∈ y) → SNoEq_ alpha x y
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
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.
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.
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
Axiom. (SNoLeE) We take the following as an axiom:
∀x y, SNo x → SNo y → x ≤ y → x < y ∨ x = y
Axiom. (SNoEq_sym_) We take the following as an axiom:
∀alpha x y, SNoEq_ alpha x y → SNoEq_ alpha y x
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
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
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
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
Axiom. (SNoLt_irref) We take the following as an axiom:
∀x, ¬ SNoLt x x
Axiom. (SNoLt_trichotomy_or) We take the following as an axiom:
∀x y, SNo x → SNo y → x < y ∨ x = y ∨ y < x
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
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
Axiom. (SNoLe_ref) We take the following as an axiom:
∀x, SNoLe x x
Axiom. (SNoLe_antisym) We take the following as an axiom:
∀x y, SNo x → SNo y → x ≤ y → y ≤ x → x = y
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
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
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
Axiom. (SNoLtLe_or) We take the following as an axiom:
∀x y, SNo x → SNo y → x < y ∨ y ≤ x
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
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
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.
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.
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)
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
Axiom. (SNoCutP_L_0) We take the following as an axiom:
∀L, (∀x ∈ L, SNo x) → SNoCutP L 0
Axiom. (SNoCutP_0_R) We take the following as an axiom:
∀R, (∀x ∈ R, SNo x) → SNoCutP 0 R
Axiom. (SNoCutP_0_0) We take the following as an axiom:
SNoCutP 0 0
Definition. We define SNoS_ to be λalpha ⇒ {x ∈ 𝒫 (SNoElts_ alpha)|∃beta ∈ alpha, SNo_ beta x} of type set → set.
Axiom. (SNoS_E) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, ∃beta ∈ alpha, SNo_ beta x
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
Axiom. (SNoS_I2) We take the following as an axiom:
∀x y, SNo x → SNo y → SNoLev x ∈ SNoLev y → x ∈ SNoS_ (SNoLev y)
Axiom. (SNoS_Subq) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta → SNoS_ alpha ⊆ SNoS_ beta
Axiom. (SNoLev_uniq2) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x, SNo_ alpha x → SNoLev x = alpha
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
Axiom. (SNoS_In_neq) We take the following as an axiom:
∀w, SNo w → ∀x ∈ SNoS_ (SNoLev w), x ≠ w
Axiom. (SNoS_SNoLev) We take the following as an axiom:
∀z, SNo z → z ∈ SNoS_ (ordsucc (SNoLev z))
Definition. We define SNoL to be λz ⇒ {x ∈ SNoS_ (SNoLev z)|x < z} of type set → set.
Definition. We define SNoR to be λz ⇒ {y ∈ SNoS_ (SNoLev z)|z < y} of type set → set.
Axiom. (SNoCutP_SNoL_SNoR) We take the following as an axiom:
∀z, SNo z → SNoCutP (SNoL z) (SNoR z)
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
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
Axiom. (SNoL_SNoS_) We take the following as an axiom:
∀z, SNoL z ⊆ SNoS_ (SNoLev z)
Axiom. (SNoR_SNoS_) We take the following as an axiom:
∀z, SNoR z ⊆ SNoS_ (SNoLev z)
Axiom. (SNoL_SNoS) We take the following as an axiom:
∀x, SNo x → ∀w ∈ SNoL x, w ∈ SNoS_ (SNoLev x)
Axiom. (SNoR_SNoS) We take the following as an axiom:
∀x, SNo x → ∀z ∈ SNoR x, z ∈ SNoS_ (SNoLev x)
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
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
Axiom. (SNo_eta) We take the following as an axiom:
∀z, SNo z → z = SNoCut (SNoL z) (SNoR z)
Axiom. (SNoCutP_SNo_SNoCut) We take the following as an axiom:
∀L R, SNoCutP L R → SNo (SNoCut L R)
Axiom. (SNoCutP_SNoCut_L) We take the following as an axiom:
∀L R, SNoCutP L R → ∀x ∈ L, x < SNoCut L R
Axiom. (SNoCutP_SNoCut_R) We take the following as an axiom:
∀L R, SNoCutP L R → ∀y ∈ R, SNoCut L R < y
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
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
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
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
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
Axiom. (ordinal_SNo_) We take the following as an axiom:
∀alpha, ordinal alpha → SNo_ alpha alpha
Axiom. (ordinal_SNo) We take the following as an axiom:
∀alpha, ordinal alpha → SNo alpha
Axiom. (ordinal_SNoLev) We take the following as an axiom:
∀alpha, ordinal alpha → SNoLev alpha = alpha
Axiom. (ordinal_SNoLev_max) We take the following as an axiom:
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ alpha → z < alpha
Axiom. (ordinal_SNoL) We take the following as an axiom:
∀alpha, ordinal alpha → SNoL alpha = SNoS_ alpha
Axiom. (ordinal_SNoR) We take the following as an axiom:
∀alpha, ordinal alpha → SNoR alpha = Empty
Axiom. (nat_p_SNo) We take the following as an axiom:
∀n, nat_p n → SNo n
Axiom. (omega_SNo) We take the following as an axiom:
∀n ∈ ω, SNo n
Axiom. (omega_SNoS_omega) We take the following as an axiom:
ω ⊆ SNoS_ ω
Axiom. (ordinal_In_SNoLt) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta ∈ alpha, beta < alpha
Axiom. (ordinal_SNoLev_max_2) We take the following as an axiom:
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ ordsucc alpha → z ≤ alpha
Axiom. (ordinal_Subq_SNoLe) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta → alpha ≤ beta
Axiom. (ordinal_SNoLt_In) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha < beta → alpha ∈ beta
Axiom. (omega_nonneg) We take the following as an axiom:
∀m ∈ ω, 0 ≤ m
Axiom. (SNo_0) We take the following as an axiom:
SNo 0
Axiom. (SNo_1) We take the following as an axiom:
SNo 1
Axiom. (SNo_2) We take the following as an axiom:
SNo 2
Axiom. (SNoLev_0) We take the following as an axiom:
SNoLev 0 = 0
Axiom. (SNoCut_0_0) We take the following as an axiom:
SNoCut 0 0 = 0
Axiom. (SNoL_0) We take the following as an axiom:
SNoL 0 = 0
Axiom. (SNoR_0) We take the following as an axiom:
SNoR 0 = 0
Axiom. (SNoL_1) We take the following as an axiom:
SNoL 1 = 1
Axiom. (SNoR_1) We take the following as an axiom:
SNoR 1 = 0
Axiom. (SNo_max_SNoLev) We take the following as an axiom:
∀x, SNo x → (∀y ∈ SNoS_ (SNoLev x), y < x) → SNoLev x = x
Axiom. (SNo_max_ordinal) We take the following as an axiom:
∀x, SNo x → (∀y ∈ SNoS_ (SNoLev x), y < x) → ordinal x
Definition. We define SNo_extend0 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta ∈ x ∧ delta ≠ SNoLev x) of type set → set.
Definition. We define SNo_extend1 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta ∈ x ∨ delta = SNoLev x) of type set → set.
Axiom. (SNo_extend0_SNo_) We take the following as an axiom:
∀x, SNo x → SNo_ (ordsucc (SNoLev x)) (SNo_extend0 x)
Axiom. (SNo_extend1_SNo_) We take the following as an axiom:
∀x, SNo x → SNo_ (ordsucc (SNoLev x)) (SNo_extend1 x)
Axiom. (SNo_extend0_SNo) We take the following as an axiom:
∀x, SNo x → SNo (SNo_extend0 x)
Axiom. (SNo_extend1_SNo) We take the following as an axiom:
∀x, SNo x → SNo (SNo_extend1 x)
Axiom. (SNo_extend0_SNoLev) We take the following as an axiom:
∀x, SNo x → SNoLev (SNo_extend0 x) = ordsucc (SNoLev x)
Axiom. (SNo_extend1_SNoLev) We take the following as an axiom:
∀x, SNo x → SNoLev (SNo_extend1 x) = ordsucc (SNoLev x)
Axiom. (SNo_extend0_nIn) We take the following as an axiom:
∀x, SNo x → SNoLev x ∉ SNo_extend0 x
Axiom. (SNo_extend1_In) We take the following as an axiom:
∀x, SNo x → SNoLev x ∈ SNo_extend1 x
Axiom. (SNo_extend0_SNoEq) We take the following as an axiom:
∀x, SNo x → SNoEq_ (SNoLev x) (SNo_extend0 x) x
Axiom. (SNo_extend1_SNoEq) We take the following as an axiom:
∀x, SNo x → SNoEq_ (SNoLev x) (SNo_extend1 x) x
Axiom. (SNoLev_0_eq_0) We take the following as an axiom:
∀x, SNo x → SNoLev x = 0 → x = 0
Definition. We define eps_ to be λn ⇒ {0} ∪ {(ordsucc m) '|m ∈ n} of type set → set.
Axiom. (eps_ordinal_In_eq_0) We take the following as an axiom:
∀n alpha, ordinal alpha → alpha ∈ eps_ n → alpha = 0
Axiom. (eps_0_1) We take the following as an axiom:
eps_ 0 = 1
Axiom. (SNo__eps_) We take the following as an axiom:
∀n ∈ ω, SNo_ (ordsucc n) (eps_ n)
Axiom. (SNo_eps_) We take the following as an axiom:
∀n ∈ ω, SNo (eps_ n)
Axiom. (SNo_eps_1) We take the following as an axiom:
SNo (eps_ 1)
Axiom. (SNoLev_eps_) We take the following as an axiom:
∀n ∈ ω, SNoLev (eps_ n) = ordsucc n
Axiom. (SNo_eps_SNoS_omega) We take the following as an axiom:
∀n ∈ ω, eps_ n ∈ SNoS_ ω
Axiom. (SNo_eps_decr) We take the following as an axiom:
∀n ∈ ω, ∀m ∈ n, eps_ n < eps_ m
Axiom. (SNo_eps_pos) We take the following as an axiom:
∀n ∈ ω, 0 < eps_ n
Axiom. (SNo_pos_eps_Lt) We take the following as an axiom:
∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc n), 0 < x → eps_ n < x
Axiom. (SNo_pos_eps_Le) We take the following as an axiom:
∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc (ordsucc n)), 0 < x → eps_ n ≤ x
Axiom. (eps_SNo_eq) We take the following as an axiom:
∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc n), 0 < x → SNoEq_ (SNoLev x) (eps_ n) x → ∃m ∈ n, x = eps_ m
Axiom. (eps_SNoCutP) We take the following as an axiom:
∀n ∈ ω, SNoCutP {0} {eps_ m|m ∈ n}
Axiom. (eps_SNoCut) We take the following as an axiom:
∀n ∈ ω, eps_ n = SNoCut {0} {eps_ m|m ∈ n}
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
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
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)
Object. The name SNo_rec_i is a term of type set → set.
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
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)
Object. The name SNo_rec_ii is a term of type set → (set → set).
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
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
Object. The name SNo_rec2 is a term of type set → set → set.
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
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))
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
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)
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)
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)
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)
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
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
Axiom. (SNo_omega) We take the following as an axiom:
SNo ω
Axiom. (SNoLt_0_1) We take the following as an axiom:
0 < 1
Axiom. (SNoLt_0_2) We take the following as an axiom:
0 < 2
Axiom. (SNoLt_1_2) We take the following as an axiom:
1 < 2
Axiom. (restr_SNo_) We take the following as an axiom:
∀x, SNo x → ∀alpha ∈ SNoLev x, SNo_ alpha (x ∩ SNoElts_ alpha)
Axiom. (restr_SNo) We take the following as an axiom:
∀x, SNo x → ∀alpha ∈ SNoLev x, SNo (x ∩ SNoElts_ alpha)
Axiom. (restr_SNoLev) We take the following as an axiom:
∀x, SNo x → ∀alpha ∈ SNoLev x, SNoLev (x ∩ SNoElts_ alpha) = alpha
Axiom. (restr_SNoEq) We take the following as an axiom:
∀x, SNo x → ∀alpha ∈ SNoLev x, SNoEq_ alpha (x ∩ SNoElts_ alpha) x
Axiom. (SNo_extend0_restr_eq) We take the following as an axiom:
∀x, SNo x → x = SNo_extend0 x ∩ SNoElts_ (SNoLev x)
Axiom. (SNo_extend1_restr_eq) We take the following as an axiom:
∀x, SNo x → x = SNo_extend1 x ∩ SNoElts_ (SNoLev x)

Part 4

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.
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.
Theorem. (minus_SNo_eq) The following is provable:
∀x, SNo x → - x = SNoCut {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
Proof:
We prove the intermediate claim L1: ∀x, SNo x → ∀g h : set → set, (∀w ∈ SNoS_ (SNoLev x), g w = h w) → SNoCut {g z|z ∈ SNoR x} {g w|w ∈ SNoL x} = SNoCut {h z|z ∈ SNoR x} {h w|w ∈ SNoL x}.
Let x be given.
Assume Hx: SNo x.
Let g and h be given.
Assume Hgh: ∀w ∈ SNoS_ (SNoLev x), g w = h w.
We will prove SNoCut {g z|z ∈ SNoR x} {g w|w ∈ SNoL x} = SNoCut {h z|z ∈ SNoR x} {h w|w ∈ SNoL x}.
We prove the intermediate claim L1a: {g z|z ∈ SNoR x} = {h z|z ∈ SNoR x}.
Apply ReplEq_ext to the current goal.
Let z be given.
Assume Hz: z ∈ SNoR x.
We will prove g z = h z.
Apply Hgh to the current goal.
We will prove z ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoR_SNoS x Hx z Hz.
We prove the intermediate claim L1b: {g w|w ∈ SNoL x} = {h w|w ∈ SNoL x}.
Apply ReplEq_ext to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL x.
We will prove g w = h w.
Apply Hgh to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoL_SNoS x Hx w Hw.
rewrite the current goal using L1a (from left to right).
rewrite the current goal using L1b (from left to right).
Use reflexivity.
An exact proof term for the current goal is SNo_rec_i_eq (λx m ⇒ SNoCut {m z|z ∈ SNoR x} {m w|w ∈ SNoL x}) L1.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Main Goal
Theorem. (minus_SNo_prop1) The following is provable:
∀x, SNo x → SNo (- x) ∧ (∀u ∈ SNoL x, - x < - u) ∧ (∀u ∈ SNoR x, - u < - x) ∧ SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
Proof:
Apply SNoLev_ind to the current goal.
Let x be given.
Assume Hx: SNo x.
Assume IH: ∀w ∈ SNoS_ (SNoLev x), SNo (- w) ∧ (∀u ∈ SNoL w, - w < - u) ∧ (∀u ∈ SNoR w, - u < - w) ∧ SNoCutP {- z|z ∈ SNoR w} {- v|v ∈ SNoL w}.
We prove the intermediate claim IHLx: ∀w ∈ SNoL x, SNo (- w) ∧ (∀u ∈ SNoL w, - w < - u) ∧ (∀u ∈ SNoR w, - u < - w).
Let w be given.
Assume Hw: w ∈ SNoL x.
Apply SNoL_E x Hx w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev x.
Assume Hw3: w < x.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
Apply IH w Lw to the current goal.
Assume H _.
An exact proof term for the current goal is H.
We prove the intermediate claim IHRx: ∀z ∈ SNoR x, SNo (- z) ∧ (∀u ∈ SNoL z, - z < - u) ∧ (∀u ∈ SNoR z, - u < - z).
Let w be given.
Assume Hw: w ∈ SNoR x.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev x.
Assume Hw3: x < w.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
Apply IH w Lw to the current goal.
Assume H _.
An exact proof term for the current goal is H.
Set L to be the term {- z|z ∈ SNoR x}.
Set R to be the term {- w|w ∈ SNoL x}.
We prove the intermediate claim LLR: SNoCutP L R.
We will prove (∀w ∈ L, SNo w) ∧ (∀z ∈ R, SNo z) ∧ (∀w ∈ L, ∀z ∈ R, w < z).
Apply and3I to the current goal.
Let w be given.
Assume Hw: w ∈ L.
We will prove SNo w.
Apply ReplE_impred (SNoR x) (λz ⇒ - z) w Hw to the current goal.
Let z be given.
Assume Hz: z ∈ SNoR x.
Assume Hwz: w = - z.
Apply IHRx z Hz to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: SNo (- z).
Assume _ _.
We will prove SNo w.
rewrite the current goal using Hwz (from left to right).
An exact proof term for the current goal is H2.
Let z be given.
Assume Hz: z ∈ R.
We will prove SNo z.
Apply ReplE_impred (SNoL x) (λw ⇒ - w) z Hz to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL x.
Assume Hzw: z = - w.
Apply IHLx w Hw to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: SNo (- w).
Assume _ _.
We will prove SNo z.
rewrite the current goal using Hzw (from left to right).
An exact proof term for the current goal is H2.
Let w be given.
Assume Hw: w ∈ L.
Let z be given.
Assume Hz: z ∈ R.
Apply ReplE_impred (SNoR x) (λz ⇒ - z) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR x.
Assume Hwu: w = - u.
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: x < u.
Apply SNoLev_prop u Hu1 to the current goal.
Assume Hu1a: ordinal (SNoLev u).
Assume Hu1b: SNo_ (SNoLev u) u.
Apply ReplE_impred (SNoL x) (λw ⇒ - w) z Hz to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL x.
Assume Hzv: z = - v.
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: v < x.
Apply SNoLev_prop v Hv1 to the current goal.
Assume Hv1a: ordinal (SNoLev v).
Assume Hv1b: SNo_ (SNoLev v) v.
Apply IHLx v Hv to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: SNo (- v).
Assume H3: ∀u ∈ SNoL v, - v < - u.
Assume H4: ∀u ∈ SNoR v, - u < - v.
Apply IHRx u Hu to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: SNo (- u).
Assume H6: ∀v ∈ SNoL u, - u < - v.
Assume H7: ∀v ∈ SNoR u, - v < - u.
We will prove w < z.
rewrite the current goal using Hwu (from left to right).
rewrite the current goal using Hzv (from left to right).
We will prove - u < - v.
We prove the intermediate claim Lvu: v < u.
An exact proof term for the current goal is SNoLt_tra v x u Hv1 Hx Hu1 Hv3 Hu3.
Apply SNoLtE v u Hv1 Hu1 Lvu to the current goal.
Let z be given.
Assume Hz: SNo z.
Assume Hz1: SNoLev z ∈ SNoLev v ∩ SNoLev u.
Assume Hz2: SNoEq_ (SNoLev z) z v.
Assume Hz3: SNoEq_ (SNoLev z) z u.
Assume Hz4: v < z.
Assume Hz5: z < u.
Assume Hz6: SNoLev z ∉ v.
Assume Hz7: SNoLev z ∈ u.
Apply SNoLev_prop z Hz to the current goal.
Assume Hza: ordinal (SNoLev z).
Assume Hzb: SNo_ (SNoLev z) z.
Apply binintersectE (SNoLev v) (SNoLev u) (SNoLev z) Hz1 to the current goal.
Assume Hz1a: SNoLev z ∈ SNoLev v.
Assume Hz1b: SNoLev z ∈ SNoLev u.
We prove the intermediate claim LzLx: z ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 z x Hz Hx to the current goal.
We will prove SNoLev z ∈ SNoLev x.
Apply SNoLev_ordinal x Hx to the current goal.
Assume Hx2: TransSet (SNoLev x).
Assume _.
An exact proof term for the current goal is Hx2 (SNoLev u) Hu2 (SNoLev z) Hz1b.
We prove the intermediate claim Lmz: SNo (- z).
Apply IH z LzLx to the current goal.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume H _ _ _.
An exact proof term for the current goal is H.
We will prove - u < - v.
Apply SNoLt_tra (- u) (- z) (- v) H5 Lmz H2 to the current goal.
We will prove - u < - z.
Apply H6 to the current goal.
We will prove z ∈ SNoL u.
We will prove z ∈ {x ∈ SNoS_ (SNoLev u)|x < u}.
Apply SepI to the current goal.
We will prove z ∈ SNoS_ (SNoLev u).
Apply SNoS_I2 z u Hz Hu1 Hz1b to the current goal.
We will prove z < u.
An exact proof term for the current goal is Hz5.
We will prove - z < - v.
Apply H4 to the current goal.
We will prove z ∈ SNoR v.
We will prove z ∈ {x ∈ SNoS_ (SNoLev v)|v < x}.
Apply SepI to the current goal.
We will prove z ∈ SNoS_ (SNoLev v).
An exact proof term for the current goal is SNoS_I2 z v Hz Hv1 Hz1a.
We will prove v < z.
An exact proof term for the current goal is Hz4.
Assume H8: SNoLev v ∈ SNoLev u.
Assume H9: SNoEq_ (SNoLev v) v u.
Assume H10: SNoLev v ∈ u.
We will prove - u < - v.
Apply H6 to the current goal.
We will prove v ∈ SNoL u.
We will prove v ∈ {x ∈ SNoS_ (SNoLev u)|x < u}.
Apply SepI to the current goal.
We will prove v ∈ SNoS_ (SNoLev u).
An exact proof term for the current goal is SNoS_I2 v u Hv1 Hu1 H8.
We will prove v < u.
An exact proof term for the current goal is Lvu.
Assume H8: SNoLev u ∈ SNoLev v.
Assume H9: SNoEq_ (SNoLev u) v u.
Assume H10: SNoLev u ∉ v.
We will prove - u < - v.
Apply H4 to the current goal.
We will prove u ∈ SNoR v.
We will prove u ∈ {x ∈ SNoS_ (SNoLev v)|v < x}.
Apply SepI to the current goal.
We will prove u ∈ SNoS_ (SNoLev v).
An exact proof term for the current goal is SNoS_I2 u v Hu1 Hv1 H8.
We will prove v < u.
An exact proof term for the current goal is Lvu.
We prove the intermediate claim LNLR: SNo (SNoCut L R).
An exact proof term for the current goal is SNoCutP_SNo_SNoCut L R LLR.
Apply andI to the current goal.
rewrite the current goal using minus_SNo_eq x Hx (from left to right).
Apply and3I to the current goal.
We will prove SNo (SNoCut L R).
An exact proof term for the current goal is LNLR.
We will prove ∀u ∈ SNoL x, SNoCut L R < - u.
Let u be given.
Assume Hu: u ∈ SNoL x.
We will prove SNoCut L R < - u.
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: u < x.
We prove the intermediate claim LmuR: - u ∈ R.
Apply ReplI to the current goal.
We will prove u ∈ SNoL x.
An exact proof term for the current goal is Hu.
We will prove SNoCut L R < - u.
An exact proof term for the current goal is SNoCutP_SNoCut_R L R LLR (- u) LmuR.
We will prove ∀u ∈ SNoR x, - u < SNoCut L R.
Let u be given.
Assume Hu: u ∈ SNoR x.
We will prove - u < SNoCut L R.
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: x < u.
We prove the intermediate claim LmuL: - u ∈ L.
Apply ReplI to the current goal.
We will prove u ∈ SNoR x.
An exact proof term for the current goal is Hu.
We will prove - u < SNoCut L R.
An exact proof term for the current goal is SNoCutP_SNoCut_L L R LLR (- u) LmuL.
We will prove SNoCutP L R.
An exact proof term for the current goal is LLR.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Subgoal 7 Subgoal 8 Subgoal 9 Subgoal 10 Subgoal 11 Main Goal
Theorem. (SNo_minus_SNo) The following is provable:
∀x, SNo x → SNo (- x)
Proof:
Let x be given.
Assume Hx.
Apply minus_SNo_prop1 x Hx to the current goal.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume H _ _ _.
An exact proof term for the current goal is H.
∎
Try to prove it yourself. Main Goal
Theorem. (minus_SNo_Lt_contra) The following is provable:
∀x y, SNo x → SNo y → x < y → - y < - x
Proof:
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hxy: x < y.
Apply minus_SNo_prop1 x Hx to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: SNo (- x).
Assume H2: ∀u ∈ SNoL x, - x < - u.
Assume H3: ∀u ∈ SNoR x, - u < - x.
Assume _.
Apply minus_SNo_prop1 y Hy to the current goal.
Assume H4.
Apply H4 to the current goal.
Assume H4.
Apply H4 to the current goal.
Assume H4: SNo (- y).
Assume H5: ∀u ∈ SNoL y, - y < - u.
Assume H6: ∀u ∈ SNoR y, - u < - y.
Assume _.
Apply SNoLtE x y Hx Hy Hxy to the current goal.
Let z be given.
Assume Hz: SNo z.
Assume Hz1: SNoLev z ∈ SNoLev x ∩ SNoLev y.
Assume Hz2: SNoEq_ (SNoLev z) z x.
Assume Hz3: SNoEq_ (SNoLev z) z y.
Assume Hz4: x < z.
Assume Hz5: z < y.
Assume Hz6: SNoLev z ∉ x.
Assume Hz7: SNoLev z ∈ y.
Apply binintersectE (SNoLev x) (SNoLev y) (SNoLev z) Hz1 to the current goal.
Assume Hz1x Hz1y.
We will prove - y < - x.
Apply SNoLt_tra (- y) (- z) (- x) H4 (SNo_minus_SNo z Hz) H1 to the current goal.
We will prove - y < - z.
Apply H5 z to the current goal.
We will prove z ∈ SNoL y.
We will prove z ∈ {x ∈ SNoS_ (SNoLev y)|x < y}.
Apply SepI to the current goal.
We will prove z ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoS_I2 z y Hz Hy Hz1y.
We will prove z < y.
An exact proof term for the current goal is Hz5.
We will prove - z < - x.
Apply H3 z to the current goal.
We will prove z ∈ SNoR x.
We will prove z ∈ {z ∈ SNoS_ (SNoLev x)|x < z}.
Apply SepI to the current goal.
We will prove z ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 z x Hz Hx Hz1x.
We will prove x < z.
An exact proof term for the current goal is Hz4.
Assume H7: SNoLev x ∈ SNoLev y.
Assume H8: SNoEq_ (SNoLev x) x y.
Assume H9: SNoLev x ∈ y.
Apply H5 x to the current goal.
We will prove x ∈ SNoL y.
We will prove x ∈ {x ∈ SNoS_ (SNoLev y)|x < y}.
Apply SepI to the current goal.
We will prove x ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoS_I2 x y Hx Hy H7.
We will prove x < y.
An exact proof term for the current goal is Hxy.
Assume H7: SNoLev y ∈ SNoLev x.
Assume H8: SNoEq_ (SNoLev y) x y.
Assume H9: SNoLev y ∉ x.
We will prove - y < - x.
Apply H3 y to the current goal.
We will prove y ∈ SNoR x.
We will prove y ∈ {y ∈ SNoS_ (SNoLev x)|x < y}.
Apply SepI to the current goal.
We will prove y ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 y x Hy Hx H7.
We will prove x < y.
An exact proof term for the current goal is Hxy.
∎
Try to prove it yourself. Main Goal
Theorem. (minus_SNo_Le_contra) The following is provable:
∀x y, SNo x → SNo y → x ≤ y → - y ≤ - x
Proof:
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hxy: x ≤ y.
Apply SNoLeE x y Hx Hy Hxy to the current goal.
Assume H1: x < y.
We will prove - y ≤ - x.
Apply SNoLtLe to the current goal.
We will prove - y < - x.
An exact proof term for the current goal is minus_SNo_Lt_contra x y Hx Hy H1.
Assume H1: x = y.
We will prove - y ≤ - x.
rewrite the current goal using H1 (from left to right).
We will prove - y ≤ - y.
Apply SNoLe_ref to the current goal.
∎
Try to prove it yourself. Main Goal
Theorem. (minus_SNo_SNoCutP) The following is provable:
∀x, SNo x → SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
Proof:
Let x be given.
Assume Hx: SNo x.
Apply minus_SNo_prop1 x Hx to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume _ _ _ H1.
An exact proof term for the current goal is H1.
∎
Try to prove it yourself. Main Goal
Theorem. (minus_SNo_SNoCutP_gen) The following is provable:
∀L R, SNoCutP L R → SNoCutP {- z|z ∈ R} {- w|w ∈ L}
Proof:
Let L and R be given.
Assume HLR: SNoCutP L R.
Apply HLR to the current goal.
Assume H.
Apply H to the current goal.
Assume HLR1: ∀x ∈ L, SNo x.
Assume HLR2: ∀y ∈ R, SNo y.
Assume HLR3: ∀x ∈ L, ∀y ∈ R, x < y.
Set Lm to be the term {- z|z ∈ R}.
Set Rm to be the term {- w|w ∈ L}.
We will prove (∀w ∈ Lm, SNo w) ∧ (∀z ∈ Rm, SNo z) ∧ (∀w ∈ Lm, ∀z ∈ Rm, w < z).
Apply and3I to the current goal.
Let w be given.
Assume Hw: w ∈ Lm.
We will prove SNo w.
Apply ReplE_impred R (λz ⇒ - z) w Hw to the current goal.
Let z be given.
Assume Hz: z ∈ R.
Assume Hwz: w = - z.
rewrite the current goal using Hwz (from left to right).
We will prove SNo (- z).
Apply SNo_minus_SNo to the current goal.
Apply HLR2 to the current goal.
An exact proof term for the current goal is Hz.
Let z be given.
Assume Hz: z ∈ Rm.
We will prove SNo z.
Apply ReplE_impred L (λw ⇒ - w) z Hz to the current goal.
Let w be given.
Assume Hw: w ∈ L.
Assume Hzw: z = - w.
rewrite the current goal using Hzw (from left to right).
We will prove SNo (- w).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is HLR1 w Hw.
Let w be given.
Assume Hw: w ∈ Lm.
Let z be given.
Assume Hz: z ∈ Rm.
Apply ReplE_impred R (λz ⇒ - z) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ R.
Assume Hwu: w = - u.
Apply ReplE_impred L (λw ⇒ - w) z Hz to the current goal.
Let v be given.
Assume Hv: v ∈ L.
Assume Hzv: z = - v.
We will prove w < z.
rewrite the current goal using Hwu (from left to right).
rewrite the current goal using Hzv (from left to right).
We will prove - u < - v.
Apply minus_SNo_Lt_contra v u (HLR1 v Hv) (HLR2 u Hu) to the current goal.
We will prove v < u.
An exact proof term for the current goal is HLR3 v Hv u Hu.
∎
Try to prove it yourself. Main Goal
Theorem. (minus_SNo_Lev_lem1) The following is provable:
∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, SNoLev (- x) ⊆ SNoLev x
Proof:
Apply ordinal_ind to the current goal.
Let alpha be given.
Assume Ha: ordinal alpha.
Apply Ha to the current goal.
Assume Ha1 Ha2.
Assume IH: ∀beta ∈ alpha, ∀x ∈ SNoS_ beta, SNoLev (- x) ⊆ SNoLev x.
Let x be given.
Assume Hx: x ∈ SNoS_ alpha.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
Assume Hx1: SNoLev x ∈ alpha.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
Set L to be the term {- z|z ∈ SNoR x}.
Set R to be the term {- w|w ∈ SNoL x}.
We prove the intermediate claim LLR: SNoCutP L R.
An exact proof term for the current goal is minus_SNo_SNoCutP x Hx3.
We will prove SNoLev (- x) ⊆ SNoLev x.
rewrite the current goal using minus_SNo_eq x Hx3 (from left to right).
We will prove SNoLev (SNoCut L R) ⊆ SNoLev x.
Apply SNoCutP_SNoCut_impred L R LLR to the current goal.
Assume H2: SNo (SNoCut L R).
Assume H3: SNoLev (SNoCut L R) ∈ ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Assume _ _ _.
We prove the intermediate claim L3: ordinal ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Apply ordinal_binunion to the current goal.
Apply ordinal_famunion to the current goal.
Let w be given.
Assume Hw: w ∈ L.
We will prove ordinal (ordsucc (SNoLev w)).
Apply ReplE_impred (SNoR x) (λz ⇒ - z) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR x.
Assume Hwu: w = - u.
Apply SNoR_E x Hx3 u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: x < u.
Apply ordinal_ordsucc to the current goal.
We will prove ordinal (SNoLev w).
Apply SNoLev_ordinal to the current goal.
We will prove SNo w.
rewrite the current goal using Hwu (from left to right).
An exact proof term for the current goal is SNo_minus_SNo u Hu1.
Apply ordinal_famunion to the current goal.
Let w be given.
Assume Hw: w ∈ R.
We will prove ordinal (ordsucc (SNoLev w)).
Apply ReplE_impred (SNoL x) (λz ⇒ - z) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Assume Hwu: w = - u.
Apply SNoL_E x Hx3 u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: u < x.
Apply ordinal_ordsucc to the current goal.
We will prove ordinal (SNoLev w).
Apply SNoLev_ordinal to the current goal.
We will prove SNo w.
rewrite the current goal using Hwu (from left to right).
An exact proof term for the current goal is SNo_minus_SNo u Hu1.
We prove the intermediate claim L3a: TransSet ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Apply L3 to the current goal.
Assume H _.
An exact proof term for the current goal is H.
Let beta be given.
Assume Hb: beta ∈ SNoLev (SNoCut L R).
We prove the intermediate claim Lb: beta ∈ ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Apply ordsuccE ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))) (SNoLev (SNoCut L R)) H3 to the current goal.
Assume H4.
An exact proof term for the current goal is L3a (SNoLev (SNoCut L R)) H4 beta Hb.
Assume H4.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is Hb.
We will prove beta ∈ SNoLev x.
Apply binunionE (⋃x ∈ Lordsucc (SNoLev x)) (⋃y ∈ Rordsucc (SNoLev y)) beta Lb to the current goal.
Assume H4: beta ∈ ⋃x ∈ Lordsucc (SNoLev x).
Apply famunionE L (λx ⇒ ordsucc (SNoLev x)) beta H4 to the current goal.
Let w be given.
Assume Hw.
Apply Hw to the current goal.
Assume Hw1: w ∈ L.
Assume Hw2: beta ∈ ordsucc (SNoLev w).
We will prove beta ∈ SNoLev x.
Apply ReplE_impred (SNoR x) (λz ⇒ - z) w Hw1 to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR x.
Assume Hwu: w = - u.
Apply SNoR_E x Hx3 u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: x < u.
We prove the intermediate claim Lu: u ∈ SNoS_ (ordsucc (SNoLev u)).
An exact proof term for the current goal is SNoS_SNoLev u Hu1.
We prove the intermediate claim LsLu: ordsucc (SNoLev u) ∈ alpha.
Apply ordinal_ordsucc_In_eq (SNoLev x) (SNoLev u) Hx2 Hu2 to the current goal.
Assume H2: ordsucc (SNoLev u) ∈ SNoLev x.
An exact proof term for the current goal is Ha1 (SNoLev x) Hx1 (ordsucc (SNoLev u)) H2.
Assume H2: SNoLev x = ordsucc (SNoLev u).
rewrite the current goal using H2 (from right to left).
An exact proof term for the current goal is Hx1.
We prove the intermediate claim IHu: SNoLev (- u) ⊆ SNoLev u.
An exact proof term for the current goal is IH (ordsucc (SNoLev u)) LsLu u Lu.
We prove the intermediate claim LLu: ordinal (SNoLev u).
An exact proof term for the current goal is SNoLev_ordinal u Hu1.
We prove the intermediate claim Lmu: SNo (- u).
An exact proof term for the current goal is SNo_minus_SNo u Hu1.
We prove the intermediate claim LLmu: ordinal (SNoLev (- u)).
An exact proof term for the current goal is SNoLev_ordinal (- u) Lmu.
We prove the intermediate claim LsLw: ordinal (ordsucc (SNoLev w)).
Apply ordinal_ordsucc to the current goal.
rewrite the current goal using Hwu (from left to right).
An exact proof term for the current goal is LLmu.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered (ordsucc (SNoLev w)) LsLw beta Hw2.
Apply ordinal_In_Or_Subq beta (SNoLev x) Lb Hx2 to the current goal.
Assume H5: beta ∈ SNoLev x.
An exact proof term for the current goal is H5.
Assume H5: SNoLev x ⊆ beta.
We will prove False.
We prove the intermediate claim LLub: SNoLev u ∈ beta.
An exact proof term for the current goal is H5 (SNoLev u) Hu2.
Apply ordsuccE (SNoLev w) beta Hw2 to the current goal.
rewrite the current goal using Hwu (from left to right).
Assume H5: beta ∈ SNoLev (- u).
Apply In_no2cycle (SNoLev u) beta LLub to the current goal.
We will prove beta ∈ SNoLev u.
An exact proof term for the current goal is IHu beta H5.
rewrite the current goal using Hwu (from left to right).
Assume H5: beta = SNoLev (- u).
Apply In_irref (SNoLev u) to the current goal.
Apply IHu (SNoLev u) to the current goal.
We will prove SNoLev u ∈ SNoLev (- u).
rewrite the current goal using H5 (from right to left).
An exact proof term for the current goal is LLub.
Assume H4: beta ∈ ⋃y ∈ Rordsucc (SNoLev y).
Apply famunionE R (λx ⇒ ordsucc (SNoLev x)) beta H4 to the current goal.
Let w be given.
Assume Hw.
Apply Hw to the current goal.
Assume Hw1: w ∈ R.
Assume Hw2: beta ∈ ordsucc (SNoLev w).
We will prove beta ∈ SNoLev x.
Apply ReplE_impred (SNoL x) (λz ⇒ - z) w Hw1 to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Assume Hwu: w = - u.
Apply SNoL_E x Hx3 u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: u < x.
We prove the intermediate claim Lu: u ∈ SNoS_ (ordsucc (SNoLev u)).
An exact proof term for the current goal is SNoS_SNoLev u Hu1.
We prove the intermediate claim LsLu: ordsucc (SNoLev u) ∈ alpha.
Apply ordinal_ordsucc_In_eq (SNoLev x) (SNoLev u) Hx2 Hu2 to the current goal.
Assume H2: ordsucc (SNoLev u) ∈ SNoLev x.
An exact proof term for the current goal is Ha1 (SNoLev x) Hx1 (ordsucc (SNoLev u)) H2.
Assume H2: SNoLev x = ordsucc (SNoLev u).
rewrite the current goal using H2 (from right to left).
An exact proof term for the current goal is Hx1.
We prove the intermediate claim IHu: SNoLev (- u) ⊆ SNoLev u.
An exact proof term for the current goal is IH (ordsucc (SNoLev u)) LsLu u Lu.
We prove the intermediate claim LLu: ordinal (SNoLev u).
An exact proof term for the current goal is SNoLev_ordinal u Hu1.
We prove the intermediate claim Lmu: SNo (- u).
An exact proof term for the current goal is SNo_minus_SNo u Hu1.
We prove the intermediate claim LLmu: ordinal (SNoLev (- u)).
An exact proof term for the current goal is SNoLev_ordinal (- u) Lmu.
We prove the intermediate claim LsLw: ordinal (ordsucc (SNoLev w)).
Apply ordinal_ordsucc to the current goal.
rewrite the current goal using Hwu (from left to right).
An exact proof term for the current goal is LLmu.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered (ordsucc (SNoLev w)) LsLw beta Hw2.
Apply ordinal_In_Or_Subq beta (SNoLev x) Lb Hx2 to the current goal.
Assume H5: beta ∈ SNoLev x.
An exact proof term for the current goal is H5.
Assume H5: SNoLev x ⊆ beta.
We will prove False.
We prove the intermediate claim LLub: SNoLev u ∈ beta.
An exact proof term for the current goal is H5 (SNoLev u) Hu2.
Apply ordsuccE (SNoLev w) beta Hw2 to the current goal.
rewrite the current goal using Hwu (from left to right).
Assume H5: beta ∈ SNoLev (- u).
Apply In_no2cycle (SNoLev u) beta LLub to the current goal.
We will prove beta ∈ SNoLev u.
An exact proof term for the current goal is IHu beta H5.
rewrite the current goal using Hwu (from left to right).
Assume H5: beta = SNoLev (- u).
Apply In_irref (SNoLev u) to the current goal.
Apply IHu (SNoLev u) to the current goal.
We will prove SNoLev u ∈ SNoLev (- u).
rewrite the current goal using H5 (from right to left).
An exact proof term for the current goal is LLub.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Subgoal 7 Subgoal 8 Subgoal 9 Subgoal 10 Subgoal 11 Subgoal 12 Subgoal 13 Subgoal 14 Subgoal 15 Subgoal 16 Subgoal 17 Subgoal 18 Subgoal 19 Subgoal 20 Subgoal 21 Subgoal 22 Main Goal
Theorem. (minus_SNo_Lev_lem2) The following is provable:
∀x, SNo x → SNoLev (- x) ⊆ SNoLev x
Proof:
Let x be given.
Assume Hx: SNo x.
We prove the intermediate claim LLx: ordinal (SNoLev x).
An exact proof term for the current goal is SNoLev_ordinal x Hx.
We prove the intermediate claim LsLx: ordinal (ordsucc (SNoLev x)).
An exact proof term for the current goal is ordinal_ordsucc (SNoLev x) LLx.
We prove the intermediate claim LxsLx: x ∈ SNoS_ (ordsucc (SNoLev x)).
An exact proof term for the current goal is SNoS_SNoLev x Hx.
An exact proof term for the current goal is minus_SNo_Lev_lem1 (ordsucc (SNoLev x)) LsLx x LxsLx.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Main Goal
Theorem. (minus_SNo_invol) The following is provable:
∀x, SNo x → - - x = x
Proof:
Apply SNo_ind to the current goal.
Let L and R be given.
Assume HLR: SNoCutP L R.
Assume IHL: ∀x ∈ L, - - x = x.
Assume IHR: ∀y ∈ R, - - y = y.
Apply HLR to the current goal.
Assume H.
Apply H to the current goal.
Assume HLR1: ∀x ∈ L, SNo x.
Assume HLR2: ∀y ∈ R, SNo y.
Assume HLR3: ∀x ∈ L, ∀y ∈ R, x < y.
We prove the intermediate claim LCLR: SNo (SNoCut L R).
An exact proof term for the current goal is SNoCutP_SNo_SNoCut L R HLR.
We prove the intermediate claim LmCLR: SNo (- SNoCut L R).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is LCLR.
We prove the intermediate claim LmmCLR: SNo (- - SNoCut L R).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is LmCLR.
We prove the intermediate claim L1: SNoLev (SNoCut L R) ⊆ SNoLev (- - SNoCut L R) ∧ SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) (- - SNoCut L R).
Apply SNoCutP_SNoCut_fst to the current goal.
An exact proof term for the current goal is HLR.
We will prove SNo (- - SNoCut L R).
An exact proof term for the current goal is LmmCLR.
We will prove ∀x ∈ L, x < - - SNoCut L R.
Let x be given.
Assume Hx.
rewrite the current goal using IHL x Hx (from right to left).
We prove the intermediate claim Lx: SNo x.
An exact proof term for the current goal is HLR1 x Hx.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Lx.
We will prove - - x < - - SNoCut L R.
Apply minus_SNo_Lt_contra (- SNoCut L R) (- x) LmCLR Lmx to the current goal.
We will prove - SNoCut L R < - x.
Apply minus_SNo_Lt_contra x (SNoCut L R) Lx LCLR to the current goal.
We will prove x < SNoCut L R.
An exact proof term for the current goal is SNoCutP_SNoCut_L L R HLR x Hx.
We will prove ∀y ∈ R, - - SNoCut L R < y.
Let y be given.
Assume Hy.
rewrite the current goal using IHR y Hy (from right to left).
We prove the intermediate claim Ly: SNo y.
An exact proof term for the current goal is HLR2 y Hy.
We prove the intermediate claim Lmy: SNo (- y).
An exact proof term for the current goal is SNo_minus_SNo y Ly.
We will prove - - SNoCut L R < - - y.
Apply minus_SNo_Lt_contra (- y) (- SNoCut L R) Lmy LmCLR to the current goal.
We will prove - y < - SNoCut L R.
Apply minus_SNo_Lt_contra (SNoCut L R) y LCLR Ly to the current goal.
We will prove SNoCut L R < y.
An exact proof term for the current goal is SNoCutP_SNoCut_R L R HLR y Hy.
Apply L1 to the current goal.
Assume L1a: SNoLev (SNoCut L R) ⊆ SNoLev (- - SNoCut L R).
Assume L1b: SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) (- - SNoCut L R).
We will prove - - SNoCut L R = SNoCut L R.
Use symmetry.
Apply SNo_eq to the current goal.
An exact proof term for the current goal is LCLR.
An exact proof term for the current goal is LmmCLR.
We will prove SNoLev (SNoCut L R) = SNoLev (- - SNoCut L R).
Apply set_ext to the current goal.
We will prove SNoLev (SNoCut L R) ⊆ SNoLev (- - SNoCut L R).
An exact proof term for the current goal is L1a.
We will prove SNoLev (- - SNoCut L R) ⊆ SNoLev (SNoCut L R).
Apply Subq_tra (SNoLev (- - SNoCut L R)) (SNoLev (- SNoCut L R)) (SNoLev (SNoCut L R)) to the current goal.
We will prove SNoLev (- - SNoCut L R) ⊆ SNoLev (- SNoCut L R).
Apply minus_SNo_Lev_lem2 (- SNoCut L R) LmCLR to the current goal.
We will prove SNoLev (- SNoCut L R) ⊆ SNoLev (SNoCut L R).
Apply minus_SNo_Lev_lem2 (SNoCut L R) LCLR to the current goal.
We will prove SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) (- - SNoCut L R).
An exact proof term for the current goal is L1b.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Subgoal 7 Subgoal 8 Main Goal
Theorem. (minus_SNo_Lev) The following is provable:
∀x, SNo x → SNoLev (- x) = SNoLev x
Proof:
Let x be given.
Assume Hx.
Apply set_ext to the current goal.
We will prove SNoLev (- x) ⊆ SNoLev x.
An exact proof term for the current goal is minus_SNo_Lev_lem2 x Hx.
We will prove SNoLev x ⊆ SNoLev (- x).
rewrite the current goal using minus_SNo_invol x Hx (from right to left) at position 1.
We will prove SNoLev (- - x) ⊆ SNoLev (- x).
An exact proof term for the current goal is minus_SNo_Lev_lem2 (- x) (SNo_minus_SNo x Hx).
∎
Try to prove it yourself. Main Goal
Theorem. (minus_SNo_SNo_) The following is provable:
∀alpha, ordinal alpha → ∀x, SNo_ alpha x → SNo_ alpha (- x)
Proof:
Let alpha be given.
Assume Ha.
Let x be given.
Assume Hx: SNo_ alpha x.
We prove the intermediate claim Lx: SNo x.
An exact proof term for the current goal is SNo_SNo alpha Ha x Hx.
We prove the intermediate claim Lxa: SNoLev x = alpha.
An exact proof term for the current goal is SNoLev_uniq2 alpha Ha x Hx.
We prove the intermediate claim Lmxa: SNoLev (- x) = alpha.
rewrite the current goal using minus_SNo_Lev x Lx (from left to right).
An exact proof term for the current goal is Lxa.
We will prove SNo_ alpha (- x).
rewrite the current goal using Lmxa (from right to left).
We will prove SNo_ (SNoLev (- x)) (- x).
Apply SNoLev_ to the current goal.
We will prove SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Lx.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Main Goal
Theorem. (minus_SNo_SNoS_) The following is provable:
∀alpha, ordinal alpha → ∀x, x ∈ SNoS_ alpha → - x ∈ SNoS_ alpha
Proof:
Let alpha be given.
Assume Ha.
Let x be given.
Assume Hx: x ∈ SNoS_ alpha.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
Assume Hx1: SNoLev x ∈ alpha.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
We prove the intermediate claim Lbmx: SNo_ (SNoLev x) (- x).
An exact proof term for the current goal is minus_SNo_SNo_ (SNoLev x) Hx2 x Hx4.
An exact proof term for the current goal is SNoS_I alpha Ha (- x) (SNoLev x) Hx1 Lbmx.
∎
Try to prove it yourself. Subgoal 1 Main Goal
Theorem. (minus_SNoCut_eq_lem) The following is provable:
∀v, SNo v → ∀L R, SNoCutP L R → v = SNoCut L R → - v = SNoCut {- z|z ∈ R} {- w|w ∈ L}
Proof:
Apply SNoLev_ind to the current goal.
Let v be given.
Assume Hv: SNo v.
Assume IHv: ∀u ∈ SNoS_ (SNoLev v), ∀L R, SNoCutP L R → u = SNoCut L R → - u = SNoCut {- z|z ∈ R} {- w|w ∈ L}.
Let L and R be given.
Assume HLR: SNoCutP L R.
Apply HLR to the current goal.
Assume HLR1.
Apply HLR1 to the current goal.
Assume HLR1: ∀x ∈ L, SNo x.
Assume HLR2: ∀y ∈ R, SNo y.
Assume HLR3: ∀x ∈ L, ∀y ∈ R, x < y.
Assume HvLR: v = SNoCut L R.
Set mL to be the term {- w|w ∈ L}.
Set mR to be the term {- z|z ∈ R}.
Set mLv to be the term {- w|w ∈ SNoL v}.
Set mRv to be the term {- z|z ∈ SNoR v}.
We prove the intermediate claim L1: SNo (SNoCut L R).
An exact proof term for the current goal is SNoCutP_SNo_SNoCut L R HLR.
We prove the intermediate claim L2: SNoCutP mR mL.
An exact proof term for the current goal is minus_SNo_SNoCutP_gen L R HLR.
Apply SNoCutP_SNoCut_impred mR mL L2 to the current goal.
Assume H1: SNo (SNoCut mR mL).
Assume H2: SNoLev (SNoCut mR mL) ∈ ordsucc ((⋃x ∈ mRordsucc (SNoLev x)) ∪ (⋃y ∈ mLordsucc (SNoLev y))).
Assume H3: ∀x ∈ mR, x < SNoCut mR mL.
Assume H4: ∀y ∈ mL, SNoCut mR mL < y.
Assume H5: ∀z, SNo z → (∀x ∈ mR, x < z) → (∀y ∈ mL, z < y) → SNoLev (SNoCut mR mL) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut mR mL)) (SNoCut mR mL) z.
We prove the intermediate claim L3: ∀x ∈ mR, x < - v.
Let x be given.
Assume Hx: x ∈ mR.
Apply ReplE_impred R minus_SNo x Hx to the current goal.
Let z be given.
Assume Hz: z ∈ R.
Assume Hxz: x = - z.
We will prove x < - v.
rewrite the current goal using Hxz (from left to right).
We will prove - z < - v.
Apply minus_SNo_Lt_contra v z Hv (HLR2 z Hz) to the current goal.
We will prove v < z.
rewrite the current goal using HvLR (from left to right).
We will prove SNoCut L R < z.
An exact proof term for the current goal is SNoCutP_SNoCut_R L R HLR z Hz.
We prove the intermediate claim L4: ∀y ∈ mL, - v < y.
Let y be given.
Assume Hy: y ∈ mL.
Apply ReplE_impred L minus_SNo y Hy to the current goal.
Let w be given.
Assume Hw: w ∈ L.
Assume Hyw: y = - w.
We will prove - v < y.
rewrite the current goal using Hyw (from left to right).
We will prove - v < - w.
Apply minus_SNo_Lt_contra w v (HLR1 w Hw) Hv to the current goal.
We will prove w < v.
rewrite the current goal using HvLR (from left to right).
We will prove w < SNoCut L R.
An exact proof term for the current goal is SNoCutP_SNoCut_L L R HLR w Hw.
Apply H5 (- v) (SNo_minus_SNo v Hv) L3 L4 to the current goal.
Assume H6: SNoLev (SNoCut mR mL) ⊆ SNoLev (- v).
Assume H7: SNoEq_ (SNoLev (SNoCut mR mL)) (SNoCut mR mL) (- v).
We prove the intermediate claim L5: ordinal (SNoLev (SNoCut mR mL)).
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is H1.
We prove the intermediate claim L6: ordinal (SNoLev (- v)).
Apply SNoLev_ordinal to the current goal.
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hv.
Apply ordinal_In_Or_Subq (SNoLev (SNoCut mR mL)) (SNoLev (- v)) L5 L6 to the current goal.
Assume H8: SNoLev (SNoCut mR mL) ∈ SNoLev (- v).
We will prove False.
We prove the intermediate claim L7: SNoCut mR mL ∈ SNoS_ (SNoLev v).
Apply SNoS_I2 to the current goal.
We will prove SNo (SNoCut mR mL).
An exact proof term for the current goal is H1.
We will prove SNo v.
An exact proof term for the current goal is Hv.
We will prove SNoLev (SNoCut mR mL) ∈ SNoLev v.
rewrite the current goal using minus_SNo_Lev v Hv (from right to left).
An exact proof term for the current goal is H8.
We prove the intermediate claim LIH: - SNoCut mR mL = SNoCut {- z|z ∈ mL} {- w|w ∈ mR}.
An exact proof term for the current goal is IHv (SNoCut mR mL) L7 mR mL L2 (λq H ⇒ H).
We prove the intermediate claim L8: {- z|z ∈ mL} = L.
Apply Repl_invol_eq (λx ⇒ x ∈ L) minus_SNo to the current goal.
Let x be given.
Assume Hx: x ∈ L.
We will prove - - x = x.
An exact proof term for the current goal is minus_SNo_invol x (HLR1 x Hx).
Let x be given.
Assume Hx: x ∈ L.
An exact proof term for the current goal is Hx.
We prove the intermediate claim L9: {- z|z ∈ mR} = R.
Apply Repl_invol_eq (λy ⇒ y ∈ R) minus_SNo to the current goal.
Let y be given.
Assume Hy: y ∈ R.
We will prove - - y = y.
An exact proof term for the current goal is minus_SNo_invol y (HLR2 y Hy).
Let y be given.
Assume Hy: y ∈ R.
An exact proof term for the current goal is Hy.
We prove the intermediate claim L10: - SNoCut mR mL = v.
rewrite the current goal using LIH (from left to right).
rewrite the current goal using L8 (from left to right).
rewrite the current goal using L9 (from left to right).
Use symmetry.
An exact proof term for the current goal is HvLR.
Apply In_irref (SNoLev v) to the current goal.
We will prove SNoLev v ∈ SNoLev v.
rewrite the current goal using L10 (from right to left) at position 1.
We will prove SNoLev (- SNoCut mR mL) ∈ SNoLev v.
rewrite the current goal using minus_SNo_Lev (SNoCut mR mL) H1 (from left to right).
rewrite the current goal using minus_SNo_Lev v Hv (from right to left).
An exact proof term for the current goal is H8.
Assume H8: SNoLev (- v) ⊆ SNoLev (SNoCut mR mL).
We will prove - v = SNoCut mR mL.
Use symmetry.
Apply SNo_eq (SNoCut mR mL) (- v) H1 (SNo_minus_SNo v Hv) to the current goal.
We will prove SNoLev (SNoCut mR mL) = SNoLev (- v).
Apply set_ext to the current goal.
An exact proof term for the current goal is H6.
An exact proof term for the current goal is H8.
We will prove SNoEq_ (SNoLev (SNoCut mR mL)) (SNoCut mR mL) (- v).
An exact proof term for the current goal is H7.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Subgoal 7 Subgoal 8 Subgoal 9 Subgoal 10 Subgoal 11 Main Goal
Theorem. (minus_SNoCut_eq) The following is provable:
∀L R, SNoCutP L R → - SNoCut L R = SNoCut {- z|z ∈ R} {- w|w ∈ L}
Proof:
Let L and R be given.
Assume HLR.
An exact proof term for the current goal is minus_SNoCut_eq_lem (SNoCut L R) (SNoCutP_SNo_SNoCut L R HLR) L R HLR (λq H ⇒ H).
∎
Try to prove it yourself. Main Goal
Theorem. (minus_SNo_Lt_contra1) The following is provable:
∀x y, SNo x → SNo y → - x < y → - y < x
Proof:
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hxy: - x < y.
We will prove - y < x.
rewrite the current goal using minus_SNo_invol x Hx (from right to left).
We will prove - y < - - x.
Apply minus_SNo_Lt_contra (- x) y (SNo_minus_SNo x Hx) Hy to the current goal.
We will prove - x < y.
An exact proof term for the current goal is Hxy.
∎
Try to prove it yourself. Main Goal
Theorem. (minus_SNo_Lt_contra2) The following is provable:
∀x y, SNo x → SNo y → x < - y → y < - x
Proof:
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hxy: x < - y.
We will prove y < - x.
rewrite the current goal using minus_SNo_invol y Hy (from right to left).
We will prove - - y < - x.
Apply minus_SNo_Lt_contra x (- y) Hx (SNo_minus_SNo y Hy) to the current goal.
We will prove x < - y.
An exact proof term for the current goal is Hxy.
∎
Try to prove it yourself. Main Goal
Theorem. (mordinal_SNoLev_min_2) The following is provable:
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ ordsucc alpha → - alpha ≤ z
Proof:
Let alpha be given.
Assume Ha.
Let z be given.
Assume Hz: SNo z.
Assume H1: SNoLev z ∈ ordsucc alpha.
We prove the intermediate claim Lz1: SNo (- z).
An exact proof term for the current goal is SNo_minus_SNo z Hz.
We prove the intermediate claim Lz2: SNoLev (- z) ∈ ordsucc alpha.
rewrite the current goal using minus_SNo_Lev z Hz (from left to right).
An exact proof term for the current goal is H1.
We will prove - alpha ≤ z.
rewrite the current goal using minus_SNo_invol z Hz (from right to left).
We will prove - alpha ≤ - - z.
Apply minus_SNo_Le_contra (- z) alpha Lz1 (ordinal_SNo alpha Ha) to the current goal.
We will prove - z ≤ alpha.
An exact proof term for the current goal is ordinal_SNoLev_max_2 alpha Ha (- z) Lz1 Lz2.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal
Theorem. (minus_SNo_SNoS_omega) The following is provable:
∀x ∈ SNoS_ ω, - x ∈ SNoS_ ω
Proof:
Let x be given.
Assume Hx.
Apply SNoS_E2 ω omega_ordinal x Hx to the current goal.
Assume Hx1: SNoLev x ∈ ω.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
Apply SNoS_I ω omega_ordinal (- x) (SNoLev (- x)) to the current goal.
We will prove SNoLev (- x) ∈ ω.
rewrite the current goal using minus_SNo_Lev x Hx3 (from left to right).
We will prove SNoLev x ∈ ω.
An exact proof term for the current goal is Hx1.
We will prove SNo_ (SNoLev (- x)) (- x).
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is SNo_minus_SNo x Hx3.
∎
Try to prove it yourself. Main Goal
Theorem. (SNoL_minus_SNoR) The following is provable:
∀x, SNo x → SNoL (- x) = {- w|w ∈ SNoR x}
Proof:
Let x be given.
Assume Hx.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Hx.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ SNoL (- x).
Apply SNoL_E (- x) Lmx z Hz to the current goal.
Assume Hz1: SNo z.
rewrite the current goal using minus_SNo_Lev x Hx (from left to right).
Assume Hz2: SNoLev z ∈ SNoLev x.
Assume Hz3: z < - x.
We will prove z ∈ {- w|w ∈ SNoR x}.
rewrite the current goal using minus_SNo_invol z Hz1 (from right to left).
Apply ReplI to the current goal.
We will prove - z ∈ SNoR x.
Apply SNoR_I x Hx (- z) (SNo_minus_SNo z Hz1) to the current goal.
We will prove SNoLev (- z) ∈ SNoLev x.
rewrite the current goal using minus_SNo_Lev z Hz1 (from left to right).
An exact proof term for the current goal is Hz2.
We will prove x < - z.
Apply minus_SNo_Lt_contra2 z x Hz1 Hx to the current goal.
An exact proof term for the current goal is Hz3.
Let z be given.
Assume Hz: z ∈ {- w|w ∈ SNoR x}.
Apply ReplE_impred (SNoR x) minus_SNo z Hz to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR x.
Assume Hzw: z = - w.
We will prove z ∈ SNoL (- x).
rewrite the current goal using Hzw (from left to right).
We will prove - w ∈ SNoL (- x).
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev x.
Assume Hw3: x < w.
Apply SNoL_I (- x) Lmx (- w) (SNo_minus_SNo w Hw1) to the current goal.
We will prove SNoLev (- w) ∈ SNoLev (- x).
rewrite the current goal using minus_SNo_Lev w Hw1 (from left to right).
rewrite the current goal using minus_SNo_Lev x Hx (from left to right).
An exact proof term for the current goal is Hw2.
We will prove - w < - x.
Apply minus_SNo_Lt_contra x w Hx Hw1 to the current goal.
An exact proof term for the current goal is Hw3.
∎
Try to prove it yourself. Subgoal 1 Main Goal
End of Section SurrealMinus