Integers and Diadic Rationals

From Parts 1 - 6

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)
Beginning of Section SurrealMinus
Object. The name minus_SNo is a term 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.
Axiom. (minus_SNo_eq) We take the following as an axiom:
∀x, SNo x → - x = SNoCut {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
Axiom. (minus_SNo_prop1) We take the following as an axiom:
∀x, SNo x → SNo (- x) ∧ (∀u ∈ SNoL x, - x < - u) ∧ (∀u ∈ SNoR x, - u < - x) ∧ SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
Axiom. (SNo_minus_SNo) We take the following as an axiom:
∀x, SNo x → SNo (- x)
Axiom. (minus_SNo_Lt_contra) We take the following as an axiom:
∀x y, SNo x → SNo y → x < y → - y < - x
Axiom. (minus_SNo_Le_contra) We take the following as an axiom:
∀x y, SNo x → SNo y → x ≤ y → - y ≤ - x
Axiom. (minus_SNo_SNoCutP) We take the following as an axiom:
∀x, SNo x → SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
Axiom. (minus_SNo_SNoCutP_gen) We take the following as an axiom:
∀L R, SNoCutP L R → SNoCutP {- z|z ∈ R} {- w|w ∈ L}
Axiom. (minus_SNo_Lev_lem1) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, SNoLev (- x) ⊆ SNoLev x
Axiom. (minus_SNo_Lev_lem2) We take the following as an axiom:
∀x, SNo x → SNoLev (- x) ⊆ SNoLev x
Axiom. (minus_SNo_invol) We take the following as an axiom:
∀x, SNo x → - - x = x
Axiom. (minus_SNo_Lev) We take the following as an axiom:
∀x, SNo x → SNoLev (- x) = SNoLev x
Axiom. (minus_SNo_SNo_) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x, SNo_ alpha x → SNo_ alpha (- x)
Axiom. (minus_SNo_SNoS_) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x, x ∈ SNoS_ alpha → - x ∈ SNoS_ alpha
Axiom. (minus_SNoCut_eq_lem) We take the following as an axiom:
∀v, SNo v → ∀L R, SNoCutP L R → v = SNoCut L R → - v = SNoCut {- z|z ∈ R} {- w|w ∈ L}
Axiom. (minus_SNoCut_eq) We take the following as an axiom:
∀L R, SNoCutP L R → - SNoCut L R = SNoCut {- z|z ∈ R} {- w|w ∈ L}
Axiom. (minus_SNo_Lt_contra1) We take the following as an axiom:
∀x y, SNo x → SNo y → - x < y → - y < x
Axiom. (minus_SNo_Lt_contra2) We take the following as an axiom:
∀x y, SNo x → SNo y → x < - y → y < - x
Axiom. (mordinal_SNoLev_min_2) We take the following as an axiom:
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ ordsucc alpha → - alpha ≤ z
Axiom. (minus_SNo_SNoS_omega) We take the following as an axiom:
∀x ∈ SNoS_ ω, - x ∈ SNoS_ ω
Axiom. (SNoL_minus_SNoR) We take the following as an axiom:
∀x, SNo x → SNoL (- x) = {- w|w ∈ SNoR x}
End of Section SurrealMinus
Beginning of Section SurrealAdd
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Object. The name add_SNo is a term 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_SNo.
Axiom. (add_SNo_eq) We take the following as an axiom:
∀x, SNo x → ∀y, SNo y → x + y = SNoCut ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y})
Axiom. (add_SNo_prop1) We take the following as an axiom:
∀x y, SNo x → SNo y → SNo (x + y) ∧ (∀u ∈ SNoL x, u + y < x + y) ∧ (∀u ∈ SNoR x, x + y < u + y) ∧ (∀u ∈ SNoL y, x + u < x + y) ∧ (∀u ∈ SNoR y, x + y < x + u) ∧ SNoCutP ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y})
Axiom. (SNo_add_SNo) We take the following as an axiom:
∀x y, SNo x → SNo y → SNo (x + y)
Axiom. (SNo_add_SNo_3) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → SNo (x + y + z)
Axiom. (SNo_add_SNo_3c) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → SNo (x + y + - z)
Axiom. (SNo_add_SNo_4) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → SNo (x + y + z + w)
Axiom. (add_SNo_Lt1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x < z → x + y < z + y
Axiom. (add_SNo_Le1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x ≤ z → x + y ≤ z + y
Axiom. (add_SNo_Lt2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → y < z → x + y < x + z
Axiom. (add_SNo_Le2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → y ≤ z → x + y ≤ x + z
Axiom. (add_SNo_Lt3a) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x < z → y ≤ w → x + y < z + w
Axiom. (add_SNo_Lt3b) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x ≤ z → y < w → x + y < z + w
Axiom. (add_SNo_Lt3) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x < z → y < w → x + y < z + w
Axiom. (add_SNo_Le3) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x ≤ z → y ≤ w → x + y ≤ z + w
Axiom. (add_SNo_SNoCutP) We take the following as an axiom:
∀x y, SNo x → SNo y → SNoCutP ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y})
Axiom. (add_SNo_com) We take the following as an axiom:
∀x y, SNo x → SNo y → x + y = y + x
Axiom. (add_SNo_0L) We take the following as an axiom:
∀x, SNo x → 0 + x = x
Axiom. (add_SNo_0R) We take the following as an axiom:
∀x, SNo x → x + 0 = x
Axiom. (add_SNo_minus_SNo_linv) We take the following as an axiom:
∀x, SNo x → - x + x = 0
Axiom. (add_SNo_minus_SNo_rinv) We take the following as an axiom:
∀x, SNo x → x + - x = 0
Axiom. (add_SNo_ordinal_SNoCutP) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → SNoCutP ({x + beta|x ∈ SNoS_ alpha} ∪ {alpha + x|x ∈ SNoS_ beta}) Empty
Axiom. (add_SNo_ordinal_eq) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → alpha + beta = SNoCut ({x + beta|x ∈ SNoS_ alpha} ∪ {alpha + x|x ∈ SNoS_ beta}) Empty
Axiom. (add_SNo_ordinal_ordinal) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → ordinal (alpha + beta)
Axiom. (add_SNo_ordinal_SL) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → ordsucc alpha + beta = ordsucc (alpha + beta)
Axiom. (add_SNo_ordinal_SR) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → alpha + ordsucc beta = ordsucc (alpha + beta)
Axiom. (add_SNo_ordinal_InL) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → ∀gamma ∈ alpha, gamma + beta ∈ alpha + beta
Axiom. (add_SNo_ordinal_InR) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta, ordinal beta → ∀gamma ∈ beta, alpha + gamma ∈ alpha + beta
Axiom. (add_nat_add_SNo) We take the following as an axiom:
∀n m ∈ ω, add_nat n m = n + m
Axiom. (add_SNo_In_omega) We take the following as an axiom:
∀n m ∈ ω, n + m ∈ ω
Axiom. (add_SNo_1_1_2) We take the following as an axiom:
1 + 1 = 2
Axiom. (add_SNo_SNoL_interpolate) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀u ∈ SNoL (x + y), (∃v ∈ SNoL x, u ≤ v + y) ∨ (∃v ∈ SNoL y, u ≤ x + v)
Axiom. (add_SNo_SNoR_interpolate) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀u ∈ SNoR (x + y), (∃v ∈ SNoR x, v + y ≤ u) ∨ (∃v ∈ SNoR y, x + v ≤ u)
Axiom. (add_SNo_assoc) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + (y + z) = (x + y) + z
Axiom. (add_SNo_cancel_L) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y = x + z → y = z
Axiom. (minus_SNo_0) We take the following as an axiom:
- 0 = 0
Axiom. (minus_add_SNo_distr) We take the following as an axiom:
∀x y, SNo x → SNo y → - (x + y) = (- x) + (- y)
Axiom. (minus_add_SNo_distr_3) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → - (x + y + z) = - x + - y + - z
Axiom. (add_SNo_Lev_bd) We take the following as an axiom:
∀x y, SNo x → SNo y → SNoLev (x + y) ⊆ SNoLev x + SNoLev y
Axiom. (add_SNo_SNoS_omega) We take the following as an axiom:
∀x y ∈ SNoS_ ω, x + y ∈ SNoS_ ω
Axiom. (add_SNo_minus_R2) We take the following as an axiom:
∀x y, SNo x → SNo y → (x + y) + - y = x
Axiom. (add_SNo_minus_R2') We take the following as an axiom:
∀x y, SNo x → SNo y → (x + - y) + y = x
Axiom. (add_SNo_minus_L2) We take the following as an axiom:
∀x y, SNo x → SNo y → - x + (x + y) = y
Axiom. (add_SNo_minus_L2') We take the following as an axiom:
∀x y, SNo x → SNo y → x + (- x + y) = y
Axiom. (add_SNo_Lt1_cancel) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y < z + y → x < z
Axiom. (add_SNo_Lt2_cancel) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y < x + z → y < z
Axiom. (add_SNo_assoc_4) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y + z + w = (x + y + z) + w
Axiom. (add_SNo_com_3_0_1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y + z = y + x + z
Axiom. (add_SNo_com_3b_1_2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → (x + y) + z = (x + z) + y
Axiom. (add_SNo_com_4_inner_mid) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y) + (z + w) = (x + z) + (y + w)
Axiom. (add_SNo_rotate_3_1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + y + z = z + x + y
Axiom. (add_SNo_rotate_4_1) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y + z + w = w + x + y + z
Axiom. (add_SNo_rotate_5_1) We take the following as an axiom:
∀x y z w v, SNo x → SNo y → SNo z → SNo w → SNo v → x + y + z + w + v = v + x + y + z + w
Axiom. (add_SNo_rotate_5_2) We take the following as an axiom:
∀x y z w v, SNo x → SNo y → SNo z → SNo w → SNo v → x + y + z + w + v = w + v + x + y + z
Axiom. (add_SNo_minus_SNo_prop3) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y + z) + (- z + w) = x + y + w
Axiom. (add_SNo_minus_SNo_prop4) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y + z) + (w + - z) = x + y + w
Axiom. (add_SNo_minus_SNo_prop5) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y + - z) + (z + w) = x + y + w
Axiom. (add_SNo_minus_Lt1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + - y < z → x < z + y
Axiom. (add_SNo_minus_Lt2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → z < x + - y → z + y < x
Axiom. (add_SNo_minus_Lt1b) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x < z + y → x + - y < z
Axiom. (add_SNo_minus_Lt2b) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → z + y < x → z < x + - y
Axiom. (add_SNo_minus_Lt1b3) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y < w + z → x + y + - z < w
Axiom. (add_SNo_minus_Lt2b3) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → w + z < x + y → w < x + y + - z
Axiom. (add_SNo_minus_Lt_lem) We take the following as an axiom:
∀x y z u v w, SNo x → SNo y → SNo z → SNo u → SNo v → SNo w → x + y + w < u + v + z → x + y + - z < u + v + - w
Axiom. (add_SNo_minus_Le2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → z ≤ x + - y → z + y ≤ x
Axiom. (add_SNo_minus_Le2b) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → z + y ≤ x → z ≤ x + - y
Axiom. (add_SNo_Lt_subprop2) We take the following as an axiom:
∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x + u < z + v → y + v < w + u → x + y < z + w
Axiom. (add_SNo_Lt_subprop3a) We take the following as an axiom:
∀x y z w u a, SNo x → SNo y → SNo z → SNo w → SNo u → SNo a → x + z < w + a → y + a < u → x + y + z < w + u
Axiom. (add_SNo_Lt_subprop3b) We take the following as an axiom:
∀x y w u v a, SNo x → SNo y → SNo w → SNo u → SNo v → SNo a → x + a < w + v → y < a + u → x + y < w + u + v
Axiom. (add_SNo_Lt_subprop3c) We take the following as an axiom:
∀x y z w u a b c, SNo x → SNo y → SNo z → SNo w → SNo u → SNo a → SNo b → SNo c → x + a < b + c → y + c < u → b + z < w + a → x + y + z < w + u
Axiom. (add_SNo_Lt_subprop3d) We take the following as an axiom:
∀x y w u v a b c, SNo x → SNo y → SNo w → SNo u → SNo v → SNo a → SNo b → SNo c → x + a < b + v → y < c + u → b + c < w + a → x + y < w + u + v
Axiom. (ordinal_ordsucc_SNo_eq) We take the following as an axiom:
∀alpha, ordinal alpha → ordsucc alpha = 1 + alpha
Axiom. (add_SNo_3a_2b) We take the following as an axiom:
∀x y z w u, SNo x → SNo y → SNo z → SNo w → SNo u → (x + y + z) + (w + u) = (u + y + z) + (w + x)
Axiom. (add_SNo_1_ordsucc) We take the following as an axiom:
∀n ∈ ω, n + 1 = ordsucc n
Axiom. (add_SNo_eps_Lt) We take the following as an axiom:
∀x, SNo x → ∀n ∈ ω, x < x + eps_ n
Axiom. (add_SNo_eps_Lt') We take the following as an axiom:
∀x y, SNo x → SNo y → ∀n ∈ ω, x < y → x < y + eps_ n
Axiom. (SNoLt_minus_pos) We take the following as an axiom:
∀x y, SNo x → SNo y → x < y → 0 < y + - x
Axiom. (add_SNo_omega_In_cases) We take the following as an axiom:
∀m, ∀n ∈ ω, ∀k, nat_p k → m ∈ n + k → m ∈ n ∨ m + - n ∈ k
Axiom. (add_SNo_Lt4) We take the following as an axiom:
∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x < w → y < u → z < v → x + y + z < w + u + v
Axiom. (add_SNo_3_3_3_Lt1) We take the following as an axiom:
∀x y z w u, SNo x → SNo y → SNo z → SNo w → SNo u → x + y < z + w → x + y + u < z + w + u
Axiom. (add_SNo_3_2_3_Lt1) We take the following as an axiom:
∀x y z w u, SNo x → SNo y → SNo z → SNo w → SNo u → y + x < z + w → x + u + y < z + w + u
End of Section SurrealAdd
Beginning of Section SurrealMul
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Definition. We define mul_SNo to be SNo_rec2 (λx y m ⇒ SNoCut ({m (w 0) y + m x (w 1) + - m (w 0) (w 1)|w ∈ SNoL x ⨯ SNoL y} ∪ {m (z 0) y + m x (z 1) + - m (z 0) (z 1)|z ∈ SNoR x ⨯ SNoR y}) ({m (w 0) y + m x (w 1) + - m (w 0) (w 1)|w ∈ SNoL x ⨯ SNoR y} ∪ {m (z 0) y + m x (z 1) + - m (z 0) (z 1)|z ∈ SNoR x ⨯ SNoL y})) of type set → set → set.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Axiom. (mul_SNo_eq) We take the following as an axiom:
∀x, SNo x → ∀y, SNo y → x * y = SNoCut ({(w 0) * y + x * (w 1) + - (w 0) * (w 1)|w ∈ SNoL x ⨯ SNoL y} ∪ {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|z ∈ SNoR x ⨯ SNoR y}) ({(w 0) * y + x * (w 1) + - (w 0) * (w 1)|w ∈ SNoL x ⨯ SNoR y} ∪ {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|z ∈ SNoR x ⨯ SNoL y})
Axiom. (mul_SNo_eq_2) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀p : prop, (∀L R, (∀u, u ∈ L → (∀q : prop, (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, u = w0 * y + x * w1 + - w0 * w1 → q) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, u = z0 * y + x * z1 + - z0 * z1 → q) → q)) → (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, w0 * y + x * w1 + - w0 * w1 ∈ L) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, z0 * y + x * z1 + - z0 * z1 ∈ L) → (∀u, u ∈ R → (∀q : prop, (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, u = w0 * y + x * z1 + - w0 * z1 → q) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, u = z0 * y + x * w1 + - z0 * w1 → q) → q)) → (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, w0 * y + x * z1 + - w0 * z1 ∈ R) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, z0 * y + x * w1 + - z0 * w1 ∈ R) → x * y = SNoCut L R → p) → p
Axiom. (mul_SNo_prop_1) We take the following as an axiom:
∀x, SNo x → ∀y, SNo y → ∀p : prop, (SNo (x * y) → (∀u ∈ SNoL x, ∀v ∈ SNoL y, u * y + x * v < x * y + u * v) → (∀u ∈ SNoR x, ∀v ∈ SNoR y, u * y + x * v < x * y + u * v) → (∀u ∈ SNoL x, ∀v ∈ SNoR y, x * y + u * v < u * y + x * v) → (∀u ∈ SNoR x, ∀v ∈ SNoL y, x * y + u * v < u * y + x * v) → p) → p
Axiom. (SNo_mul_SNo) We take the following as an axiom:
∀x y, SNo x → SNo y → SNo (x * y)
Axiom. (SNo_mul_SNo_lem) We take the following as an axiom:
∀x y u v, SNo x → SNo y → SNo u → SNo v → SNo (u * y + x * v + - (u * v))
Axiom. (SNo_mul_SNo_3) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → SNo (x * y * z)
Axiom. (mul_SNo_eq_3) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀p : prop, (∀L R, SNoCutP L R → (∀u, u ∈ L → (∀q : prop, (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, u = w0 * y + x * w1 + - w0 * w1 → q) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, u = z0 * y + x * z1 + - z0 * z1 → q) → q)) → (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, w0 * y + x * w1 + - w0 * w1 ∈ L) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, z0 * y + x * z1 + - z0 * z1 ∈ L) → (∀u, u ∈ R → (∀q : prop, (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, u = w0 * y + x * z1 + - w0 * z1 → q) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, u = z0 * y + x * w1 + - z0 * w1 → q) → q)) → (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, w0 * y + x * z1 + - w0 * z1 ∈ R) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, z0 * y + x * w1 + - z0 * w1 ∈ R) → x * y = SNoCut L R → p) → p
Axiom. (mul_SNo_Lt) We take the following as an axiom:
∀x y u v, SNo x → SNo y → SNo u → SNo v → u < x → v < y → u * y + x * v < x * y + u * v
Axiom. (mul_SNo_Le) We take the following as an axiom:
∀x y u v, SNo x → SNo y → SNo u → SNo v → u ≤ x → v ≤ y → u * y + x * v ≤ x * y + u * v
Axiom. (mul_SNo_SNoL_interpolate) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀u ∈ SNoL (x * y), (∃v ∈ SNoL x, ∃w ∈ SNoL y, u + v * w ≤ v * y + x * w) ∨ (∃v ∈ SNoR x, ∃w ∈ SNoR y, u + v * w ≤ v * y + x * w)
Axiom. (mul_SNo_SNoL_interpolate_impred) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀u ∈ SNoL (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoL y, u + v * w ≤ v * y + x * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoR y, u + v * w ≤ v * y + x * w → p) → p
Axiom. (mul_SNo_SNoR_interpolate) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀u ∈ SNoR (x * y), (∃v ∈ SNoL x, ∃w ∈ SNoR y, v * y + x * w ≤ u + v * w) ∨ (∃v ∈ SNoR x, ∃w ∈ SNoL y, v * y + x * w ≤ u + v * w)
Axiom. (mul_SNo_SNoR_interpolate_impred) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀u ∈ SNoR (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoR y, v * y + x * w ≤ u + v * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoL y, v * y + x * w ≤ u + v * w → p) → p
Axiom. (mul_SNo_Subq_lem) We take the following as an axiom:
∀x y X Y Z W, ∀U U', (∀u, u ∈ U → (∀q : prop, (∀w0 ∈ X, ∀w1 ∈ Y, u = w0 * y + x * w1 + - w0 * w1 → q) → (∀z0 ∈ Z, ∀z1 ∈ W, u = z0 * y + x * z1 + - z0 * z1 → q) → q)) → (∀w0 ∈ X, ∀w1 ∈ Y, w0 * y + x * w1 + - w0 * w1 ∈ U') → (∀w0 ∈ Z, ∀w1 ∈ W, w0 * y + x * w1 + - w0 * w1 ∈ U') → U ⊆ U'
Axiom. (mul_SNo_zeroR) We take the following as an axiom:
∀x, SNo x → x * 0 = 0
Axiom. (mul_SNo_oneR) We take the following as an axiom:
∀x, SNo x → x * 1 = x
Axiom. (mul_SNo_com) We take the following as an axiom:
∀x y, SNo x → SNo y → x * y = y * x
Axiom. (mul_SNo_minus_distrL) We take the following as an axiom:
∀x y, SNo x → SNo y → (- x) * y = - x * y
Axiom. (mul_SNo_minus_distrR) We take the following as an axiom:
∀x y, SNo x → SNo y → x * (- y) = - (x * y)
Axiom. (mul_SNo_distrR) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → (x + y) * z = x * z + y * z
Axiom. (mul_SNo_distrL) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x * (y + z) = x * y + x * z
Beginning of Section mul_SNo_assoc_lems
Variable M : set → set → set
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term M.
Hypothesis SNo_M : ∀x y, SNo x → SNo y → SNo (x * y)
Hypothesis DL : ∀x y z, SNo x → SNo y → SNo z → x * (y + z) = x * y + x * z
Hypothesis DR : ∀x y z, SNo x → SNo y → SNo z → (x + y) * z = x * z + y * z
Hypothesis IL : ∀x y, SNo x → SNo y → ∀u ∈ SNoL (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoL y, u + v * w ≤ v * y + x * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoR y, u + v * w ≤ v * y + x * w → p) → p
Hypothesis IR : ∀x y, SNo x → SNo y → ∀u ∈ SNoR (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoR y, v * y + x * w ≤ u + v * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoL y, v * y + x * w ≤ u + v * w → p) → p
Hypothesis M_Lt : ∀x y u v, SNo x → SNo y → SNo u → SNo v → u < x → v < y → u * y + x * v < x * y + u * v
Hypothesis M_Le : ∀x y u v, SNo x → SNo y → SNo u → SNo v → u ≤ x → v ≤ y → u * y + x * v ≤ x * y + u * v
Axiom. (mul_SNo_assoc_lem1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x), u * (y * z) = (u * y) * z) → (∀v ∈ SNoS_ (SNoLev y), x * (v * z) = (x * v) * z) → (∀w ∈ SNoS_ (SNoLev z), x * (y * w) = (x * y) * w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), u * (v * z) = (u * v) * z) → (∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), u * (y * w) = (u * y) * w) → (∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), x * (v * w) = (x * v) * w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), u * (v * w) = (u * v) * w) → ∀L, (∀u ∈ L, ∀q : prop, (∀v ∈ SNoL x, ∀w ∈ SNoL (y * z), u = v * (y * z) + x * w + - v * w → q) → (∀v ∈ SNoR x, ∀w ∈ SNoR (y * z), u = v * (y * z) + x * w + - v * w → q) → q) → ∀u ∈ L, u < (x * y) * z
Axiom. (mul_SNo_assoc_lem2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x), u * (y * z) = (u * y) * z) → (∀v ∈ SNoS_ (SNoLev y), x * (v * z) = (x * v) * z) → (∀w ∈ SNoS_ (SNoLev z), x * (y * w) = (x * y) * w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), u * (v * z) = (u * v) * z) → (∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), u * (y * w) = (u * y) * w) → (∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), x * (v * w) = (x * v) * w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), u * (v * w) = (u * v) * w) → ∀R, (∀u ∈ R, ∀q : prop, (∀v ∈ SNoL x, ∀w ∈ SNoR (y * z), u = v * (y * z) + x * w + - v * w → q) → (∀v ∈ SNoR x, ∀w ∈ SNoL (y * z), u = v * (y * z) + x * w + - v * w → q) → q) → ∀u ∈ R, (x * y) * z < u
End of Section mul_SNo_assoc_lems
Axiom. (mul_SNo_assoc) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x * (y * z) = (x * y) * z
Axiom. (mul_nat_mul_SNo) We take the following as an axiom:
∀n m ∈ ω, mul_nat n m = n * m
Axiom. (mul_SNo_In_omega) We take the following as an axiom:
∀n m ∈ ω, n * m ∈ ω
Axiom. (mul_SNo_zeroL) We take the following as an axiom:
∀x, SNo x → 0 * x = 0
Axiom. (mul_SNo_oneL) We take the following as an axiom:
∀x, SNo x → 1 * x = x
Axiom. (pos_mul_SNo_Lt) We take the following as an axiom:
∀x y z, SNo x → 0 < x → SNo y → SNo z → y < z → x * y < x * z
Axiom. (nonneg_mul_SNo_Le) We take the following as an axiom:
∀x y z, SNo x → 0 ≤ x → SNo y → SNo z → y ≤ z → x * y ≤ x * z
Axiom. (neg_mul_SNo_Lt) We take the following as an axiom:
∀x y z, SNo x → x < 0 → SNo y → SNo z → z < y → x * y < x * z
Axiom. (pos_mul_SNo_Lt') We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → 0 < z → x < y → x * z < y * z
Axiom. (mul_SNo_Lt1_pos_Lt) We take the following as an axiom:
∀x y, SNo x → SNo y → x < 1 → 0 < y → x * y < y
Axiom. (nonneg_mul_SNo_Le') We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → 0 ≤ z → x ≤ y → x * z ≤ y * z
Axiom. (mul_SNo_Le1_nonneg_Le) We take the following as an axiom:
∀x y, SNo x → SNo y → x ≤ 1 → 0 ≤ y → x * y ≤ y
Axiom. (pos_mul_SNo_Lt2) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → 0 < x → 0 < y → x < z → y < w → x * y < z * w
Axiom. (nonneg_mul_SNo_Le2) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → 0 ≤ x → 0 ≤ y → x ≤ z → y ≤ w → x * y ≤ z * w
Axiom. (mul_SNo_pos_pos) We take the following as an axiom:
∀x y, SNo x → SNo y → 0 < x → 0 < y → 0 < x * y
Axiom. (mul_SNo_pos_neg) We take the following as an axiom:
∀x y, SNo x → SNo y → 0 < x → y < 0 → x * y < 0
Axiom. (mul_SNo_neg_pos) We take the following as an axiom:
∀x y, SNo x → SNo y → x < 0 → 0 < y → x * y < 0
Axiom. (mul_SNo_neg_neg) We take the following as an axiom:
∀x y, SNo x → SNo y → x < 0 → y < 0 → 0 < x * y
Axiom. (SNo_sqr_nonneg) We take the following as an axiom:
∀x, SNo x → 0 ≤ x * x
Axiom. (SNo_zero_or_sqr_pos) We take the following as an axiom:
∀x, SNo x → x = 0 ∨ 0 < x * x
Axiom. (SNo_foil) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y) * (z + w) = x * z + x * w + y * z + y * w
Axiom. (mul_SNo_minus_minus) We take the following as an axiom:
∀x y, SNo x → SNo y → (- x) * (- y) = x * y
Axiom. (mul_SNo_com_3_0_1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x * y * z = y * x * z
Axiom. (mul_SNo_com_3b_1_2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → (x * y) * z = (x * z) * y
Axiom. (mul_SNo_com_4_inner_mid) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x * y) * (z * w) = (x * z) * (y * w)
Axiom. (mul_SNo_rotate_3_1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x * y * z = z * x * y
Axiom. (mul_SNo_rotate_4_1) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x * y * z * w = w * x * y * z
Axiom. (SNo_foil_mm) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + - y) * (z + - w) = x * z + - x * w + - y * z + y * w
Axiom. (mul_SNo_nonzero_cancel) We take the following as an axiom:
∀x y z, SNo x → x ≠ 0 → SNo y → SNo z → x * y = x * z → y = z
End of Section SurrealMul
Beginning of Section SurrealExp
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Definition. We define exp_SNo_nat to be λn m : set ⇒ nat_primrec 1 (λ_ r ⇒ n * r) m of type set → set → set.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Axiom. (exp_SNo_nat_0) We take the following as an axiom:
∀x, SNo x → x ^ 0 = 1
Axiom. (exp_SNo_nat_S) We take the following as an axiom:
∀x, SNo x → ∀n, nat_p n → x ^ (ordsucc n) = x * x ^ n
Axiom. (SNo_exp_SNo_nat) We take the following as an axiom:
∀x, SNo x → ∀n, nat_p n → SNo (x ^ n)
Axiom. (nat_exp_SNo_nat) We take the following as an axiom:
∀x, nat_p x → ∀n, nat_p n → nat_p (x ^ n)
Axiom. (eps_ordsucc_half_add) We take the following as an axiom:
∀n, nat_p n → eps_ (ordsucc n) + eps_ (ordsucc n) = eps_ n
Axiom. (eps_1_half_eq1) We take the following as an axiom:
eps_ 1 + eps_ 1 = 1
Axiom. (eps_1_half_eq2) We take the following as an axiom:
2 * eps_ 1 = 1
Axiom. (double_eps_1) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x + x = y + z → x = eps_ 1 * (y + z)
Axiom. (exp_SNo_1_bd) We take the following as an axiom:
∀x, SNo x → 1 ≤ x → ∀n, nat_p n → 1 ≤ x ^ n
Axiom. (exp_SNo_2_bd) We take the following as an axiom:
∀n, nat_p n → n < 2 ^ n
Axiom. (mul_SNo_eps_power_2) We take the following as an axiom:
∀n, nat_p n → eps_ n * 2 ^ n = 1
Axiom. (eps_bd_1) We take the following as an axiom:
∀n ∈ ω, eps_ n ≤ 1
Axiom. (mul_SNo_eps_power_2') We take the following as an axiom:
∀n, nat_p n → 2 ^ n * eps_ n = 1
Axiom. (exp_SNo_nat_mul_add) We take the following as an axiom:
∀x, SNo x → ∀m, nat_p m → ∀n, nat_p n → x ^ m * x ^ n = x ^ (m + n)
Axiom. (exp_SNo_nat_mul_add') We take the following as an axiom:
∀x, SNo x → ∀m n ∈ ω, x ^ m * x ^ n = x ^ (m + n)
Axiom. (exp_SNo_nat_pos) We take the following as an axiom:
∀x, SNo x → 0 < x → ∀n, nat_p n → 0 < x ^ n
Axiom. (mul_SNo_eps_eps_add_SNo) We take the following as an axiom:
∀m n ∈ ω, eps_ m * eps_ n = eps_ (m + n)
Axiom. (SNoS_omega_Lev_equip) We take the following as an axiom:
∀n, nat_p n → equip {x ∈ SNoS_ ω|SNoLev x = n} (2 ^ n)
Axiom. (SNoS_finite) We take the following as an axiom:
∀n ∈ ω, finite (SNoS_ n)
Axiom. (SNoS_omega_SNoL_finite) We take the following as an axiom:
∀x ∈ SNoS_ ω, finite (SNoL x)
Axiom. (SNoS_omega_SNoR_finite) We take the following as an axiom:
∀x ∈ SNoS_ ω, finite (SNoR x)
End of Section SurrealExp

Part 7

Beginning of Section Int
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Definition. We define int to be ω ∪ {- n|n ∈ ω} of type set.
Theorem. (int_SNo_cases) The following is provable:
∀p : set → prop, (∀n ∈ ω, p n) → (∀n ∈ ω, p (- n)) → ∀x ∈ int, p x
Proof:
Let p be given.
Assume Hp1 Hp2.
Let x be given.
Assume Hx.
We will prove p x.
Apply binunionE ω {- n|n ∈ ω} x Hx to the current goal.
Assume Hx: x ∈ ω.
An exact proof term for the current goal is Hp1 x Hx.
Assume Hx.
Apply ReplE_impred ω minus_SNo x Hx to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume Hxn: x = - n.
rewrite the current goal using Hxn (from left to right).
An exact proof term for the current goal is Hp2 n Hn.
∎
Try to prove it yourself. Main Goal
Theorem. (int_SNo) The following is provable:
∀x ∈ int, SNo x
Proof:
Apply int_SNo_cases to the current goal.
An exact proof term for the current goal is omega_SNo.
Let n be given.
Assume Hn.
We will prove SNo (- n).
Apply SNo_minus_SNo to the current goal.
We will prove SNo n.
An exact proof term for the current goal is omega_SNo n Hn.
∎
Try to prove it yourself. Main Goal
Theorem. (Subq_omega_int) The following is provable:
ω ⊆ int
Proof:
Let n be given.
Assume Hn.
We will prove n ∈ ω ∪ {- k|k ∈ ω}.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is Hn.
∎
Try to prove it yourself. Main Goal
Theorem. (int_minus_SNo_omega) The following is provable:
∀n ∈ ω, - n ∈ int
Proof:
Let n be given.
Assume Hn.
We will prove - n ∈ ω ∪ {- k|k ∈ ω}.
Apply binunionI2 to the current goal.
We will prove - n ∈ {- k|k ∈ ω}.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hn.
∎
Try to prove it yourself. Main Goal
Theorem. (int_add_SNo_lem) The following is provable:
∀n ∈ ω, ∀m, nat_p m → - n + m ∈ int
Proof:
Let n be given.
Assume Hn.
We prove the intermediate claim Lnn: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We prove the intermediate claim Lno: ordinal n.
An exact proof term for the current goal is nat_p_ordinal n Lnn.
We prove the intermediate claim LnS: SNo n.
An exact proof term for the current goal is ordinal_SNo n Lno.
Apply nat_ind to the current goal.
We will prove - n + 0 ∈ int.
rewrite the current goal using add_SNo_0R (- n) (SNo_minus_SNo n LnS) (from left to right).
We will prove - n ∈ int.
Apply int_minus_SNo_omega to the current goal.
An exact proof term for the current goal is Hn.
Let m be given.
Assume Hm: nat_p m.
Assume IHm: - n + m ∈ int.
We prove the intermediate claim Lmo: ordinal m.
An exact proof term for the current goal is nat_p_ordinal m Hm.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is ordinal_SNo m Lmo.
We will prove - n + ordsucc m ∈ int.
rewrite the current goal using ordinal_ordsucc_SNo_eq m Lmo (from left to right).
We will prove - n + (1 + m) ∈ int.
rewrite the current goal using add_SNo_com_3_0_1 (- n) 1 m (SNo_minus_SNo n LnS) SNo_1 LmS (from left to right).
We will prove 1 + (- n + m) ∈ int.
We prove the intermediate claim L1: ∀k ∈ ω, - n + m = k → 1 + (- n + m) ∈ int.
Let k be given.
Assume Hk He.
rewrite the current goal using He (from left to right).
We will prove 1 + k ∈ int.
rewrite the current goal using ordinal_ordsucc_SNo_eq k (nat_p_ordinal k (omega_nat_p k Hk)) (from right to left).
We will prove ordsucc k ∈ int.
Apply Subq_omega_int to the current goal.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is Hk.
We prove the intermediate claim L2: ∀k ∈ ω, - n + m = - k → 1 + (- n + m) ∈ int.
Let k be given.
Assume Hk He.
rewrite the current goal using He (from left to right).
We will prove 1 + - k ∈ int.
Apply nat_inv k (omega_nat_p k Hk) to the current goal.
Assume H1: k = 0.
rewrite the current goal using H1 (from left to right).
rewrite the current goal using minus_SNo_0 (from left to right).
rewrite the current goal using add_SNo_0R 1 SNo_1 (from left to right).
We will prove 1 ∈ int.
Apply Subq_omega_int to the current goal.
We will prove 1 ∈ ω.
An exact proof term for the current goal is nat_p_omega 1 nat_1.
Assume H1.
Apply H1 to the current goal.
Let k' be given.
Assume H1.
Apply H1 to the current goal.
Assume H1: nat_p k'.
Assume H2: k = ordsucc k'.
rewrite the current goal using H2 (from left to right).
We will prove 1 + - (ordsucc k') ∈ int.
rewrite the current goal using ordinal_ordsucc_SNo_eq k' (nat_p_ordinal k' H1) (from left to right).
We will prove 1 + - (1 + k') ∈ int.
rewrite the current goal using minus_add_SNo_distr 1 k' SNo_1 (ordinal_SNo k' (nat_p_ordinal k' H1)) (from left to right).
We will prove 1 + - 1 + - k' ∈ int.
rewrite the current goal using add_SNo_minus_L2' 1 (- k') SNo_1 (SNo_minus_SNo k' (ordinal_SNo k' (nat_p_ordinal k' H1))) (from left to right).
We will prove - k' ∈ int.
Apply int_minus_SNo_omega to the current goal.
An exact proof term for the current goal is nat_p_omega k' H1.
Apply int_SNo_cases (λx ⇒ - n + m = x → 1 + (- n + m) ∈ int) L1 L2 (- n + m) IHm to the current goal.
Use reflexivity.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Subgoal 7 Main Goal
Theorem. (int_add_SNo) The following is provable:
∀x y ∈ int, x + y ∈ int
Proof:
Apply int_SNo_cases to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Apply int_SNo_cases to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
Apply Subq_omega_int to the current goal.
We will prove n + m ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega n Hn m Hm.
Let m be given.
Assume Hm: m ∈ ω.
We will prove n + - m ∈ int.
rewrite the current goal using add_SNo_com n (- m) (ordinal_SNo n (nat_p_ordinal n (omega_nat_p n Hn))) (SNo_minus_SNo m (ordinal_SNo m (nat_p_ordinal m (omega_nat_p m Hm)))) (from left to right).
We will prove - m + n ∈ int.
An exact proof term for the current goal is int_add_SNo_lem m Hm n (omega_nat_p n Hn).
Let n be given.
Assume Hn: n ∈ ω.
Apply int_SNo_cases to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
We will prove - n + m ∈ int.
An exact proof term for the current goal is int_add_SNo_lem n Hn m (omega_nat_p m Hm).
Let m be given.
Assume Hm: m ∈ ω.
We will prove - n + - m ∈ int.
We prove the intermediate claim Ln: SNo n.
An exact proof term for the current goal is ordinal_SNo n (nat_p_ordinal n (omega_nat_p n Hn)).
We prove the intermediate claim Lm: SNo m.
An exact proof term for the current goal is ordinal_SNo m (nat_p_ordinal m (omega_nat_p m Hm)).
rewrite the current goal using minus_add_SNo_distr n m Ln Lm (from right to left).
Apply int_minus_SNo_omega to the current goal.
We will prove n + m ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega n Hn m Hm.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal
Theorem. (int_minus_SNo) The following is provable:
∀x ∈ int, - x ∈ int
Proof:
Apply int_SNo_cases to the current goal.
Let n be given.
Assume Hn.
We will prove - n ∈ int.
Apply int_minus_SNo_omega to the current goal.
An exact proof term for the current goal is Hn.
Let n be given.
Assume Hn.
We will prove - - n ∈ int.
rewrite the current goal using minus_SNo_invol n (ordinal_SNo n (nat_p_ordinal n (omega_nat_p n Hn))) (from left to right).
We will prove n ∈ int.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is Hn.
∎
Try to prove it yourself. Main Goal
Theorem. (int_mul_SNo) The following is provable:
∀x y ∈ int, x * y ∈ int
Proof:
Apply int_SNo_cases to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
We prove the intermediate claim Lnn: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We prove the intermediate claim Lno: ordinal n.
An exact proof term for the current goal is nat_p_ordinal n Lnn.
We prove the intermediate claim LnS: SNo n.
An exact proof term for the current goal is ordinal_SNo n Lno.
Apply int_SNo_cases to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
Apply Subq_omega_int to the current goal.
We will prove n * m ∈ ω.
An exact proof term for the current goal is mul_SNo_In_omega n Hn m Hm.
Let m be given.
Assume Hm: m ∈ ω.
We prove the intermediate claim Lmn: nat_p m.
An exact proof term for the current goal is omega_nat_p m Hm.
We prove the intermediate claim Lmo: ordinal m.
An exact proof term for the current goal is nat_p_ordinal m Lmn.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is ordinal_SNo m Lmo.
We will prove n * (- m) ∈ int.
rewrite the current goal using mul_SNo_com n (- m) LnS (SNo_minus_SNo m LmS) (from left to right).
We will prove (- m) * n ∈ int.
rewrite the current goal using mul_SNo_minus_distrL m n LmS LnS (from left to right).
We will prove - (m * n) ∈ int.
Apply int_minus_SNo to the current goal.
We will prove m * n ∈ int.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is mul_SNo_In_omega m Hm n Hn.
Let n be given.
Assume Hn: n ∈ ω.
We prove the intermediate claim Lnn: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We prove the intermediate claim Lno: ordinal n.
An exact proof term for the current goal is nat_p_ordinal n Lnn.
We prove the intermediate claim LnS: SNo n.
An exact proof term for the current goal is ordinal_SNo n Lno.
Apply int_SNo_cases to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
We prove the intermediate claim Lmn: nat_p m.
An exact proof term for the current goal is omega_nat_p m Hm.
We prove the intermediate claim Lmo: ordinal m.
An exact proof term for the current goal is nat_p_ordinal m Lmn.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is ordinal_SNo m Lmo.
We will prove (- n) * m ∈ int.
rewrite the current goal using mul_SNo_minus_distrL n m LnS LmS (from left to right).
We will prove - (n * m) ∈ int.
Apply int_minus_SNo to the current goal.
We will prove n * m ∈ int.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is mul_SNo_In_omega n Hn m Hm.
Let m be given.
Assume Hm: m ∈ ω.
We prove the intermediate claim Lmn: nat_p m.
An exact proof term for the current goal is omega_nat_p m Hm.
We prove the intermediate claim Lmo: ordinal m.
An exact proof term for the current goal is nat_p_ordinal m Lmn.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is ordinal_SNo m Lmo.
We will prove (- n) * (- m) ∈ int.
rewrite the current goal using mul_SNo_minus_distrL n (- m) LnS (SNo_minus_SNo m LmS) (from left to right).
We will prove - (n * (- m)) ∈ int.
rewrite the current goal using mul_SNo_com n (- m) LnS (SNo_minus_SNo m LmS) (from left to right).
We will prove - ((- m) * n) ∈ int.
rewrite the current goal using mul_SNo_minus_distrL m n LmS LnS (from left to right).
We will prove - - (m * n) ∈ int.
rewrite the current goal using minus_SNo_invol (m * n) (SNo_mul_SNo m n LmS LnS) (from left to right).
We will prove m * n ∈ int.
Apply Subq_omega_int to the current goal.
We will prove m * n ∈ ω.
An exact proof term for the current goal is mul_SNo_In_omega m Hm n Hn.
∎
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 Main Goal
End of Section Int
Beginning of Section SurrealAbs
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Definition. We define abs_SNo to be λx ⇒ if 0 ≤ x then x else - x of type set → set.
Theorem. (nonneg_abs_SNo) The following is provable:
∀x, 0 ≤ x → abs_SNo x = x
Proof:
Let x be given.
Assume Hx.
An exact proof term for the current goal is If_i_1 (0 ≤ x) x (- x) Hx.
∎
Try to prove it yourself. Main Goal
Theorem. (not_nonneg_abs_SNo) The following is provable:
∀x, ¬ (0 ≤ x) → abs_SNo x = - x
Proof:
Let x be given.
Assume Hx.
An exact proof term for the current goal is If_i_0 (0 ≤ x) x (- x) Hx.
∎
Try to prove it yourself. Main Goal
Theorem. (abs_SNo_0) The following is provable:
abs_SNo 0 = 0
Proof:
Apply nonneg_abs_SNo to the current goal.
We will prove 0 ≤ 0.
Apply SNoLe_ref to the current goal.
∎
Try to prove it yourself. Main Goal
Theorem. (pos_abs_SNo) The following is provable:
∀x, 0 < x → abs_SNo x = x
Proof:
Let x be given.
Assume Hx.
Apply nonneg_abs_SNo to the current goal.
We will prove 0 ≤ x.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hx.
∎
Try to prove it yourself. Main Goal
Theorem. (neg_abs_SNo) The following is provable:
∀x, SNo x → x < 0 → abs_SNo x = - x
Proof:
Let x be given.
Assume Hx1 Hx2.
Apply not_nonneg_abs_SNo to the current goal.
Assume H1: 0 ≤ x.
We will prove False.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
An exact proof term for the current goal is SNoLtLe_tra x 0 x Hx1 SNo_0 Hx1 Hx2 H1.
∎
Try to prove it yourself. Main Goal
Theorem. (SNo_abs_SNo) The following is provable:
∀x, SNo x → SNo (abs_SNo x)
Proof:
Let x be given.
Assume Hx.
Apply xm (0 ≤ x) to the current goal.
Assume H1.
rewrite the current goal using nonneg_abs_SNo x H1 (from left to right).
An exact proof term for the current goal is Hx.
Assume H1.
rewrite the current goal using not_nonneg_abs_SNo x H1 (from left to right).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hx.
∎
Try to prove it yourself. Main Goal
Theorem. (abs_SNo_Lev) The following is provable:
∀x, SNo x → SNoLev (abs_SNo x) = SNoLev x
Proof:
Let x be given.
Assume Hx.
Apply xm (0 ≤ x) to the current goal.
Assume H1.
rewrite the current goal using nonneg_abs_SNo x H1 (from left to right).
Use reflexivity.
Assume H1.
rewrite the current goal using not_nonneg_abs_SNo x H1 (from left to right).
Apply minus_SNo_Lev to the current goal.
An exact proof term for the current goal is Hx.
∎
Try to prove it yourself. Main Goal
Theorem. (abs_SNo_minus) The following is provable:
∀x, SNo x → abs_SNo (- x) = abs_SNo x
Proof:
Let x be given.
Assume Hx.
Apply SNoLtLe_or x 0 Hx SNo_0 to the current goal.
Assume H1: x < 0.
rewrite the current goal using neg_abs_SNo x Hx H1 (from left to right).
We will prove abs_SNo (- x) = - x.
We prove the intermediate claim L1: 0 ≤ - x.
Apply SNoLtLe to the current goal.
We will prove 0 < - x.
Apply minus_SNo_Lt_contra2 x 0 Hx SNo_0 to the current goal.
We will prove x < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is H1.
An exact proof term for the current goal is nonneg_abs_SNo (- x) L1.
Assume H1: 0 ≤ x.
Apply SNoLtLe_or (- x) 0 (SNo_minus_SNo x Hx) SNo_0 to the current goal.
Assume H2: - x < 0.
rewrite the current goal using nonneg_abs_SNo x H1 (from left to right).
rewrite the current goal using neg_abs_SNo (- x) (SNo_minus_SNo x Hx) H2 (from left to right).
We will prove - - x = x.
An exact proof term for the current goal is minus_SNo_invol x Hx.
Assume H2: 0 ≤ - x.
We prove the intermediate claim L2: x = 0.
Apply SNoLe_antisym x 0 Hx SNo_0 to the current goal.
We will prove x ≤ 0.
rewrite the current goal using minus_SNo_0 (from right to left).
rewrite the current goal using minus_SNo_invol x Hx (from right to left).
We will prove - - x ≤ - 0.
Apply minus_SNo_Le_contra 0 (- x) SNo_0 (SNo_minus_SNo x Hx) to the current goal.
We will prove 0 ≤ - x.
An exact proof term for the current goal is H2.
We will prove 0 ≤ x.
An exact proof term for the current goal is H1.
rewrite the current goal using L2 (from left to right).
Use f_equal.
An exact proof term for the current goal is minus_SNo_0.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal
Theorem. (abs_SNo_dist_swap) The following is provable:
∀x y, SNo x → SNo y → abs_SNo (x + - y) = abs_SNo (y + - x)
Proof:
Let x and y be given.
Assume Hx Hy.
We prove the intermediate claim Lmx: SNo (- x).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hx.
We prove the intermediate claim Lmy: SNo (- y).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hy.
We prove the intermediate claim Lymx: SNo (y + - x).
An exact proof term for the current goal is SNo_add_SNo y (- x) Hy Lmx.
Use transitivity with and abs_SNo (- (y + - x)).
Use f_equal.
We will prove x + - y = - (y + - x).
rewrite the current goal using minus_add_SNo_distr y (- x) Hy Lmx (from left to right).
We will prove x + - y = - y + - - x.
rewrite the current goal using minus_SNo_invol x Hx (from left to right).
We will prove x + - y = - y + x.
An exact proof term for the current goal is add_SNo_com x (- y) Hx Lmy.
An exact proof term for the current goal is abs_SNo_minus (y + - x) Lymx.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Main Goal
Theorem. (SNo_triangle) The following is provable:
∀x y, SNo x → SNo y → abs_SNo (x + y) ≤ abs_SNo x + abs_SNo y
Proof:
Let x and y be given.
Assume Hx Hy.
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx Hy.
We prove the intermediate claim Lmx: SNo (- x).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hx.
We prove the intermediate claim Lmy: SNo (- y).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hy.
Apply SNoLtLe_or x 0 Hx SNo_0 to the current goal.
Assume H1: x < 0.
rewrite the current goal using neg_abs_SNo x Hx H1 (from left to right).
Apply SNoLtLe_or y 0 Hy SNo_0 to the current goal.
Assume H2: y < 0.
rewrite the current goal using neg_abs_SNo y Hy H2 (from left to right).
We will prove abs_SNo (x + y) ≤ - x + - y.
We prove the intermediate claim L1: x + y < 0.
rewrite the current goal using add_SNo_0L 0 SNo_0 (from right to left).
We will prove x + y < 0 + 0.
An exact proof term for the current goal is add_SNo_Lt3 x y 0 0 Hx Hy SNo_0 SNo_0 H1 H2.
rewrite the current goal using neg_abs_SNo (x + y) Lxy L1 (from left to right).
We will prove - (x + y) ≤ - x + - y.
rewrite the current goal using minus_add_SNo_distr x y Hx Hy (from left to right).
Apply SNoLe_ref to the current goal.
Assume H2: 0 ≤ y.
rewrite the current goal using nonneg_abs_SNo y H2 (from left to right).
We will prove abs_SNo (x + y) ≤ - x + y.
Apply xm (0 ≤ x + y) to the current goal.
Assume H3.
rewrite the current goal using nonneg_abs_SNo (x + y) H3 (from left to right).
We will prove x + y ≤ - x + y.
Apply add_SNo_Le1 x y (- x) Hx Hy Lmx to the current goal.
We will prove x ≤ - x.
Apply SNoLtLe to the current goal.
We will prove x < - x.
Apply SNoLt_tra x 0 (- x) Hx SNo_0 Lmx H1 to the current goal.
We will prove 0 < - x.
Apply minus_SNo_Lt_contra2 x 0 Hx SNo_0 to the current goal.
We will prove x < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is H1.
Assume H3.
rewrite the current goal using not_nonneg_abs_SNo (x + y) H3 (from left to right).
We will prove - (x + y) ≤ - x + y.
rewrite the current goal using minus_add_SNo_distr x y Hx Hy (from left to right).
We will prove - x + - y ≤ - x + y.
Apply add_SNo_Le2 (- x) (- y) y Lmx Lmy Hy to the current goal.
We will prove - y ≤ y.
We prove the intermediate claim L2: - y ≤ 0.
rewrite the current goal using minus_SNo_0 (from right to left).
An exact proof term for the current goal is minus_SNo_Le_contra 0 y SNo_0 Hy H2.
An exact proof term for the current goal is SNoLe_tra (- y) 0 y Lmy SNo_0 Hy L2 H2.
Assume H1: 0 ≤ x.
rewrite the current goal using nonneg_abs_SNo x H1 (from left to right).
Apply SNoLtLe_or y 0 Hy SNo_0 to the current goal.
Assume H2: y < 0.
rewrite the current goal using neg_abs_SNo y Hy H2 (from left to right).
We will prove abs_SNo (x + y) ≤ x + - y.
Apply xm (0 ≤ x + y) to the current goal.
Assume H3.
rewrite the current goal using nonneg_abs_SNo (x + y) H3 (from left to right).
We will prove x + y ≤ x + - y.
Apply add_SNo_Le2 x y (- y) Hx Hy Lmy to the current goal.
We will prove y ≤ - y.
Apply SNoLtLe to the current goal.
We will prove y < - y.
Apply SNoLt_tra y 0 (- y) Hy SNo_0 Lmy H2 to the current goal.
We will prove 0 < - y.
Apply minus_SNo_Lt_contra2 y 0 Hy SNo_0 to the current goal.
We will prove y < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is H2.
Assume H3.
rewrite the current goal using not_nonneg_abs_SNo (x + y) H3 (from left to right).
We will prove - (x + y) ≤ x + - y.
rewrite the current goal using minus_add_SNo_distr x y Hx Hy (from left to right).
We will prove - x + - y ≤ x + - y.
Apply add_SNo_Le1 (- x) (- y) x Lmx Lmy Hx to the current goal.
We will prove - x ≤ x.
We prove the intermediate claim L3: - x ≤ 0.
rewrite the current goal using minus_SNo_0 (from right to left).
An exact proof term for the current goal is minus_SNo_Le_contra 0 x SNo_0 Hx H1.
An exact proof term for the current goal is SNoLe_tra (- x) 0 x Lmx SNo_0 Hx L3 H1.
Assume H2: 0 ≤ y.
rewrite the current goal using nonneg_abs_SNo y H2 (from left to right).
We will prove abs_SNo (x + y) ≤ x + y.
We prove the intermediate claim L1: 0 ≤ x + y.
rewrite the current goal using add_SNo_0L 0 SNo_0 (from right to left).
We will prove 0 + 0 ≤ x + y.
An exact proof term for the current goal is add_SNo_Le3 0 0 x y SNo_0 SNo_0 Hx Hy H1 H2.
rewrite the current goal using nonneg_abs_SNo (x + y) L1 (from left to right).
Apply SNoLe_ref to the current goal.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Subgoal 7 Main Goal
Theorem. (SNo_triangle2) The following is provable:
∀x y z, SNo x → SNo y → SNo z → abs_SNo (x + - z) ≤ abs_SNo (x + - y) + abs_SNo (y + - z)
Proof:
Let x, y and z be given.
Assume Hx Hy Hz.
We prove the intermediate claim Lmy: SNo (- y).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hy.
We prove the intermediate claim Lmz: SNo (- z).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hz.
We prove the intermediate claim L1: x + - z = (x + - y) + (y + - z).
rewrite the current goal using add_SNo_assoc x (- y) (y + - z) Hx Lmy (SNo_add_SNo y (- z) Hy Lmz) (from right to left).
We will prove x + - z = x + (- y + y + - z).
Use f_equal.
Use symmetry.
An exact proof term for the current goal is add_SNo_minus_L2 y (- z) Hy Lmz.
rewrite the current goal using L1 (from left to right).
Apply SNo_triangle to the current goal.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Lmy.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Lmz.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Main Goal
End of Section SurrealAbs
Beginning of Section SNoMaxMin
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Definition. We define SNo_max_of to be λX x ⇒ x ∈ X ∧ SNo x ∧ ∀y ∈ X, SNo y → y ≤ x of type set → set → prop.
Definition. We define SNo_min_of to be λX x ⇒ x ∈ X ∧ SNo x ∧ ∀y ∈ X, SNo y → x ≤ y of type set → set → prop.
Theorem. (minus_SNo_max_min) The following is provable:
∀X y, (∀x ∈ X, SNo x) → SNo_max_of X y → SNo_min_of {- x|x ∈ X} (- y)
Proof:
Let X and y be given.
Assume HX H1.
Apply H1 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1a: y ∈ X.
Assume H1b: SNo y.
Assume H1c: ∀z ∈ X, SNo z → z ≤ y.
We will prove - y ∈ {- x|x ∈ X} ∧ SNo (- y) ∧ (∀z ∈ {- x|x ∈ X}, SNo z → - y ≤ z).
Apply and3I to the current goal.
Apply ReplI to the current goal.
An exact proof term for the current goal is H1a.
An exact proof term for the current goal is SNo_minus_SNo y H1b.
Let z be given.
Assume Hz1: z ∈ {- x|x ∈ X}.
Assume Hz2: SNo z.
Apply ReplE_impred X (λx ⇒ - x) z Hz1 to the current goal.
Let x be given.
Assume Hx: x ∈ X.
Assume Hze: z = - x.
rewrite the current goal using Hze (from left to right).
We will prove - y ≤ - x.
Apply minus_SNo_Le_contra x y (HX x Hx) H1b to the current goal.
We will prove x ≤ y.
An exact proof term for the current goal is H1c x Hx (HX x Hx).
∎
Try to prove it yourself. Main Goal
Theorem. (minus_SNo_max_min') The following is provable:
∀X y, (∀x ∈ X, SNo x) → SNo_max_of {- x|x ∈ X} y → SNo_min_of X (- y)
Proof:
Let X and y be given.
Assume HX H1.
We prove the intermediate claim L1: {- z|z ∈ {- x|x ∈ X}} = X.
Apply Repl_invol_eq SNo minus_SNo to the current goal.
We will prove ∀x, SNo x → - - x = x.
An exact proof term for the current goal is minus_SNo_invol.
We will prove ∀x ∈ X, SNo x.
An exact proof term for the current goal is HX.
We prove the intermediate claim L2: ∀z ∈ {- x|x ∈ X}, SNo z.
Let z be given.
Assume Hz.
Apply ReplE_impred X (λx ⇒ - x) z Hz to the current goal.
Let x be given.
Assume Hx: x ∈ X.
Assume Hzx: z = - x.
rewrite the current goal using Hzx (from left to right).
Apply SNo_minus_SNo to the current goal.
We will prove SNo x.
An exact proof term for the current goal is HX x Hx.
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is minus_SNo_max_min {- x|x ∈ X} y L2 H1.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal
Theorem. (minus_SNo_min_max) The following is provable:
∀X y, (∀x ∈ X, SNo x) → SNo_min_of X y → SNo_max_of {- x|x ∈ X} (- y)
Proof:
Let X and y be given.
Assume HX H1.
Apply H1 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1a: y ∈ X.
Assume H1b: SNo y.
Assume H1c: ∀z ∈ X, SNo z → y ≤ z.
We will prove - y ∈ {- x|x ∈ X} ∧ SNo (- y) ∧ (∀z ∈ {- x|x ∈ X}, SNo z → z ≤ - y).
Apply and3I to the current goal.
Apply ReplI to the current goal.
An exact proof term for the current goal is H1a.
An exact proof term for the current goal is SNo_minus_SNo y H1b.
Let z be given.
Assume Hz1: z ∈ {- x|x ∈ X}.
Assume Hz2: SNo z.
Apply ReplE_impred X (λx ⇒ - x) z Hz1 to the current goal.
Let x be given.
Assume Hx: x ∈ X.
Assume Hze: z = - x.
rewrite the current goal using Hze (from left to right).
We will prove - x ≤ - y.
Apply minus_SNo_Le_contra y x H1b (HX x Hx) to the current goal.
We will prove y ≤ x.
An exact proof term for the current goal is H1c x Hx (HX x Hx).
∎
Try to prove it yourself. Main Goal
Theorem. (double_SNo_max_1) The following is provable:
∀x y, SNo x → SNo_max_of (SNoL x) y → ∀z, SNo z → x < z → y + z < x + x → ∃w ∈ SNoR z, y + w = x + x
Proof:
Let x and y be given.
Assume Hx Hy.
Apply Hy to the current goal.
Assume H.
Apply H to the current goal.
Assume Hy1: y ∈ SNoL x.
Assume Hy2: SNo y.
Assume Hy3: ∀w ∈ SNoL x, SNo w → w ≤ y.
Apply SNoL_E x Hx y Hy1 to the current goal.
Assume Hy1a.
Assume Hy1b: SNoLev y ∈ SNoLev x.
Assume Hy1c: y < x.
Apply SNoLev_ind to the current goal.
Let z be given.
Assume Hz: SNo z.
Assume IH: ∀w ∈ SNoS_ (SNoLev z), x < w → y + w < x + x → ∃u ∈ SNoR w, y + u = x + x.
Assume H1: x < z.
Assume H2: y + z < x + x.
We will prove ∃w ∈ SNoR z, y + w = x + x.
We prove the intermediate claim Lxx: SNo (x + x).
An exact proof term for the current goal is SNo_add_SNo x x Hx Hx.
We prove the intermediate claim Lyz: SNo (y + z).
An exact proof term for the current goal is SNo_add_SNo y z Hy2 Hz.
We prove the intermediate claim L1: ∀w ∈ SNoR y, w + z ≤ x + x → False.
Let w be given.
Assume Hw.
Assume H3: w + z ≤ x + x.
Apply SNoR_E y Hy2 w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev y.
Assume Hw3: y < w.
Apply SNoLt_irref (x + x) to the current goal.
We will prove x + x < x + x.
Apply SNoLtLe_tra (x + x) (w + z) (x + x) Lxx (SNo_add_SNo w z Hw1 Hz) Lxx to the current goal.
We will prove x + x < w + z.
Apply add_SNo_Lt3b x x w z Hx Hx Hw1 Hz to the current goal.
We will prove x ≤ w.
Apply SNoLtLe_or w x Hw1 Hx to the current goal.
Assume H4: w < x.
We prove the intermediate claim L1a: w ∈ SNoL x.
Apply SNoL_I x Hx w Hw1 to the current goal.
We will prove SNoLev w ∈ SNoLev x.
An exact proof term for the current goal is ordinal_TransSet (SNoLev x) (SNoLev_ordinal x Hx) (SNoLev y) Hy1b (SNoLev w) Hw2.
We will prove w < x.
An exact proof term for the current goal is H4.
Apply SNoLt_irref y to the current goal.
We will prove y < y.
Apply SNoLtLe_tra y w y Hy2 Hw1 Hy2 Hw3 to the current goal.
We will prove w ≤ y.
An exact proof term for the current goal is Hy3 w L1a Hw1.
Assume H4: x ≤ w.
An exact proof term for the current goal is H4.
We will prove x < z.
An exact proof term for the current goal is H1.
We will prove w + z ≤ x + x.
An exact proof term for the current goal is H3.
We prove the intermediate claim L2: ∀w ∈ SNoL x, y + z ≤ w + x → False.
Let w be given.
Assume Hw.
Assume H3: y + z ≤ w + 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.
Apply SNoLt_irref (w + x) to the current goal.
We will prove w + x < w + x.
Apply SNoLtLe_tra (w + x) (w + z) (w + x) (SNo_add_SNo w x Hw1 Hx) (SNo_add_SNo w z Hw1 Hz) (SNo_add_SNo w x Hw1 Hx) to the current goal.
We will prove w + x < w + z.
Apply add_SNo_Lt2 w x z Hw1 Hx Hz to the current goal.
We will prove x < z.
An exact proof term for the current goal is H1.
We will prove w + z ≤ w + x.
Apply SNoLe_tra (w + z) (y + z) (w + x) (SNo_add_SNo w z Hw1 Hz) Lyz (SNo_add_SNo w x Hw1 Hx) to the current goal.
We will prove w + z ≤ y + z.
Apply add_SNo_Le1 w z y Hw1 Hz Hy2 to the current goal.
We will prove w ≤ y.
An exact proof term for the current goal is Hy3 w Hw Hw1.
We will prove y + z ≤ w + x.
An exact proof term for the current goal is H3.
We prove the intermediate claim L3: ∀w ∈ SNoR z, y + w < x + x → ∃w ∈ SNoR z, y + w = x + x.
Let w be given.
Assume Hw: w ∈ SNoR z.
Assume H4: y + w < x + x.
Apply SNoR_E z Hz w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2.
Assume Hw3: z < w.
We prove the intermediate claim LIH: ∃u ∈ SNoR w, y + u = x + x.
Apply IH w (SNoR_SNoS_ z w Hw) to the current goal.
We will prove x < w.
An exact proof term for the current goal is SNoLt_tra x z w Hx Hz Hw1 H1 Hw3.
We will prove y + w < x + x.
An exact proof term for the current goal is H4.
Apply LIH to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Assume Hu1: u ∈ SNoR w.
Assume Hu2: y + u = x + x.
Apply SNoR_E w Hw1 u Hu1 to the current goal.
Assume Hu1a Hu1b Hu1c.
We use u to witness the existential quantifier.
Apply andI to the current goal.
We will prove u ∈ SNoR z.
Apply SNoR_I z Hz u Hu1a to the current goal.
We will prove SNoLev u ∈ SNoLev z.
An exact proof term for the current goal is ordinal_TransSet (SNoLev z) (SNoLev_ordinal z Hz) (SNoLev w) Hw2 (SNoLev u) Hu1b.
We will prove z < u.
An exact proof term for the current goal is SNoLt_tra z w u Hz Hw1 Hu1a Hw3 Hu1c.
An exact proof term for the current goal is Hu2.
Apply SNoLt_SNoL_or_SNoR_impred (y + z) (x + x) Lyz Lxx H2 to the current goal.
Let u be given.
Assume Hu1: u ∈ SNoL (x + x).
Assume Hu2: u ∈ SNoR (y + z).
Apply SNoL_E (x + x) Lxx u Hu1 to the current goal.
Assume Hu1a: SNo u.
Assume Hu1b.
Assume Hu1c: u < x + x.
Apply add_SNo_SNoR_interpolate y z Hy2 Hz u Hu2 to the current goal.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR y.
Assume H4: w + z ≤ u.
Apply SNoR_E y Hy2 w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2.
Assume Hw3: y < w.
We will prove False.
Apply L1 w Hw to the current goal.
We will prove w + z ≤ x + x.
Apply SNoLtLe to the current goal.
We will prove w + z < x + x.
Apply SNoLeLt_tra (w + z) u (x + x) (SNo_add_SNo w z Hw1 Hz) Hu1a Lxx H4 to the current goal.
We will prove u < x + x.
An exact proof term for the current goal is Hu1c.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR z.
Assume H4: y + w ≤ u.
Apply SNoR_E z Hz w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2.
Assume Hw3: z < w.
Apply L3 w Hw to the current goal.
We will prove y + w < x + x.
Apply SNoLeLt_tra (y + w) u (x + x) (SNo_add_SNo y w Hy2 Hw1) Hu1a Lxx H4 to the current goal.
We will prove u < x + x.
An exact proof term for the current goal is Hu1c.
Assume H3: y + z ∈ SNoL (x + x).
We will prove False.
Apply add_SNo_SNoL_interpolate x x Hx Hx (y + z) H3 to the current goal.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoL x.
Assume H4: y + z ≤ w + x.
An exact proof term for the current goal is L2 w Hw H4.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoL x.
Assume H4: y + z ≤ x + w.
Apply SNoL_E x Hx w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
Apply L2 w Hw to the current goal.
We will prove y + z ≤ w + x.
rewrite the current goal using add_SNo_com w x Hw1 Hx (from left to right).
We will prove y + z ≤ x + w.
An exact proof term for the current goal is H4.
Assume H3: x + x ∈ SNoR (y + z).
Apply add_SNo_SNoR_interpolate y z Hy2 Hz (x + x) H3 to the current goal.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR y.
Assume H4: w + z ≤ x + x.
We will prove False.
An exact proof term for the current goal is L1 w Hw H4.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR z.
Assume H4: y + w ≤ x + x.
Apply SNoR_E z Hz w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev z.
Assume Hw3: z < w.
Apply SNoLtLe_or (y + w) (x + x) (SNo_add_SNo y w Hy2 Hw1) Lxx to the current goal.
Assume H5: y + w < x + x.
We will prove ∃w ∈ SNoR z, y + w = x + x.
Apply L3 w Hw to the current goal.
We will prove y + w < x + x.
An exact proof term for the current goal is H5.
Assume H5: x + x ≤ y + w.
We will prove ∃w ∈ SNoR z, y + w = x + x.
We use w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw.
Apply SNoLe_antisym (y + w) (x + x) (SNo_add_SNo y w Hy2 Hw1) Lxx to the current goal.
An exact proof term for the current goal is H4.
An exact proof term for the current goal is H5.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Subgoal 7 Main Goal
Theorem. (double_SNo_min_1) The following is provable:
∀x y, SNo x → SNo_min_of (SNoR x) y → ∀z, SNo z → z < x → x + x < y + z → ∃w ∈ SNoL z, y + w = x + x
Proof:
Let x and y be given.
Assume Hx Hy.
Apply Hy to the current goal.
Assume H.
Apply H to the current goal.
Assume Hy1: y ∈ SNoR x.
Assume Hy2: SNo y.
Assume Hy3: ∀w ∈ SNoR x, SNo w → y ≤ w.
Apply SNoR_E x Hx y Hy1 to the current goal.
Assume Hy1a.
Assume Hy1b: SNoLev y ∈ SNoLev x.
Assume Hy1c: x < y.
Let z be given.
Assume Hz: SNo z.
Assume H1: z < x.
Assume H2: x + x < y + z.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Hx.
We prove the intermediate claim Lmy: SNo (- y).
An exact proof term for the current goal is SNo_minus_SNo y Hy2.
We prove the intermediate claim Lmz: SNo (- z).
An exact proof term for the current goal is SNo_minus_SNo z Hz.
We prove the intermediate claim Lxx: SNo (x + x).
An exact proof term for the current goal is SNo_add_SNo x x Hx Hx.
We prove the intermediate claim Lyz: SNo (y + z).
An exact proof term for the current goal is SNo_add_SNo y z Hy2 Hz.
We prove the intermediate claim L1: SNo_max_of (SNoL (- x)) (- y).
rewrite the current goal using SNoL_minus_SNoR x Hx (from left to right).
We will prove SNo_max_of {- w|w ∈ SNoR x} (- y).
Apply minus_SNo_min_max to the current goal.
We will prove ∀w ∈ SNoR x, SNo w.
Let w be given.
Assume Hw.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw1 _ _.
An exact proof term for the current goal is Hw1.
We will prove SNo_min_of (SNoR x) y.
An exact proof term for the current goal is Hy.
We prove the intermediate claim L2: - x < - z.
An exact proof term for the current goal is minus_SNo_Lt_contra z x Hz Hx H1.
We prove the intermediate claim L3: - y + - z < - x + - x.
rewrite the current goal using minus_add_SNo_distr y z Hy2 Hz (from right to left).
rewrite the current goal using minus_add_SNo_distr x x Hx Hx (from right to left).
An exact proof term for the current goal is minus_SNo_Lt_contra (x + x) (y + z) Lxx Lyz H2.
Apply double_SNo_max_1 (- x) (- y) Lmx L1 (- z) Lmz L2 L3 to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR (- z).
rewrite the current goal using minus_add_SNo_distr x x Hx Hx (from right to left).
Assume H3: - y + w = - (x + x).
Apply SNoR_E (- z) Lmz w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev (- z).
Assume Hw3: - z < w.
We prove the intermediate claim Lmw: SNo (- w).
An exact proof term for the current goal is SNo_minus_SNo w Hw1.
We use (- w) to witness the existential quantifier.
Apply andI to the current goal.
We will prove - w ∈ SNoL z.
rewrite the current goal using minus_SNo_invol z Hz (from right to left).
We will prove - w ∈ SNoL (- - z).
rewrite the current goal using SNoL_minus_SNoR (- z) Lmz (from left to right).
We will prove - w ∈ {- w|w ∈ SNoR (- z)}.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hw.
We will prove y + - w = x + x.
rewrite the current goal using minus_SNo_invol (x + x) Lxx (from right to left).
We will prove y + - w = - - (x + x).
rewrite the current goal using H3 (from right to left).
We will prove y + - w = - (- y + w).
rewrite the current goal using minus_add_SNo_distr (- y) w Lmy Hw1 (from left to right).
We will prove y + - w = - - y + - w.
rewrite the current goal using minus_SNo_invol y Hy2 (from left to right).
Use reflexivity.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Subgoal 7 Subgoal 8 Subgoal 9 Main Goal
Theorem. (finite_max_exists) The following is provable:
∀X, (∀x ∈ X, SNo x) → finite X → X ≠ 0 → ∃x, SNo_max_of X x
Proof:
We prove the intermediate claim L1: ∀n, nat_p n → ∀X, (∀x ∈ X, SNo x) → equip X (ordsucc n) → ∃x, SNo_max_of X x.
Apply nat_ind to the current goal.
Let X be given.
Assume HX.
Assume H1: equip X 1.
Apply equip_sym X 1 H1 to the current goal.
Let f be given.
Assume Hf: bij 1 X f.
Apply bijE 1 X f Hf to the current goal.
Assume Hf1 Hf2 Hf3.
We use f 0 to witness the existential quantifier.
We will prove SNo_max_of X (f 0).
We will prove f 0 ∈ X ∧ SNo (f 0) ∧ ∀y ∈ X, SNo y → y ≤ f 0.
We prove the intermediate claim Lf0X: f 0 ∈ X.
An exact proof term for the current goal is Hf1 0 In_0_1.
Apply and3I to the current goal.
We will prove f 0 ∈ X.
An exact proof term for the current goal is Lf0X.
An exact proof term for the current goal is HX (f 0) Lf0X.
Let y be given.
Assume Hy: y ∈ X.
Assume Hy2: SNo y.
Apply Hf3 y Hy to the current goal.
Let i be given.
Assume H.
Apply H to the current goal.
Assume Hi: i ∈ 1.
Assume Hyi: f i = y.
We will prove y ≤ f 0.
rewrite the current goal using Hyi (from right to left).
Apply cases_1 i Hi to the current goal.
We will prove f 0 ≤ f 0.
Apply SNoLe_ref to the current goal.
Let n be given.
Assume Hn.
Assume IHn: ∀X, (∀x ∈ X, SNo x) → equip X (ordsucc n) → ∃x, SNo_max_of X x.
Let X be given.
Assume HX.
Assume H1: equip X (ordsucc (ordsucc n)).
Apply equip_sym X (ordsucc (ordsucc n)) H1 to the current goal.
Let f be given.
Assume Hf: bij (ordsucc (ordsucc n)) X f.
Apply bijE (ordsucc (ordsucc n)) X f Hf to the current goal.
Assume Hf1 Hf2 Hf3.
Set X' to be the term {f i|i ∈ ordsucc n}.
We prove the intermediate claim LX'1: X' ⊆ X.
Let w be given.
Assume Hw: w ∈ X'.
Apply ReplE_impred (ordsucc n) f w Hw to the current goal.
Let i be given.
Assume Hi: i ∈ ordsucc n.
Assume Hwi: w = f i.
rewrite the current goal using Hwi (from left to right).
We will prove f i ∈ X.
Apply Hf1 i to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
We prove the intermediate claim LX'2: equip X' (ordsucc n).
Apply equip_sym to the current goal.
We will prove ∃f : set → set, bij (ordsucc n) X' f.
We use f to witness the existential quantifier.
Apply bijI to the current goal.
Let i be given.
Assume Hi: i ∈ ordsucc n.
We will prove f i ∈ X'.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hi.
Let i be given.
Assume Hi.
Let j be given.
Assume Hj.
Assume Hij: f i = f j.
Apply Hf2 to the current goal.
We will prove i ∈ ordsucc (ordsucc n).
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
We will prove j ∈ ordsucc (ordsucc n).
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hj.
An exact proof term for the current goal is Hij.
Let w be given.
Assume Hw: w ∈ X'.
Apply ReplE_impred (ordsucc n) f w Hw to the current goal.
Let i be given.
Assume Hi: i ∈ ordsucc n.
Assume Hwi: w = f i.
We use i to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hi.
Use symmetry.
An exact proof term for the current goal is Hwi.
Apply IHn X' (λx' Hx' ⇒ HX x' (LX'1 x' Hx')) LX'2 to the current goal.
Let z be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume Hz1: z ∈ X'.
Assume Hz2: SNo z.
Assume Hz3: ∀y ∈ X', SNo y → y ≤ z.
We prove the intermediate claim Lfn1: f (ordsucc n) ∈ X.
Apply Hf1 (ordsucc n) to the current goal.
Apply ordsuccI2 to the current goal.
We prove the intermediate claim Lfn1': SNo (f (ordsucc n)).
Apply HX (f (ordsucc n)) Lfn1 to the current goal.
Apply SNoLtLe_or z (f (ordsucc n)) Hz2 Lfn1' to the current goal.
Assume H2: z < f (ordsucc n).
We use (f (ordsucc n)) to witness the existential quantifier.
We will prove f (ordsucc n) ∈ X ∧ SNo (f (ordsucc n)) ∧ ∀y ∈ X, SNo y → y ≤ f (ordsucc n).
Apply and3I to the current goal.
An exact proof term for the current goal is Lfn1.
An exact proof term for the current goal is Lfn1'.
Let y be given.
Assume Hy Hy2.
Apply Hf3 y Hy to the current goal.
Let i be given.
Assume H.
Apply H to the current goal.
Assume Hi: i ∈ ordsucc (ordsucc n).
Assume Hyi: f i = y.
Apply ordsuccE (ordsucc n) i Hi to the current goal.
Assume H3: i ∈ ordsucc n.
We will prove y ≤ f (ordsucc n).
Apply SNoLe_tra y z (f (ordsucc n)) Hy2 Hz2 Lfn1' to the current goal.
We will prove y ≤ z.
Apply Hz3 y to the current goal.
We will prove y ∈ X'.
rewrite the current goal using Hyi (from right to left).
We will prove f i ∈ X'.
Apply ReplI to the current goal.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is Hy2.
We will prove z ≤ f (ordsucc n).
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is H2.
Assume H3: i = ordsucc n.
rewrite the current goal using Hyi (from right to left).
rewrite the current goal using H3 (from left to right).
We will prove f (ordsucc n) ≤ f (ordsucc n).
Apply SNoLe_ref to the current goal.
Assume H2: f (ordsucc n) ≤ z.
We use z to witness the existential quantifier.
We will prove z ∈ X ∧ SNo z ∧ ∀y ∈ X, SNo y → y ≤ z.
Apply and3I to the current goal.
An exact proof term for the current goal is LX'1 z Hz1.
An exact proof term for the current goal is Hz2.
Let y be given.
Assume Hy Hy2.
Apply Hf3 y Hy to the current goal.
Let i be given.
Assume H.
Apply H to the current goal.
Assume Hi: i ∈ ordsucc (ordsucc n).
Assume Hyi: f i = y.
Apply ordsuccE (ordsucc n) i Hi to the current goal.
Assume H3: i ∈ ordsucc n.
We will prove y ≤ z.
Apply Hz3 y to the current goal.
We will prove y ∈ X'.
rewrite the current goal using Hyi (from right to left).
We will prove f i ∈ X'.
Apply ReplI to the current goal.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is Hy2.
Assume H3: i = ordsucc n.
rewrite the current goal using Hyi (from right to left).
rewrite the current goal using H3 (from left to right).
We will prove f (ordsucc n) ≤ z.
An exact proof term for the current goal is H2.
Let X be given.
Assume HX.
Assume H1: finite X.
Apply H1 to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ∈ ω.
Apply nat_inv n (omega_nat_p n Hn) to the current goal.
Assume Hn0: n = 0.
rewrite the current goal using Hn0 (from left to right).
Assume H2: equip X 0.
Assume H3: X ≠ 0.
We will prove False.
Apply H2 to the current goal.
Let f be given.
Assume Hf: bij X 0 f.
Apply bijE X 0 f Hf to the current goal.
Assume Hf1 _ _.
Apply H3 to the current goal.
Apply Empty_eq to the current goal.
Let x be given.
Assume Hx.
Apply EmptyE (f x) to the current goal.
An exact proof term for the current goal is Hf1 x Hx.
Assume H.
Apply H to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: nat_p m.
Assume Hnm: n = ordsucc m.
rewrite the current goal using Hnm (from left to right).
Assume H2: equip X (ordsucc m).
Assume _.
An exact proof term for the current goal is L1 m Hm X HX H2.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Main Goal
Theorem. (finite_min_exists) The following is provable:
∀X, (∀x ∈ X, SNo x) → finite X → X ≠ 0 → ∃x, SNo_min_of X x
Proof:
Let X be given.
Assume HX: ∀x ∈ X, SNo x.
Assume H1: finite X.
Assume H2: X ≠ 0.
Set X' to be the term {- x|x ∈ X}.
We prove the intermediate claim L1: ∀z ∈ X', SNo z.
Let z be given.
Assume Hz.
Apply ReplE_impred X (λx ⇒ - x) z Hz to the current goal.
Let x be given.
Assume Hx: x ∈ X.
Assume Hzx: z = - x.
rewrite the current goal using Hzx (from left to right).
Apply SNo_minus_SNo to the current goal.
We will prove SNo x.
An exact proof term for the current goal is HX x Hx.
We prove the intermediate claim L2: finite X'.
Apply H1 to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ∈ ω.
Assume H3: equip X n.
We will prove ∃n ∈ ω, equip X' n.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn.
We will prove equip X' n.
Apply equip_tra X' X n to the current goal.
We will prove equip X' X.
Apply equip_sym to the current goal.
We will prove equip X X'.
We will prove ∃f : set → set, bij X X' f.
We use minus_SNo to witness the existential quantifier.
Apply bijI to the current goal.
Let x be given.
Assume Hx: x ∈ X.
We will prove - x ∈ X'.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hx.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
Assume Hxx': - x = - x'.
We will prove x = x'.
Use transitivity with - - x, and - - x'.
Use symmetry.
An exact proof term for the current goal is minus_SNo_invol x (HX x Hx).
Use f_equal.
An exact proof term for the current goal is Hxx'.
An exact proof term for the current goal is minus_SNo_invol x' (HX x' Hx').
Let w be given.
Assume Hw: w ∈ X'.
Apply ReplE_impred X (λx ⇒ - x) w Hw to the current goal.
Let x be given.
Assume Hx.
Assume Hwx: w = - x.
We will prove ∃u ∈ X, - u = w.
We use x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hx.
Use symmetry.
An exact proof term for the current goal is Hwx.
We will prove equip X n.
An exact proof term for the current goal is H3.
We prove the intermediate claim L3: X' ≠ 0.
Assume H1: X' = 0.
Apply H2 to the current goal.
We will prove X = 0.
Apply Empty_eq to the current goal.
Let x be given.
Assume Hx: x ∈ X.
Apply EmptyE (- x) to the current goal.
We will prove - x ∈ 0.
rewrite the current goal using H1 (from right to left).
Apply ReplI to the current goal.
An exact proof term for the current goal is Hx.
Apply finite_max_exists X' L1 L2 L3 to the current goal.
Let y be given.
Assume Hy: SNo_max_of X' y.
We use (- y) to witness the existential quantifier.
We will prove SNo_min_of X (- y).
An exact proof term for the current goal is minus_SNo_max_min' X y HX Hy.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Main Goal
Theorem. (SNoS_omega_SNoL_max_exists) The following is provable:
∀x ∈ SNoS_ ω, SNoL x = 0 ∨ ∃y, SNo_max_of (SNoL x) y
Proof:
Let x be given.
Assume Hx.
Apply xm (SNoL x = 0) to the current goal.
Assume H1: SNoL x = 0.
Apply orIL to the current goal.
An exact proof term for the current goal is H1.
Assume H1: SNoL x ≠ 0.
Apply orIR to the current goal.
We prove the intermediate claim L1: ∀y ∈ SNoL x, SNo y.
Let y be given.
Assume Hy.
Apply SNoS_E2 ω omega_ordinal x Hx to the current goal.
Assume _ _ Hx3 _.
Apply SNoL_E x Hx3 y Hy to the current goal.
Assume H _ _.
An exact proof term for the current goal is H.
An exact proof term for the current goal is finite_max_exists (SNoL x) L1 (SNoS_omega_SNoL_finite x Hx) H1.
∎
Try to prove it yourself. Subgoal 1 Main Goal
Theorem. (SNoS_omega_SNoR_min_exists) The following is provable:
∀x ∈ SNoS_ ω, SNoR x = 0 ∨ ∃y, SNo_min_of (SNoR x) y
Proof:
Let x be given.
Assume Hx.
Apply xm (SNoR x = 0) to the current goal.
Assume H1: SNoR x = 0.
Apply orIL to the current goal.
An exact proof term for the current goal is H1.
Assume H1: SNoR x ≠ 0.
Apply orIR to the current goal.
We prove the intermediate claim L1: ∀y ∈ SNoR x, SNo y.
Let y be given.
Assume Hy.
Apply SNoS_E2 ω omega_ordinal x Hx to the current goal.
Assume _ _ Hx3 _.
Apply SNoR_E x Hx3 y Hy to the current goal.
Assume H _ _.
An exact proof term for the current goal is H.
An exact proof term for the current goal is finite_min_exists (SNoR x) L1 (SNoS_omega_SNoR_finite x Hx) H1.
∎
Try to prove it yourself. Subgoal 1 Main Goal
End of Section SNoMaxMin
Beginning of Section DiadicRationals
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Theorem. (nonneg_diadic_rational_p_SNoS_omega) The following is provable:
∀k ∈ ω, ∀n, nat_p n → eps_ k * n ∈ SNoS_ ω
Proof:
Let k be given.
Assume Hk.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hk.
We prove the intermediate claim Lek2: eps_ k ∈ SNoS_ ω.
An exact proof term for the current goal is SNo_eps_SNoS_omega k Hk.
Apply nat_ind to the current goal.
We will prove eps_ k * 0 ∈ SNoS_ ω.
rewrite the current goal using mul_SNo_zeroR (eps_ k) Lek (from left to right).
We will prove 0 ∈ SNoS_ ω.
An exact proof term for the current goal is omega_SNoS_omega 0 (nat_p_omega 0 nat_0).
Let n be given.
Assume Hn.
Assume IHn: eps_ k * n ∈ SNoS_ ω.
We will prove eps_ k * ordsucc n ∈ SNoS_ ω.
rewrite the current goal using add_SNo_1_ordsucc n (nat_p_omega n Hn) (from right to left).
We will prove eps_ k * (n + 1) ∈ SNoS_ ω.
rewrite the current goal using mul_SNo_distrL (eps_ k) n 1 Lek (omega_SNo n (nat_p_omega n Hn)) (omega_SNo 1 (nat_p_omega 1 nat_1)) (from left to right).
We will prove eps_ k * n + eps_ k * 1 ∈ SNoS_ ω.
rewrite the current goal using mul_SNo_oneR (eps_ k) Lek (from left to right).
We will prove eps_ k * n + eps_ k ∈ SNoS_ ω.
Apply add_SNo_SNoS_omega to the current goal.
An exact proof term for the current goal is IHn.
An exact proof term for the current goal is SNo_eps_SNoS_omega k Hk.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal
Definition. We define diadic_rational_p to be λx ⇒ ∃k ∈ ω, ∃m ∈ int, x = eps_ k * m of type set → prop.
Theorem. (diadic_rational_p_SNoS_omega) The following is provable:
∀x, diadic_rational_p x → x ∈ SNoS_ ω
Proof:
Let x be given.
Assume H.
Apply H to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: k ∈ ω.
Assume H.
Apply H to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ int.
Assume Hxkm: x = eps_ k * m.
rewrite the current goal using Hxkm (from left to right).
We will prove eps_ k * m ∈ SNoS_ ω.
We prove the intermediate claim L1: ∀n ∈ ω, eps_ k * n ∈ SNoS_ ω.
Let n be given.
Assume Hn: n ∈ ω.
We will prove eps_ k * n ∈ SNoS_ ω.
An exact proof term for the current goal is nonneg_diadic_rational_p_SNoS_omega k Hk n (omega_nat_p n Hn).
We prove the intermediate claim L2: ∀n ∈ ω, eps_ k * (- n) ∈ SNoS_ ω.
Let n be given.
Assume Hn: n ∈ ω.
We will prove eps_ k * (- n) ∈ SNoS_ ω.
rewrite the current goal using mul_SNo_minus_distrR (eps_ k) n (SNo_eps_ k Hk) (omega_SNo n Hn) (from left to right).
Apply minus_SNo_SNoS_omega to the current goal.
An exact proof term for the current goal is nonneg_diadic_rational_p_SNoS_omega k Hk n (omega_nat_p n Hn).
An exact proof term for the current goal is int_SNo_cases (λm ⇒ eps_ k * m ∈ SNoS_ ω) L1 L2 m Hm.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal
Theorem. (int_diadic_rational_p) The following is provable:
∀m ∈ int, diadic_rational_p m
Proof:
Let m be given.
Assume Hm.
We will prove ∃k ∈ ω, ∃m' ∈ int, m = eps_ k * m'.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is nat_p_omega 0 nat_0.
We use m to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hm.
We will prove m = eps_ 0 * m.
rewrite the current goal using eps_0_1 (from left to right).
Use symmetry.
An exact proof term for the current goal is mul_SNo_oneL m (int_SNo m Hm).
∎
Try to prove it yourself. Main Goal
Theorem. (omega_diadic_rational_p) The following is provable:
∀m ∈ ω, diadic_rational_p m
Proof:
Let m be given.
Assume Hm.
Apply int_diadic_rational_p to the current goal.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is Hm.
∎
Try to prove it yourself. Main Goal
Theorem. (eps_diadic_rational_p) The following is provable:
∀k ∈ ω, diadic_rational_p (eps_ k)
Proof:
Let k be given.
Assume Hk.
We will prove ∃k' ∈ ω, ∃m ∈ int, eps_ k = eps_ k' * m.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is nat_p_omega 1 nat_1.
We will prove eps_ k = eps_ k * 1.
Use symmetry.
An exact proof term for the current goal is mul_SNo_oneR (eps_ k) (SNo_eps_ k Hk).
∎
Try to prove it yourself. Main Goal
Theorem. (minus_SNo_diadic_rational_p) The following is provable:
∀x, diadic_rational_p x → diadic_rational_p (- x)
Proof:
Let x be given.
Assume H.
Apply H to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: k ∈ ω.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hk.
Assume H.
Apply H to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ int.
Assume Hxkm: x = eps_ k * m.
We prove the intermediate claim Lm: SNo m.
An exact proof term for the current goal is int_SNo m Hm.
We prove the intermediate claim Lekm: SNo (eps_ k * m).
An exact proof term for the current goal is SNo_mul_SNo (eps_ k) m Lek Lm.
We will prove ∃k' ∈ ω, ∃m' ∈ int, - x = eps_ k' * m'.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
We use (- m) to witness the existential quantifier.
Apply andI to the current goal.
Apply int_minus_SNo to the current goal.
An exact proof term for the current goal is Hm.
We will prove - x = eps_ k * (- m).
rewrite the current goal using mul_SNo_minus_distrR (eps_ k) m (SNo_eps_ k Hk) Lm (from left to right).
We will prove - x = - eps_ k * m.
Use f_equal.
An exact proof term for the current goal is Hxkm.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Main Goal
Theorem. (mul_SNo_diadic_rational_p) The following is provable:
∀x y, diadic_rational_p x → diadic_rational_p y → diadic_rational_p (x * y)
Proof:
Let x and y be given.
Assume Hx.
Apply Hx to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: k ∈ ω.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hk.
Assume H.
Apply H to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ int.
Assume Hxkm: x = eps_ k * m.
We prove the intermediate claim Lm: SNo m.
An exact proof term for the current goal is int_SNo m Hm.
We prove the intermediate claim Lekm: SNo (eps_ k * m).
An exact proof term for the current goal is SNo_mul_SNo (eps_ k) m Lek Lm.
Assume Hy.
Apply Hy to the current goal.
Let l be given.
Assume H.
Apply H to the current goal.
Assume Hl: l ∈ ω.
We prove the intermediate claim Lel: SNo (eps_ l).
An exact proof term for the current goal is SNo_eps_ l Hl.
Assume H.
Apply H to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ∈ int.
We prove the intermediate claim Ln: SNo n.
An exact proof term for the current goal is int_SNo n Hn.
We prove the intermediate claim Leln: SNo (eps_ l * n).
An exact proof term for the current goal is SNo_mul_SNo (eps_ l) n Lel Ln.
Assume Hyln: y = eps_ l * n.
We will prove ∃k' ∈ ω, ∃m' ∈ int, x * y = eps_ k' * m'.
We use (k + l) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is add_SNo_In_omega k Hk l Hl.
We use (m * n) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is int_mul_SNo m Hm n Hn.
We will prove x * y = eps_ (k + l) * (m * n).
rewrite the current goal using mul_SNo_eps_eps_add_SNo k Hk l Hl (from right to left).
We will prove x * y = (eps_ k * eps_ l) * (m * n).
rewrite the current goal using mul_SNo_com_4_inner_mid (eps_ k) (eps_ l) m n Lek Lel Lm Ln (from left to right).
We will prove x * y = (eps_ k * m) * (eps_ l * n).
Use f_equal.
An exact proof term for the current goal is Hxkm.
An exact proof term for the current goal is Hyln.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Main Goal
Theorem. (add_SNo_diadic_rational_p) The following is provable:
∀x y, diadic_rational_p x → diadic_rational_p y → diadic_rational_p (x + y)
Proof:
Let x and y be given.
Assume Hx.
Apply Hx to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: k ∈ ω.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hk.
Assume H.
Apply H to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ int.
Assume Hxkm: x = eps_ k * m.
We prove the intermediate claim Lm: SNo m.
An exact proof term for the current goal is int_SNo m Hm.
We prove the intermediate claim Lekm: SNo (eps_ k * m).
An exact proof term for the current goal is SNo_mul_SNo (eps_ k) m Lek Lm.
Assume Hy.
Apply Hy to the current goal.
Let l be given.
Assume H.
Apply H to the current goal.
Assume Hl: l ∈ ω.
We prove the intermediate claim Lel: SNo (eps_ l).
An exact proof term for the current goal is SNo_eps_ l Hl.
Assume H.
Apply H to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ∈ int.
Assume Hyln: y = eps_ l * n.
We prove the intermediate claim Ln: SNo n.
An exact proof term for the current goal is int_SNo n Hn.
We prove the intermediate claim Leln: SNo (eps_ l * n).
An exact proof term for the current goal is SNo_mul_SNo (eps_ l) n Lel Ln.
We will prove ∃k' ∈ ω, ∃m' ∈ int, x + y = eps_ k' * m'.
We use (k + l) to witness the existential quantifier.
Apply andI to the current goal.
We will prove k + l ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega k Hk l Hl.
We use (2 ^ l * m + 2 ^ k * n) to witness the existential quantifier.
We prove the intermediate claim L2l: 2 ^ l ∈ int.
Apply Subq_omega_int to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_exp_SNo_nat 2 nat_2 l (omega_nat_p l Hl).
We prove the intermediate claim L2lm: 2 ^ l * m ∈ int.
Apply int_mul_SNo to the current goal.
An exact proof term for the current goal is L2l.
An exact proof term for the current goal is Hm.
We prove the intermediate claim L2k: 2 ^ k ∈ int.
Apply Subq_omega_int to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_exp_SNo_nat 2 nat_2 k (omega_nat_p k Hk).
We prove the intermediate claim L2kn: 2 ^ k * n ∈ int.
Apply int_mul_SNo to the current goal.
An exact proof term for the current goal is L2k.
An exact proof term for the current goal is Hn.
Apply andI to the current goal.
We will prove 2 ^ l * m + 2 ^ k * n ∈ int.
Apply int_add_SNo to the current goal.
An exact proof term for the current goal is L2lm.
An exact proof term for the current goal is L2kn.
We will prove x + y = eps_ (k + l) * (2 ^ l * m + 2 ^ k * n).
rewrite the current goal using mul_SNo_eps_eps_add_SNo k Hk l Hl (from right to left).
We will prove x + y = (eps_ k * eps_ l) * (2 ^ l * m + 2 ^ k * n).
rewrite the current goal using mul_SNo_distrL (eps_ k * eps_ l) (2 ^ l * m) (2 ^ k * n) (SNo_mul_SNo (eps_ k) (eps_ l) Lek Lel) (int_SNo (2 ^ l * m) L2lm) (int_SNo (2 ^ k * n) L2kn) (from left to right).
We will prove x + y = (eps_ k * eps_ l) * 2 ^ l * m + (eps_ k * eps_ l) * 2 ^ k * n.
Use f_equal.
We will prove x = (eps_ k * eps_ l) * 2 ^ l * m.
rewrite the current goal using mul_SNo_assoc (eps_ k) (eps_ l) (2 ^ l * m) Lek Lel (int_SNo (2 ^ l * m) L2lm) (from right to left).
We will prove x = eps_ k * eps_ l * 2 ^ l * m.
rewrite the current goal using mul_SNo_assoc (eps_ l) (2 ^ l) m Lel (int_SNo (2 ^ l) L2l) (int_SNo m Hm) (from left to right).
We will prove x = eps_ k * (eps_ l * 2 ^ l) * m.
rewrite the current goal using mul_SNo_eps_power_2 l (omega_nat_p l Hl) (from left to right).
We will prove x = eps_ k * 1 * m.
rewrite the current goal using mul_SNo_oneL m (int_SNo m Hm) (from left to right).
We will prove x = eps_ k * m.
An exact proof term for the current goal is Hxkm.
We will prove y = (eps_ k * eps_ l) * (2 ^ k * n).
rewrite the current goal using mul_SNo_com_4_inner_mid (eps_ k) (eps_ l) (2 ^ k) n Lek Lel (int_SNo (2 ^ k) L2k) (int_SNo n Hn) (from left to right).
We will prove y = (eps_ k * 2 ^ k) * (eps_ l * n).
rewrite the current goal using mul_SNo_eps_power_2 k (omega_nat_p k Hk) (from left to right).
We will prove y = 1 * (eps_ l * n).
rewrite the current goal using mul_SNo_oneL (eps_ l * n) Leln (from left to right).
An exact proof term for the current goal is Hyln.
∎
Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Subgoal 7 Subgoal 8 Subgoal 9 Subgoal 10 Main Goal
Theorem. (SNoS_omega_diadic_rational_p_lem) The following is provable:
∀n, nat_p n → ∀x, SNo x → SNoLev x = n → diadic_rational_p x
Proof:
Apply nat_complete_ind to the current goal.
Let n be given.
Assume Hn.
Assume IH: ∀m ∈ n, ∀x, SNo x → SNoLev x = m → diadic_rational_p x.
Let x be given.
Assume Hx: SNo x.
Assume Hxn: SNoLev x = n.
We will prove diadic_rational_p x.
Apply dneg to the current goal.
Assume HC: ¬ diadic_rational_p x.
We will prove False.
We prove the intermediate claim LxSo: x ∈ SNoS_ ω.
Apply SNoS_I ω omega_ordinal x (SNoLev x) to the current goal.
We will prove SNoLev x ∈ ω.
rewrite the current goal using Hxn (from left to right).
An exact proof term for the current goal is nat_p_omega n Hn.
We will prove SNo_ (SNoLev x) x.
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is Hx.
We prove the intermediate claim L1: ∃y, SNo_max_of (SNoL x) y.
Apply SNoS_omega_SNoL_max_exists x LxSo to the current goal.
Assume H1: SNoL x = 0.
We prove the intermediate claim L1a: ordinal (- x).
Apply SNo_max_ordinal (- x) (SNo_minus_SNo x Hx) to the current goal.
Let w be given.
rewrite the current goal using minus_SNo_Lev x Hx (from left to right).
Assume Hw: w ∈ SNoS_ (SNoLev x).
We will prove w < - x.
Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x Hx) w Hw to the current goal.
Assume Hw1 Hw2 Hw3 Hw4.
Apply SNoLt_trichotomy_or_impred w (- x) ?? (SNo_minus_SNo x Hx) to the current goal.
Assume H2: w < - x.
An exact proof term for the current goal is H2.
Assume H2: w = - x.
We will prove False.
Apply In_irref (SNoLev w) to the current goal.
rewrite the current goal using H2 (from left to right) at position 2.
rewrite the current goal using minus_SNo_Lev x Hx (from left to right).
An exact proof term for the current goal is ??.
Assume H2: - x < w.
We will prove False.
Apply EmptyE (- w) to the current goal.
We will prove - w ∈ 0.
rewrite the current goal using H1 (from right to left).
We will prove - w ∈ SNoL x.
Apply SNoL_I x Hx (- w) (SNo_minus_SNo w ??) to the current goal.
We will prove SNoLev (- w) ∈ SNoLev x.
rewrite the current goal using minus_SNo_Lev w ?? (from left to right).
An exact proof term for the current goal is ??.
We will prove - w < x.
An exact proof term for the current goal is minus_SNo_Lt_contra1 x w Hx ?? ??.
We prove the intermediate claim L1b: - x = n.
rewrite the current goal using Hxn (from right to left).
We will prove - x = SNoLev x.
Use symmetry.
rewrite the current goal using minus_SNo_Lev x ?? (from right to left).
An exact proof term for the current goal is ordinal_SNoLev (- x) L1a.
We will prove False.
Apply HC to the current goal.
We will prove diadic_rational_p x.
rewrite the current goal using minus_SNo_invol x ?? (from right to left).
We will prove diadic_rational_p (- - x).
Apply minus_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p (- x).
rewrite the current goal using L1b (from left to right).
We will prove diadic_rational_p n.
Apply omega_diadic_rational_p to the current goal.
An exact proof term for the current goal is nat_p_omega n Hn.
Assume H1.
An exact proof term for the current goal is H1.
We prove the intermediate claim L2: ∃z, SNo_min_of (SNoR x) z.
Apply SNoS_omega_SNoR_min_exists x LxSo to the current goal.
Assume H1: SNoR x = 0.
We prove the intermediate claim L2a: ordinal x.
Apply SNo_max_ordinal x Hx to the current goal.
Let w be given.
Assume Hw: w ∈ SNoS_ (SNoLev x).
We will prove w < x.
Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x ??) w Hw to the current goal.
Assume Hw1 Hw2 Hw3 Hw4.
Apply SNoLt_trichotomy_or_impred w x ?? ?? to the current goal.
Assume H2: w < x.
An exact proof term for the current goal is H2.
Assume H2: w = x.
We will prove False.
Apply In_irref (SNoLev x) to the current goal.
rewrite the current goal using H2 (from right to left) at position 1.
An exact proof term for the current goal is ??.
Assume H2: x < w.
We will prove False.
Apply EmptyE w to the current goal.
We will prove w ∈ 0.
rewrite the current goal using H1 (from right to left).
We will prove w ∈ SNoR x.
Apply SNoR_I x ?? w ?? ?? ?? to the current goal.
We prove the intermediate claim L2b: x = n.
rewrite the current goal using Hxn (from right to left).
We will prove x = SNoLev x.
Use symmetry.
An exact proof term for the current goal is ordinal_SNoLev x L2a.
We will prove False.
Apply HC to the current goal.
We will prove diadic_rational_p x.
Apply omega_diadic_rational_p to the current goal.
We will prove x ∈ ω.
rewrite the current goal using L2b (from left to right).
An exact proof term for the current goal is nat_p_omega n Hn.
Assume H1.
An exact proof term for the current goal is H1.
Apply L1 to the current goal.
Let y be given.
Assume Hy: SNo_max_of (SNoL x) y.
Apply Hy to the current goal.
Assume H.
Apply H to the current goal.
Assume Hy1: y ∈ SNoL x.
Assume Hy2: SNo y.
Assume Hy3: ∀w ∈ SNoL x, SNo w → w ≤ y.
Apply SNoL_E x Hx y Hy1 to the current goal.
Assume _ Hy1b Hy1c.
Apply L2 to the current goal.
Let z be given.
Assume Hz: SNo_min_of (SNoR x) z.
Apply Hz to the current goal.
Assume H.
Apply H to the current goal.
Assume Hz1: z ∈ SNoR x.
Assume Hz2: SNo z.
Assume Hz3: ∀w ∈ SNoR x, SNo w → z ≤ w.
Apply SNoR_E x Hx z Hz1 to the current goal.
Assume _ Hz1b Hz1c.
We prove the intermediate claim Lxx: SNo (x + x).
An exact proof term for the current goal is SNo_add_SNo x x Hx Hx.
We prove the intermediate claim Lyz: SNo (y + z).
An exact proof term for the current goal is SNo_add_SNo y z Hy2 Hz2.
We prove the intermediate claim Ldry: diadic_rational_p y.
Apply IH (SNoLev y) to the current goal.
We will prove SNoLev y ∈ n.
rewrite the current goal using Hxn (from right to left).
We will prove SNoLev y ∈ SNoLev x.
An exact proof term for the current goal is Hy1b.
We will prove SNo y.
An exact proof term for the current goal is Hy2.
We will prove SNoLev y = SNoLev y.
Use reflexivity.
We prove the intermediate claim Ldrz: diadic_rational_p z.
Apply IH (SNoLev z) to the current goal.
We will prove SNoLev z ∈ n.
rewrite the current goal using Hxn (from right to left).
We will prove SNoLev z ∈ SNoLev x.
An exact proof term for the current goal is Hz1b.
We will prove SNo z.
An exact proof term for the current goal is Hz2.
We will prove SNoLev z = SNoLev z.
Use reflexivity.
Apply SNoLt_trichotomy_or_impred (x + x) (y + z) Lxx Lyz to the current goal.
rewrite the current goal using add_SNo_com y z Hy2 Hz2 (from left to right).
Assume H1: x + x < z + y.
Apply double_SNo_min_1 x z Hx Hz y Hy2 Hy1c H1 to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoL y.
Assume H2: z + w = x + x.
Apply SNoL_E y Hy2 w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Ldrw: diadic_rational_p w.
Apply IH (SNoLev w) to the current goal.
We will prove SNoLev w ∈ n.
Apply ordinal_TransSet n (nat_p_ordinal n Hn) (SNoLev y) to the current goal.
We will prove SNoLev y ∈ n.
rewrite the current goal using Hxn (from right to left).
An exact proof term for the current goal is Hy1b.
We will prove SNoLev w ∈ SNoLev y.
An exact proof term for the current goal is Hw2.
We will prove SNo w.
An exact proof term for the current goal is Hw1.
We will prove SNoLev w = SNoLev w.
Use reflexivity.
We prove the intermediate claim Lxe: x = eps_ 1 * (z + w).
Apply double_eps_1 x z w Hx Hz2 Hw1 to the current goal.
Use symmetry.
An exact proof term for the current goal is H2.
Apply HC to the current goal.
We will prove diadic_rational_p x.
rewrite the current goal using Lxe (from left to right).
Apply mul_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p (eps_ 1).
An exact proof term for the current goal is eps_diadic_rational_p 1 (nat_p_omega 1 nat_1).
We will prove diadic_rational_p (z + w).
Apply add_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p z.
An exact proof term for the current goal is Ldrz.
We will prove diadic_rational_p w.
An exact proof term for the current goal is Ldrw.
Assume H1: x + x = y + z.
We prove the intermediate claim Lxe: x = eps_ 1 * (y + z).
An exact proof term for the current goal is double_eps_1 x y z Hx Hy2 Hz2 H1.
Apply HC to the current goal.
We will prove diadic_rational_p x.
rewrite the current goal using Lxe (from left to right).
Apply mul_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p (eps_ 1).
An exact proof term for the current goal is eps_diadic_rational_p 1 (nat_p_omega 1 nat_1).
We will prove diadic_rational_p (y + z).
Apply add_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p y.
An exact proof term for the current goal is Ldry.
We will prove diadic_rational_p z.
An exact proof term for the current goal is Ldrz.
Assume H1: y + z < x + x.
Apply double_SNo_max_1 x y Hx Hy z Hz2 Hz1c H1 to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR z.
Assume H2: y + w = x + x.
Apply SNoR_E z Hz2 w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Ldrw: diadic_rational_p w.
Apply IH (SNoLev w) to the current goal.
We will prove SNoLev w ∈ n.
Apply ordinal_TransSet n (nat_p_ordinal n Hn) (SNoLev z) to the current goal.
We will prove SNoLev z ∈ n.
rewrite the current goal using Hxn (from right to left).
An exact proof term for the current goal is Hz1b.
We will prove SNoLev w ∈ SNoLev z.
An exact proof term for the current goal is Hw2.
We will prove SNo w.
An exact proof term for the current goal is Hw1.
We will prove SNoLev w = SNoLev w.
Use reflexivity.
We prove the intermediate claim Lxe: x = eps_ 1 * (y + w).
Apply double_eps_1 x y w Hx Hy2 Hw1 to the current goal.
Use symmetry.
An exact proof term for the current goal is H2.
Apply HC to the current goal.
We will prove diadic_rational_p x.
rewrite the current goal using Lxe (from left to right).
Apply mul_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p (eps_ 1).
An exact proof term for the current goal is eps_diadic_rational_p 1 (nat_p_omega 1 nat_1).
We will prove diadic_rational_p (y + w).
Apply add_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p y.
An exact proof term for the current goal is Ldry.
We will prove diadic_rational_p w.
An exact proof term for the current goal is Ldrw.
∎
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 Main Goal
Theorem. (SNoS_omega_diadic_rational_p) The following is provable:
∀x ∈ SNoS_ ω, diadic_rational_p x
Proof:
Let x be given.
Assume Hx: x ∈ SNoS_ ω.
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_omega_diadic_rational_p_lem (SNoLev x) to the current goal.
We will prove nat_p (SNoLev x).
An exact proof term for the current goal is omega_nat_p (SNoLev x) Hx1.
We will prove SNo x.
An exact proof term for the current goal is Hx3.
We will prove SNoLev x = SNoLev x.
Use reflexivity.
∎
Try to prove it yourself. Main Goal
Theorem. (mul_SNo_SNoS_omega) The following is provable:
∀x y ∈ SNoS_ ω, x * y ∈ SNoS_ ω
Proof:
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Apply diadic_rational_p_SNoS_omega to the current goal.
Apply mul_SNo_diadic_rational_p to the current goal.
Apply SNoS_omega_diadic_rational_p to the current goal.
An exact proof term for the current goal is Hx.
Apply SNoS_omega_diadic_rational_p to the current goal.
An exact proof term for the current goal is Hy.
∎
Try to prove it yourself. Main Goal
End of Section DiadicRationals