12 of 100 Theorems Formalized in Megalodon

Introduction

Below is an html presentation of a formal development in Megalodon (1.12 or later) that includes proofs of 12 of the 100 theorems from the Formalizing 100 Theorems webpage. The foundation is higher-order Tarski-Grothendieck set theory, so the first part of the development is listing the primitives and axioms. After that the first 10 theorems lead up to a proof of excluded middle, so that we can freely use classical logic.

After some basic infrastructure the natural numbers are defined as finite ordinals. This is enough to prove the first of the 100 theorems:

74. The Principle of Mathematical Induction nat_ind and nat_complete_ind

The next 4 of the 100 theorems require injections, bijections, atleastp (when a set has at least the cardinality of another) and equipotence (when a set has the same cardinality as another). We also need the notions of finite (equipotent to a natural number) and infinite (not finite). In addition, we use an axiom of infinity (for the only time in the development) to define a set ω of natural numbers, which in turn allows us to define the set of prime numbers.

63. Cantor's Theorem form100_63_injCantor
25. Schroeder-Bernstein Theorem SchroederBernstein
52. The Number of Subsets of a Set equip_finite_Power
11. The Infinitude of Primes form100_11_infinite_primes
31. Ramsey's Theorem infiniteRamsey

The next 3 of the 100 theorems require integers. Instead of simply defining integers, we construct Conway's surreal numbers as ordinal length sequences indicating left and right moves. We construct the linear order of these numbers and define basic operations: (unary) minus, addition and multiplication. Ordinals are nonnegative and are surreal numbers always moving to the right. The nonpositive counterpart of ordinals are surreal numbers always moving to the left. Zero, as the only zero-length sequence, is both nonnegative and nonpositive. The set of integers is the set of finite ordinals closed under minus. The integers are closed under surreal addition and surreal multiplication.

60. Bezout's Theorem BezoutThm
69. Greatest Common Divisor Algorithm euclidean_algorithm
80. The Fundamental Theorem of Arithmetic prime_factorization_ex_uniq

The next two results require the reals and the rationals. We define division on the surreals and carve the set of reals from the surreal numbers. The rational numbers are then simply the reals that can be expressed as an integer divided by a nonnegative natural number.

22. The Non-Denumerability of the Continuum form100_22_real_uncountable_equip
3. The Denumerability of the Rational Numbers form100_3

The final of the 12 of the 100 theorems requires square roots. We define square roots for nonnegative surreal numbers and prove the square root of a nonnegative real is real. We then prove the square root of 2 is irrational (i.e., in the set of reals, but not in the set of rationals).

1. The Irrationality of the Square Root of 2 sqrt_2_irrational

Primitives and Axioms

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

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

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

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

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

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

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

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.

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

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

¬ ∃x : set, x ∈ Empty

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

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

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

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

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

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

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

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

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

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

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.

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

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

∀N : set, N ∈ UnivOf N

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

First Theorems Up To Excluded Middle

Theorem. (andI)

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

Click to Load Proof

Theorem. (orIL)

∀A B : prop, A → A ∨ B

Click to Load Proof

Theorem. (orIR)

∀A B : prop, B → A ∨ B

Click to Load Proof

Theorem. (iffI)

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

Click to Load Proof

Theorem. (pred_ext)

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

Click to Load Proof

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

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

Theorem. (EmptyE)

∀x : set, x ∉ Empty

Click to Load Proof

Theorem. (PowerI)

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

Click to Load Proof

Theorem. (Subq_Empty)

∀X : set, Empty ⊆ X

Click to Load Proof

Theorem. (Empty_In_Power)

∀X : set, Empty ∈ 𝒫 X

Click to Load Proof

Theorem. (xm)

∀P : prop, P ∨ ¬ P

Click to Load Proof

The Rest of the Development

Theorem. (FalseE)

False → ∀p : prop, p

Click to Load Proof

Theorem. (andEL)

∀A B : prop, A ∧ B → A

Click to Load Proof

Theorem. (andER)

∀A B : prop, A ∧ B → B

Click to Load Proof

Beginning of Section PropN

Variable P1 P2 P3 : prop

Theorem. (and3I)

P1 → P2 → P3 → P1 ∧ P2 ∧ P3

Click to Load Proof

Theorem. (and3E)

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

Click to Load Proof

Theorem. (or3I1)

P1 → P1 ∨ P2 ∨ P3

Click to Load Proof

Theorem. (or3I2)

P2 → P1 ∨ P2 ∨ P3

Click to Load Proof

Theorem. (or3I3)

P3 → P1 ∨ P2 ∨ P3

Click to Load Proof

Theorem. (or3E)

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

Click to Load Proof

Variable P4 : prop

Theorem. (and4I)

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

Click to Load Proof

Variable P5 : prop

Theorem. (and5I)

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

Click to Load Proof

Variable P6 : prop

Theorem. (and6I)

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

Click to Load Proof

Variable P7 : prop

Theorem. (and7I)

P1 → P2 → P3 → P4 → P5 → P6 → P7 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7

Click to Load Proof

End of Section PropN

Theorem. (not_or_and_demorgan)

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

Click to Load Proof

Theorem. (not_ex_all_demorgan_i)

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

Click to Load Proof

Theorem. (iffEL)

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

Click to Load Proof

Theorem. (iffER)

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

Click to Load Proof

Theorem. (iff_refl)

∀A : prop, A ↔ A

Click to Load Proof

Theorem. (iff_sym)

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

Click to Load Proof

Theorem. (iff_trans)

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

Click to Load Proof

Theorem. (eq_i_tra)

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

Click to Load Proof

Theorem. (neq_i_sym)

∀x y, x ≠ y → y ≠ x

Click to Load Proof

Theorem. (Eps_i_ex)

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

Click to Load Proof

Theorem. (prop_ext_2)

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

Click to Load Proof

Theorem. (Subq_ref)

∀X : set, X ⊆ X

Click to Load Proof

Theorem. (Subq_tra)

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

Click to Load Proof

Theorem. (Empty_Subq_eq)

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

Click to Load Proof

Theorem. (Empty_eq)

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

Click to Load Proof

Theorem. (UnionI)

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

Click to Load Proof

Theorem. (UnionE)

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

Click to Load Proof

Theorem. (UnionE_impred)

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

Click to Load Proof

Theorem. (PowerE)

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

Click to Load Proof

Theorem. (Self_In_Power)

∀X : set, X ∈ 𝒫 X

Click to Load Proof

Theorem. (dneg)

∀P : prop, ¬ ¬ P → P

Click to Load Proof

Theorem. (not_all_ex_demorgan_i)

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

Click to Load Proof

Theorem. (eq_or_nand)

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

Click to Load Proof

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

Theorem. (exactly1of2_I1)

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

Click to Load Proof

Theorem. (exactly1of2_I2)

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

Click to Load Proof

Theorem. (exactly1of2_E)

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

Click to Load Proof

Theorem. (exactly1of2_or)

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

Click to Load Proof

Theorem. (ReplI)

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

Click to Load Proof

Theorem. (ReplE)

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

Click to Load Proof

Theorem. (ReplE_impred)

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

Click to Load Proof

Theorem. (ReplE')

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

Click to Load Proof

Theorem. (Repl_Empty)

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

Click to Load Proof

Theorem. (ReplEq_ext_sub)

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

Click to Load Proof

Theorem. (ReplEq_ext)

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

Click to Load Proof

Theorem. (Repl_inv_eq)

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

Click to Load Proof

Theorem. (Repl_invol_eq)

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

Click to Load Proof

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

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

Theorem. (If_i_correct)

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

Click to Load Proof

Theorem. (If_i_0)

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

Click to Load Proof

Theorem. (If_i_1)

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

Click to Load Proof

Theorem. (If_i_or)

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

Click to Load Proof

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

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

Theorem. (UPairE)

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

Click to Load Proof

Theorem. (UPairI1)

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

Click to Load Proof

Theorem. (UPairI2)

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

Click to Load Proof

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

Notation. {x} is notation for Sing x.

Theorem. (SingI)

∀x : set, x ∈ {x}

Click to Load Proof

Theorem. (SingE)

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

Click to Load Proof

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

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

Theorem. (binunionI1)

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

Click to Load Proof

Theorem. (binunionI2)

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

Click to Load Proof

Theorem. (binunionE)

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

Click to Load Proof

Theorem. (binunionE')

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

Click to Load Proof

Theorem. (binunion_asso)

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

Click to Load Proof

Theorem. (binunion_com_Subq)

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

Click to Load Proof

Theorem. (binunion_com)

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

Click to Load Proof

Theorem. (binunion_idl)

∀X : set, Empty ∪ X = X

Click to Load Proof

Theorem. (binunion_idr)

∀X : set, X ∪ Empty = X

Click to Load Proof

Theorem. (binunion_Subq_1)

∀X Y : set, X ⊆ X ∪ Y

Click to Load Proof

Theorem. (binunion_Subq_2)

∀X Y : set, Y ⊆ X ∪ Y

Click to Load Proof

Theorem. (binunion_Subq_min)

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

Click to Load Proof

Theorem. (Subq_binunion_eq)

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

Click to Load Proof

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

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

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

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

Theorem. (famunionI)

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

Click to Load Proof

Theorem. (famunionE)

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

Click to Load Proof

Theorem. (famunionE_impred)

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

Click to Load Proof

Theorem. (famunion_Empty)

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

Click to Load Proof

Theorem. (famunion_Subq)

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

Click to Load Proof

Theorem. (famunion_ext)

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

Click to Load Proof

Beginning of Section SepSec

Variable X : set

Variable P : set → prop

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

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

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

End of Section SepSec

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

Theorem. (SepI)

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

Click to Load Proof

Theorem. (SepE)

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

Click to Load Proof

Theorem. (SepE1)

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

Click to Load Proof

Theorem. (SepE2)

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

Click to Load Proof

Theorem. (Sep_Empty)

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

Click to Load Proof

Theorem. (Sep_Subq)

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

Click to Load Proof

Theorem. (Sep_In_Power)

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

Click to Load Proof

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

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

Theorem. (ReplSepI)

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

Click to Load Proof

Theorem. (ReplSepE)

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

Click to Load Proof

Theorem. (ReplSepE_impred)

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

Click to Load Proof

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

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

Theorem. (binintersectI)

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

Click to Load Proof

Theorem. (binintersectE)

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

Click to Load Proof

Theorem. (binintersectE1)

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

Click to Load Proof

Theorem. (binintersectE2)

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

Click to Load Proof

Theorem. (binintersect_Subq_1)

∀X Y : set, X ∩ Y ⊆ X

Click to Load Proof

Theorem. (binintersect_Subq_2)

∀X Y : set, X ∩ Y ⊆ Y

Click to Load Proof

Theorem. (binintersect_Subq_eq_1)

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

Click to Load Proof

Theorem. (binintersect_Subq_max)

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

Click to Load Proof

Theorem. (binintersect_com_Subq)

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

Click to Load Proof

Theorem. (binintersect_com)

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

Click to Load Proof

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

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

Theorem. (setminusI)

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

Click to Load Proof

Theorem. (setminusE)

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

Click to Load Proof

Theorem. (setminusE1)

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

Click to Load Proof

Theorem. (setminusE2)

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

Click to Load Proof

Theorem. (setminus_Subq)

∀X Y : set, X ∖ Y ⊆ X

Click to Load Proof

Theorem. (setminus_In_Power)

∀A U, A ∖ U ∈ 𝒫 A

Click to Load Proof

Theorem. (binunion_remove1_eq)

∀X, ∀x ∈ X, X = (X ∖ {x}) ∪ {x}

Click to Load Proof

Theorem. (In_irref)

∀x, x ∉ x

Click to Load Proof

Theorem. (In_no2cycle)

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

Click to Load Proof

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

Theorem. (ordsuccI1)

∀x : set, x ⊆ ordsucc x

Click to Load Proof

Theorem. (ordsuccI2)

∀x : set, x ∈ ordsucc x

Click to Load Proof

Theorem. (ordsuccE)

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

Click to Load Proof

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

Theorem. (neq_0_ordsucc)

∀a : set, 0 ≠ ordsucc a

Click to Load Proof

Theorem. (neq_ordsucc_0)

∀a : set, ordsucc a ≠ 0

Click to Load Proof

Theorem. (ordsucc_inj)

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

Click to Load Proof

Theorem. (In_0_1)

0 ∈ 1

Click to Load Proof

Theorem. (In_0_2)

0 ∈ 2

Click to Load Proof

Theorem. (In_1_2)

1 ∈ 2

Click to Load Proof

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

Theorem. (nat_0)

nat_p 0

Click to Load Proof

Theorem. (nat_ordsucc)

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

Click to Load Proof

Theorem. (nat_1)

nat_p 1

Click to Load Proof

Theorem. (nat_2)

nat_p 2

Click to Load Proof

Theorem. (nat_0_in_ordsucc)

∀n, nat_p n → 0 ∈ ordsucc n

Click to Load Proof

Theorem. (nat_ordsucc_in_ordsucc)

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

Click to Load Proof

Theorem. (nat_ind)

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

Click to Load Proof

Theorem. (nat_complete_ind)

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

Click to Load Proof

Theorem. (nat_inv_impred)

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

Click to Load Proof

Theorem. (nat_inv)

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

Click to Load Proof

Theorem. (nat_p_trans)

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

Click to Load Proof

Theorem. (nat_trans)

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

Click to Load Proof

Theorem. (nat_ordsucc_trans)

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

Click to Load Proof

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

Theorem. (form100_63_surjCantor)

∀A : set, ∀f : set → set, ¬ surj A (𝒫 A) f

Click to Load Proof

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.

Theorem. (form100_63_injCantor)

∀A : set, ∀f : set → set, ¬ inj (𝒫 A) A f

Click to Load Proof

Theorem. (injI)

∀X Y, ∀f : set → set, (∀x ∈ X, f x ∈ Y) → (∀x z ∈ X, f x = f z → x = z) → inj X Y f

Click to Load Proof

Theorem. (inj_comp)

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

Click to Load Proof

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

Theorem. (bijI)

∀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

Click to Load Proof

Theorem. (bijE)

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

Click to Load Proof

Theorem. (bij_inj)

∀X Y, ∀f : set → set, bij X Y f → inj X Y f

Click to Load Proof

Theorem. (bij_id)

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

Click to Load Proof

Theorem. (bij_comp)

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

Click to Load Proof

Theorem. (bij_surj)

∀X Y, ∀f : set → set, bij X Y f → surj X Y f

Click to Load Proof

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

Theorem. (surj_rinv)

∀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

Click to Load Proof

Theorem. (inj_linv)

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

Click to Load Proof

Theorem. (bij_inv)

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

Click to Load Proof

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

Theorem. (atleastp_tra)

∀X Y Z, atleastp X Y → atleastp Y Z → atleastp X Z

Click to Load Proof

Theorem. (Subq_atleastp)

∀X Y, X ⊆ Y → atleastp X Y

Click to Load Proof

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

Theorem. (equip_atleastp)

∀X Y, equip X Y → atleastp X Y

Click to Load Proof

Theorem. (equip_ref)

∀X, equip X X

Click to Load Proof

Theorem. (equip_sym)

∀X Y, equip X Y → equip Y X

Click to Load Proof

Theorem. (equip_tra)

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

Click to Load Proof

Theorem. (equip_0_Empty)

∀X, equip X 0 → X = 0

Click to Load Proof

Theorem. (equip_adjoin_ordsucc)

∀N X y, y ∉ X → equip N X → equip (ordsucc N) (X ∪ {y})

Click to Load Proof

Theorem. (equip_ordsucc_remove1)

∀X N, ∀x ∈ X, equip X (ordsucc N) → equip (X ∖ {x}) N

Click to Load Proof

Beginning of Section SchroederBernstein

Theorem. (KnasterTarski_set)

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

Click to Load Proof

Theorem. (image_In_Power)

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

Click to Load Proof

Theorem. (image_monotone)

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

Click to Load Proof

Theorem. (setminus_antimonotone)

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

Click to Load Proof

Theorem. (SchroederBernstein)

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

Click to Load Proof

Theorem. (atleastp_antisym_equip)

∀A B, atleastp A B → atleastp B A → equip A B

Click to Load Proof

End of Section SchroederBernstein

Beginning of Section PigeonHole

Theorem. (PigeonHole_nat)

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

Click to Load Proof

Theorem. (Pigeonhole_not_atleastp_ordsucc)

∀n, nat_p n → ¬ atleastp (ordsucc n) n

Click to Load Proof

End of Section PigeonHole

Theorem. (Union_ordsucc_eq)

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

Click to Load Proof

Theorem. (cases_1)

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

Click to Load Proof

Theorem. (cases_2)

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

Click to Load Proof

Theorem. (neq_0_1)

0 ≠ 1

Click to Load Proof

Theorem. (neq_1_0)

1 ≠ 0

Click to Load Proof

Theorem. (neq_0_2)

0 ≠ 2

Click to Load Proof

Theorem. (neq_2_0)

2 ≠ 0

Click to Load Proof

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

Theorem. (ordinal_TransSet)

∀α : set, ordinal α → TransSet α

Click to Load Proof

Theorem. (ordinal_Empty)

ordinal Empty

Click to Load Proof

Theorem. (ordinal_Hered)

∀α : set, ordinal α → ∀β ∈ α, ordinal β

Click to Load Proof

Theorem. (TransSet_ordsucc)

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

Click to Load Proof

Theorem. (ordinal_ordsucc)

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

Click to Load Proof

Theorem. (nat_p_ordinal)

∀n : set, nat_p n → ordinal n

Click to Load Proof

Theorem. (ordinal_1)

ordinal 1

Click to Load Proof

Theorem. (ordinal_2)

ordinal 2

Click to Load Proof

Theorem. (TransSet_ordsucc_In_Subq)

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

Click to Load Proof

Theorem. (ordinal_ordsucc_In_Subq)

∀α, ordinal α → ∀β ∈ α, ordsucc β ⊆ α

Click to Load Proof

Theorem. (ordinal_trichotomy_or)

∀α β : set, ordinal α → ordinal β → α ∈ β ∨ α = β ∨ β ∈ α

Click to Load Proof

Theorem. (ordinal_trichotomy_or_impred)

∀α β : set, ordinal α → ordinal β → ∀p : prop, (α ∈ β → p) → (α = β → p) → (β ∈ α → p) → p

Click to Load Proof

Theorem. (ordinal_In_Or_Subq)

∀α β, ordinal α → ordinal β → α ∈ β ∨ β ⊆ α

Click to Load Proof

Theorem. (ordinal_linear)

∀α β, ordinal α → ordinal β → α ⊆ β ∨ β ⊆ α

Click to Load Proof

Theorem. (ordinal_ordsucc_In_eq)

∀α β, ordinal α → β ∈ α → ordsucc β ∈ α ∨ α = ordsucc β

Click to Load Proof

Theorem. (ordinal_lim_or_succ)

∀α, ordinal α → (∀β ∈ α, ordsucc β ∈ α) ∨ (∃β ∈ α, α = ordsucc β)

Click to Load Proof

Theorem. (ordinal_ordsucc_In)

∀α, ordinal α → ∀β ∈ α, ordsucc β ∈ ordsucc α

Click to Load Proof

Theorem. (ordinal_famunion)

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

Click to Load Proof

Theorem. (ordinal_binintersect)

∀α β, ordinal α → ordinal β → ordinal (α ∩ β)

Click to Load Proof

Theorem. (ordinal_binunion)

∀α β, ordinal α → ordinal β → ordinal (α ∪ β)

Click to Load Proof

Theorem. (ordinal_ind)

∀p : set → prop, (∀α, ordinal α → (∀β ∈ α, p β) → p α) → ∀α, ordinal α → p α

Click to Load Proof

Theorem. (least_ordinal_ex)

∀p : set → prop, (∃α, ordinal α ∧ p α) → ∃α, ordinal α ∧ p α ∧ ∀β ∈ α, ¬ p β

Click to Load Proof

Theorem. (equip_Sing_1)

∀x, equip {x} 1

Click to Load Proof

Theorem. (TransSet_In_ordsucc_Subq)

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

Click to Load Proof

Theorem. (exandE_i)

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

Click to Load Proof

Theorem. (exandE_ii)

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

Click to Load Proof

Theorem. (exandE_iii)

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

Click to Load Proof

Theorem. (exandE_iiii)

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

Click to Load Proof

Beginning of Section Descr_ii

Variable P : (set → set) → prop

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

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

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

Theorem. (Descr_ii_prop)

P Descr_ii

Click to Load Proof

End of Section Descr_ii

Beginning of Section Descr_iii

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

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

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

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

Theorem. (Descr_iii_prop)

P Descr_iii

Click to Load Proof

End of Section Descr_iii

Beginning of Section Descr_Vo1

Variable P : Vo 1 → prop

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

Hypothesis Pex : ∃f : Vo 1, P f

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

Theorem. (Descr_Vo1_prop)

P Descr_Vo1

Click to Load Proof

End of Section Descr_Vo1

Beginning of Section If_ii

Variable p : prop

Variable f g : set → set

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

Theorem. (If_ii_1)

p → If_ii = f

Click to Load Proof

Theorem. (If_ii_0)

¬ p → If_ii = g

Click to Load Proof

End of Section If_ii

Beginning of Section If_iii

Variable p : prop

Variable f g : set → set → set

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

Theorem. (If_iii_1)

p → If_iii = f

Click to Load Proof

Theorem. (If_iii_0)

¬ p → If_iii = g

Click to Load Proof

End of Section If_iii

Beginning of Section EpsilonRec_i

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

Definition. We define In_rec_i_G to be λX Y ⇒ ∀R : set → set → prop, (∀X : set, ∀f : set → set, (∀x ∈ X, R x (f x)) → R X (F X f)) → R X Y of type set → set → prop.

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

Theorem. (In_rec_i_G_c)

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

Click to Load Proof

Theorem. (In_rec_i_G_inv)

∀X : set, ∀Y : set, In_rec_i_G X Y → ∃f : set → set, (∀x ∈ X, In_rec_i_G x (f x)) ∧ Y = F X f

Click to Load Proof

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

Theorem. (In_rec_i_G_f)

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

Click to Load Proof

Theorem. (In_rec_i_G_In_rec_i)

∀X : set, In_rec_i_G X (In_rec_i X)

Click to Load Proof

Theorem. (In_rec_i_G_In_rec_i_d)

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

Click to Load Proof

Theorem. (In_rec_i_eq)

∀X : set, In_rec_i X = F X In_rec_i

Click to Load Proof

End of Section EpsilonRec_i

Beginning of Section EpsilonRec_ii

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

Definition. We define In_rec_G_ii to be λX Y ⇒ ∀R : set → (set → set) → prop, (∀X : set, ∀f : set → (set → set), (∀x ∈ X, R x (f x)) → R X (F X f)) → R X Y of type set → (set → set) → prop.

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

Theorem. (In_rec_G_ii_c)

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

Click to Load Proof

Theorem. (In_rec_G_ii_inv)

∀X : set, ∀Y : (set → set), In_rec_G_ii X Y → ∃f : set → (set → set), (∀x ∈ X, In_rec_G_ii x (f x)) ∧ Y = F X f

Click to Load Proof

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

Theorem. (In_rec_G_ii_f)

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

Click to Load Proof

Theorem. (In_rec_G_ii_In_rec_ii)

∀X : set, In_rec_G_ii X (In_rec_ii X)

Click to Load Proof

Theorem. (In_rec_G_ii_In_rec_ii_d)

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

Click to Load Proof

Theorem. (In_rec_ii_eq)

∀X : set, In_rec_ii X = F X In_rec_ii

Click to Load Proof

End of Section EpsilonRec_ii

Beginning of Section EpsilonRec_iii

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

Definition. We define In_rec_G_iii to be λX Y ⇒ ∀R : set → (set → set → set) → prop, (∀X : set, ∀f : set → (set → set → set), (∀x ∈ X, R x (f x)) → R X (F X f)) → R X Y of type set → (set → set → set) → prop.

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

Theorem. (In_rec_G_iii_c)

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

Click to Load Proof

Theorem. (In_rec_G_iii_inv)

∀X : set, ∀Y : (set → set → set), In_rec_G_iii X Y → ∃f : set → (set → set → set), (∀x ∈ X, In_rec_G_iii x (f x)) ∧ Y = F X f

Click to Load Proof

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

Theorem. (In_rec_G_iii_f)

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

Click to Load Proof

Theorem. (In_rec_G_iii_In_rec_iii)

∀X : set, In_rec_G_iii X (In_rec_iii X)

Click to Load Proof

Theorem. (In_rec_G_iii_In_rec_iii_d)

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

Click to Load Proof

Theorem. (In_rec_iii_eq)

∀X : set, In_rec_iii X = F X In_rec_iii

Click to Load Proof

End of Section EpsilonRec_iii

Beginning of Section NatRec

Variable z : set

Variable f : set → set → set

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

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

Theorem. (nat_primrec_r)

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

Click to Load Proof

Theorem. (nat_primrec_0)

nat_primrec 0 = z

Click to Load Proof

Theorem. (nat_primrec_S)

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

Click to Load Proof

End of Section NatRec

Beginning of Section NatAdd

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

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

Theorem. (add_nat_0R)

∀n : set, n + 0 = n

Click to Load Proof

Theorem. (add_nat_SR)

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

Click to Load Proof

Theorem. (add_nat_p)

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

Click to Load Proof

Theorem. (add_nat_1_1_2)

1 + 1 = 2

Click to Load Proof

Theorem. (add_nat_asso)

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

Click to Load Proof

Theorem. (add_nat_0L)

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

Click to Load Proof

Theorem. (add_nat_SL)

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

Click to Load Proof

Theorem. (add_nat_com)

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

Click to Load Proof

Theorem. (add_nat_In_R)

∀m, nat_p m → ∀k ∈ m, ∀n, nat_p n → k + n ∈ m + n

Click to Load Proof

Theorem. (add_nat_In_L)

∀n, nat_p n → ∀m, nat_p m → ∀k ∈ m, n + k ∈ n + m

Click to Load Proof

Theorem. (add_nat_Subq_R)

∀k, nat_p k → ∀m, nat_p m → k ⊆ m → ∀n, nat_p n → k + n ⊆ m + n

Click to Load Proof

Theorem. (add_nat_Subq_L)

∀n, nat_p n → ∀k, nat_p k → ∀m, nat_p m → k ⊆ m → n + k ⊆ n + m

Click to Load Proof

Theorem. (add_nat_Subq_R')

∀m, nat_p m → ∀n, nat_p n → m ⊆ m + n

Click to Load Proof

Theorem. (nat_Subq_add_ex)

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

Click to Load Proof

Theorem. (add_nat_cancel_R)

∀k, nat_p k → ∀m, nat_p m → ∀n, nat_p n → k + n = m + n → k = m

Click to Load Proof

End of Section NatAdd

Beginning of Section NatMul

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

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

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

Theorem. (mul_nat_0R)

∀n : set, n * 0 = 0

Click to Load Proof

Theorem. (mul_nat_SR)

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

Click to Load Proof

Theorem. (mul_nat_1R)

∀n, n * 1 = n

Click to Load Proof

Theorem. (mul_nat_p)

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

Click to Load Proof

Theorem. (mul_nat_0L)

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

Click to Load Proof

Theorem. (mul_nat_SL)

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

Click to Load Proof

Theorem. (mul_nat_com)

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

Click to Load Proof

Theorem. (mul_add_nat_distrL)

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

Click to Load Proof

Theorem. (mul_nat_asso)

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

Click to Load Proof

Theorem. (mul_nat_Subq_R)

∀m n, nat_p m → nat_p n → m ⊆ n → ∀k, nat_p k → m * k ⊆ n * k

Click to Load Proof

Theorem. (mul_nat_Subq_L)

∀m n, nat_p m → nat_p n → m ⊆ n → ∀k, nat_p k → k * m ⊆ k * n

Click to Load Proof

Theorem. (mul_nat_0_or_Subq)

∀m, nat_p m → ∀n, nat_p n → n = 0 ∨ m ⊆ m * n

Click to Load Proof

Theorem. (mul_nat_0_inv)

∀m, nat_p m → ∀n, nat_p n → m * n = 0 → m = 0 ∨ n = 0

Click to Load Proof

Theorem. (mul_nat_0m_1n_In)

∀m, nat_p m → ∀n, nat_p n → 0 ∈ m → 1 ∈ n → m ∈ m * n

Click to Load Proof

Theorem. (nat_le1_cases)

∀m, nat_p m → m ⊆ 1 → m = 0 ∨ m = 1

Click to Load Proof

Definition. We define Pi_nat to be λf n ⇒ nat_primrec 1 (λi r ⇒ r * f i) n of type (set → set) → set → set.

Theorem. (Pi_nat_0)

∀f : set → set, Pi_nat f 0 = 1

Click to Load Proof

Theorem. (Pi_nat_S)

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

Click to Load Proof

Theorem. (Pi_nat_p)

∀f : set → set, ∀n, nat_p n → (∀i ∈ n, nat_p (f i)) → nat_p (Pi_nat f n)

Click to Load Proof

Theorem. (Pi_nat_0_inv)

∀f : set → set, ∀n, nat_p n → (∀i ∈ n, nat_p (f i)) → Pi_nat f n = 0 → (∃i ∈ n, f i = 0)

Click to Load Proof

Definition. We define exp_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_nat.

Theorem. (exp_nat_0)

∀n, n ^ 0 = 1

Click to Load Proof

Theorem. (exp_nat_S)

∀n m, nat_p m → n ^ (ordsucc m) = n * n ^ m

Click to Load Proof

Theorem. (exp_nat_p)

∀n, nat_p n → ∀m, nat_p m → nat_p (n ^ m)

Click to Load Proof

Theorem. (exp_nat_1)

∀n, n ^ 1 = n

Click to Load Proof

End of Section NatMul

Beginning of Section form100_52

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

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

Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_nat.

Theorem. (Subq_Sing0_1)

{0} ⊆ 1

Click to Load Proof

Theorem. (Subq_1_Sing0)

1 ⊆ {0}

Click to Load Proof

Theorem. (eq_1_Sing0)

1 = {0}

Click to Load Proof

Theorem. (Power_0_Sing_0)

𝒫 0 = {0}

Click to Load Proof

Theorem. (equip_finite_Power)

∀n, nat_p n → ∀X, equip X n → equip (𝒫 X) (2 ^ n)

Click to Load Proof

End of Section form100_52

Theorem. (ZF_closed_E)

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

Click to Load Proof

Theorem. (ZF_Union_closed)

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

Click to Load Proof

Theorem. (ZF_Power_closed)

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

Click to Load Proof

Theorem. (ZF_Repl_closed)

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

Click to Load Proof

Theorem. (ZF_UPair_closed)

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

Click to Load Proof

Theorem. (ZF_Sing_closed)

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

Click to Load Proof

Theorem. (ZF_binunion_closed)

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

Click to Load Proof

Theorem. (ZF_ordsucc_closed)

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

Click to Load Proof

Theorem. (nat_p_UnivOf_Empty)

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

Click to Load Proof

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

Theorem. (omega_nat_p)

∀n ∈ ω, nat_p n

Click to Load Proof

Theorem. (nat_p_omega)

∀n : set, nat_p n → n ∈ ω

Click to Load Proof

Theorem. (omega_ordsucc)

∀n ∈ ω, ordsucc n ∈ ω

Click to Load Proof

Theorem. (form100_22_v2)

∀f : set → set, ¬ inj (𝒫 ω) ω f

Click to Load Proof

Theorem. (form100_22_v3)

∀g : set → set, ¬ surj ω (𝒫 ω) g

Click to Load Proof

Theorem. (form100_22_v1)

¬ equip ω (𝒫 ω)

Click to Load Proof

Theorem. (omega_TransSet)

TransSet ω

Click to Load Proof

Theorem. (omega_ordinal)

ordinal ω

Click to Load Proof

Theorem. (ordsucc_omega_ordinal)

ordinal (ordsucc ω)

Click to Load Proof

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

Theorem. (nat_finite)

∀n, nat_p n → finite n

Click to Load Proof

Theorem. (finite_ind)

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

Click to Load Proof

Theorem. (finite_Empty)

finite 0

Click to Load Proof

Theorem. (Sing_finite)

∀x, finite {x}

Click to Load Proof

Theorem. (adjoin_finite)

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

Click to Load Proof

Theorem. (binunion_finite)

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

Click to Load Proof

Theorem. (famunion_nat_finite)

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

Click to Load Proof

Theorem. (Subq_finite)

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

Click to Load Proof

Definition. We define infinite to be λA ⇒ ¬ finite A of type set → prop.

Beginning of Section InfinitePrimes

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

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

Definition. We define divides_nat to be λm n ⇒ m ∈ ω ∧ n ∈ ω ∧ ∃k ∈ ω, m * k = n of type set → set → prop.

Theorem. (divides_nat_ref)

∀n, nat_p n → divides_nat n n

Click to Load Proof

Theorem. (divides_nat_tra)

∀k m n, divides_nat k m → divides_nat m n → divides_nat k n

Click to Load Proof

Definition. We define prime_nat to be λn ⇒ n ∈ ω ∧ 1 ∈ n ∧ ∀k ∈ ω, divides_nat k n → k = 1 ∨ k = n of type set → prop.

Theorem. (divides_nat_mulR)

∀m n ∈ ω, divides_nat m (m * n)

Click to Load Proof

Theorem. (divides_nat_mulL)

∀m n ∈ ω, divides_nat n (m * n)

Click to Load Proof

Theorem. (Pi_nat_divides)

∀f : set → set, ∀n, nat_p n → (∀i ∈ n, nat_p (f i)) → (∀i ∈ n, divides_nat (f i) (Pi_nat f n))

Click to Load Proof

Definition. We define composite_nat to be λn ⇒ n ∈ ω ∧ ∃k m ∈ ω, 1 ∈ k ∧ 1 ∈ m ∧ k * m = n of type set → prop.

Theorem. (prime_nat_or_composite_nat)

∀n ∈ ω, 1 ∈ n → prime_nat n ∨ composite_nat n

Click to Load Proof

Theorem. (prime_nat_divisor_ex)

∀n, nat_p n → 1 ∈ n → ∃p, prime_nat p ∧ divides_nat p n

Click to Load Proof

Theorem. (nat_1In_not_divides_ordsucc)

∀m n, 1 ∈ m → divides_nat m n → ¬ divides_nat m (ordsucc n)

Click to Load Proof

Definition. We define primes to be {n ∈ ω|prime_nat n} of type set.

Theorem. (form100_11_infinite_primes)

infinite primes

Click to Load Proof

End of Section InfinitePrimes

Beginning of Section InfiniteRamsey

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

Theorem. (atleastp_omega_infinite)

∀X, atleastp ω X → infinite X

Click to Load Proof

Theorem. (infinite_remove1)

∀X, infinite X → ∀y, infinite (X ∖ {y})

Click to Load Proof

Theorem. (infinite_Finite_Subq_ex)

∀X, infinite X → ∀n, nat_p n → ∃Y ⊆ X, equip Y n

Click to Load Proof

Theorem. (infiniteRamsey_lem)

∀X, ∀f g f' : set → set, infinite X → (∀Z ⊆ X, infinite Z → f Z ⊆ Z ∧ infinite (f Z)) → (∀Z ⊆ X, infinite Z → g Z ∈ Z ∧ g Z ∉ f Z) → f' 0 = f X → (∀m, nat_p m → f' (ordsucc m) = f (f' m)) → (∀m, nat_p m → f' m ⊆ X ∧ infinite (f' m)) ∧ (∀m m' ∈ ω, m ⊆ m' → f' m' ⊆ f' m) ∧ (∀m m' ∈ ω, g (f' m) = g (f' m') → m = m')

Click to Load Proof

Theorem. (infiniteRamsey)

∀c, nat_p c → ∀n, nat_p n → ∀X, infinite X → ∀C : set → set, (∀Y ⊆ X, equip Y n → C Y ∈ c) → ∃H ⊆ X, ∃i ∈ c, infinite H ∧ ∀Y ⊆ H, equip Y n → C Y = i

Click to Load Proof

End of Section InfiniteRamsey

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

Theorem. (Inj1_eq)

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

Click to Load Proof

Theorem. (Inj1I1)

∀X : set, 0 ∈ Inj1 X

Click to Load Proof

Theorem. (Inj1I2)

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

Click to Load Proof

Theorem. (Inj1E)

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

Click to Load Proof

Theorem. (Inj1NE1)

∀x : set, Inj1 x ≠ 0

Click to Load Proof

Theorem. (Inj1NE2)

∀x : set, Inj1 x ∉ {0}

Click to Load Proof

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

Theorem. (Inj0I)

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

Click to Load Proof

Theorem. (Inj0E)

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

Click to Load Proof

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

Theorem. (Unj_eq)

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

Click to Load Proof

Theorem. (Unj_Inj1_eq)

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

Click to Load Proof

Theorem. (Inj1_inj)

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

Click to Load Proof

Theorem. (Unj_Inj0_eq)

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

Click to Load Proof

Theorem. (Inj0_inj)

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

Click to Load Proof

Theorem. (Inj0_0)

Inj0 0 = 0

Click to Load Proof

Theorem. (Inj0_Inj1_neq)

∀X Y : set, Inj0 X ≠ Inj1 Y

Click to Load Proof

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

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

Theorem. (Inj0_setsum)

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

Click to Load Proof

Theorem. (Inj1_setsum)

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

Click to Load Proof

Theorem. (setsum_Inj_inv)

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

Click to Load Proof

Theorem. (Inj0_setsum_0L)

∀X : set, 0 + X = Inj0 X

Click to Load Proof

Theorem. (Inj1_setsum_1L)

∀X : set, 1 + X = Inj1 X

Click to Load Proof

Beginning of Section pair_setsum

Let pair ≝ setsum

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

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

Theorem. (Inj0_pair_0_eq)

Inj0 = pair 0

Click to Load Proof

Theorem. (Inj1_pair_1_eq)

Inj1 = pair 1

Click to Load Proof

Theorem. (pairI0)

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

Click to Load Proof

Theorem. (pairI1)

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

Click to Load Proof

Theorem. (pairE)

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

Click to Load Proof

Theorem. (pairE0)

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

Click to Load Proof

Theorem. (pairE1)

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

Click to Load Proof

Theorem. (proj0I)

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

Click to Load Proof

Theorem. (proj0E)

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

Click to Load Proof

Theorem. (proj1I)

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

Click to Load Proof

Theorem. (proj1E)

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

Click to Load Proof

Theorem. (proj0_pair_eq)

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

Click to Load Proof

Theorem. (proj1_pair_eq)

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

Click to Load Proof

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

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

Theorem. (Sigma_eta_proj0_proj1)

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

Click to Load Proof

Theorem. (proj0_Sigma)

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

Click to Load Proof

Theorem. (proj1_Sigma)

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

Click to Load Proof

Theorem. (pair_Sigma)

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

Click to Load Proof

Theorem. (pair_Sigma_E1)

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

Click to Load Proof

Theorem. (Sigma_E)

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

Click to Load Proof

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

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

Theorem. (lamI)

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

Click to Load Proof

Theorem. (lamE)

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

Click to Load Proof

Theorem. (apI)

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

Click to Load Proof

Theorem. (apE)

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

Click to Load Proof

Theorem. (beta)

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

Click to Load Proof

Theorem. (proj0_ap_0)

∀u, proj0 u = u 0

Click to Load Proof

Theorem. (proj1_ap_1)

∀u, proj1 u = u 1

Click to Load Proof

Theorem. (pair_ap_0)

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

Click to Load Proof

Theorem. (pair_ap_1)

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

Click to Load Proof

Theorem. (ap0_Sigma)

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

Click to Load Proof

Theorem. (ap1_Sigma)

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

Click to Load Proof

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

Theorem. (pair_p_I)

∀x y, pair_p (pair x y)

Click to Load Proof

Theorem. (Subq_2_UPair01)

2 ⊆ {0,1}

Click to Load Proof

Theorem. (tuple_pair)

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

Click to Load Proof

Definition. We define Pi to be λX Y ⇒ {f ∈ 𝒫 (∑x ∈ X, ⋃ (Y x))|∀x ∈ X, f x ∈ Y x} of type set → (set → set) → set.

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

Theorem. (PiI)

∀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

Click to Load Proof

Theorem. (lam_Pi)

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

Click to Load Proof

Theorem. (ap_Pi)

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

Click to Load Proof

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

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

Theorem. (pair_tuple_fun)

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

Click to Load Proof

Beginning of Section Tuples

Variable x0 x1 : set

Theorem. (tuple_2_0_eq)

(x0,x1) 0 = x0

Click to Load Proof

Theorem. (tuple_2_1_eq)

(x0,x1) 1 = x1

Click to Load Proof

End of Section Tuples

Theorem. (ReplEq_setprod_ext)

∀X Y, ∀F G : set → set → set, (∀x ∈ X, ∀y ∈ Y, F x y = G x y) → {F (w 0) (w 1)|w ∈ X ⨯ Y} = {G (w 0) (w 1)|w ∈ X ⨯ Y}

Click to Load Proof

Theorem. (lamI2)

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

Click to Load Proof

Theorem. (tuple_2_Sigma)

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

Click to Load Proof

Theorem. (tuple_2_setprod)

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

Click to Load Proof

End of Section pair_setsum

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

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

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

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

Definition. We define DescrR_i_io_1 to be λR ⇒ Eps_i (λx ⇒ (∃y : set → prop, R x y) ∧ (∀y z : set → prop, R x y → R x z → y = z)) of type (set → (set → prop) → prop) → set.

Definition. We define DescrR_i_io_2 to be λR ⇒ Descr_Vo1 (λy ⇒ R (DescrR_i_io_1 R) y) of type (set → (set → prop) → prop) → set → prop.

Theorem. (DescrR_i_io_12)

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

Click to Load Proof

Definition. We define PNoEq_ to be λα p q ⇒ ∀β ∈ α, p β ↔ q β of type set → (set → prop) → (set → prop) → prop.

Theorem. (PNoEq_ref_)

∀α, ∀p : set → prop, PNoEq_ α p p

Click to Load Proof

Theorem. (PNoEq_sym_)

∀α, ∀p q : set → prop, PNoEq_ α p q → PNoEq_ α q p

Click to Load Proof

Theorem. (PNoEq_tra_)

∀α, ∀p q r : set → prop, PNoEq_ α p q → PNoEq_ α q r → PNoEq_ α p r

Click to Load Proof

Theorem. (PNoEq_antimon_)

∀p q : set → prop, ∀α, ordinal α → ∀β ∈ α, PNoEq_ α p q → PNoEq_ β p q

Click to Load Proof

Definition. We define PNoLt_ to be λα p q ⇒ ∃β ∈ α, PNoEq_ β p q ∧ ¬ p β ∧ q β of type set → (set → prop) → (set → prop) → prop.

Theorem. (PNoLt_E_)

∀α, ∀p q : set → prop, PNoLt_ α p q → ∀R : prop, (∀β, β ∈ α → PNoEq_ β p q → ¬ p β → q β → R) → R

Click to Load Proof

Theorem. (PNoLt_irref_)

∀α, ∀p : set → prop, ¬ PNoLt_ α p p

Click to Load Proof

Theorem. (PNoLt_mon_)

∀p q : set → prop, ∀α, ordinal α → ∀β ∈ α, PNoLt_ β p q → PNoLt_ α p q

Click to Load Proof

Theorem. (PNoLt_trichotomy_or_)

∀p q : set → prop, ∀α, ordinal α → PNoLt_ α p q ∨ PNoEq_ α p q ∨ PNoLt_ α q p

Click to Load Proof

Definition. We define PNoLt to be λα p β q ⇒ PNoLt_ (α ∩ β) p q ∨ α ∈ β ∧ PNoEq_ α p q ∧ q α ∨ β ∈ α ∧ PNoEq_ β p q ∧ ¬ p β of type set → (set → prop) → set → (set → prop) → prop.

Theorem. (PNoLtI1)

∀α β, ∀p q : set → prop, PNoLt_ (α ∩ β) p q → PNoLt α p β q

Click to Load Proof

Theorem. (PNoLtI2)

∀α β, ∀p q : set → prop, α ∈ β → PNoEq_ α p q → q α → PNoLt α p β q

Click to Load Proof

Theorem. (PNoLtI3)

∀α β, ∀p q : set → prop, β ∈ α → PNoEq_ β p q → ¬ p β → PNoLt α p β q

Click to Load Proof

Theorem. (PNoLtE)

∀α β, ∀p q : set → prop, PNoLt α p β q → ∀R : prop, (PNoLt_ (α ∩ β) p q → R) → (α ∈ β → PNoEq_ α p q → q α → R) → (β ∈ α → PNoEq_ β p q → ¬ p β → R) → R

Click to Load Proof

Theorem. (PNoLt_irref)

∀α, ∀p : set → prop, ¬ PNoLt α p α p

Click to Load Proof

Theorem. (PNoLt_trichotomy_or)

∀α β, ∀p q : set → prop, ordinal α → ordinal β → PNoLt α p β q ∨ α = β ∧ PNoEq_ α p q ∨ PNoLt β q α p

Click to Load Proof

Theorem. (PNoLtEq_tra)

∀α β, ordinal α → ordinal β → ∀p q r : set → prop, PNoLt α p β q → PNoEq_ β q r → PNoLt α p β r

Click to Load Proof

Theorem. (PNoEqLt_tra)

∀α β, ordinal α → ordinal β → ∀p q r : set → prop, PNoEq_ α p q → PNoLt α q β r → PNoLt α p β r

Click to Load Proof

Theorem. (PNoLt_tra)

∀α β γ, ordinal α → ordinal β → ordinal γ → ∀p q r : set → prop, PNoLt α p β q → PNoLt β q γ r → PNoLt α p γ r

Click to Load Proof

Definition. We define PNoLe to be λα p β q ⇒ PNoLt α p β q ∨ α = β ∧ PNoEq_ α p q of type set → (set → prop) → set → (set → prop) → prop.

Theorem. (PNoLeI1)

∀α β, ∀p q : set → prop, PNoLt α p β q → PNoLe α p β q

Click to Load Proof

Theorem. (PNoLeI2)

∀α, ∀p q : set → prop, PNoEq_ α p q → PNoLe α p α q

Click to Load Proof

Theorem. (PNoLe_ref)

∀α, ∀p : set → prop, PNoLe α p α p

Click to Load Proof

Theorem. (PNoLe_antisym)

∀α β, ordinal α → ordinal β → ∀p q : set → prop, PNoLe α p β q → PNoLe β q α p → α = β ∧ PNoEq_ α p q

Click to Load Proof

Theorem. (PNoLtLe_tra)

∀α β γ, ordinal α → ordinal β → ordinal γ → ∀p q r : set → prop, PNoLt α p β q → PNoLe β q γ r → PNoLt α p γ r

Click to Load Proof

Theorem. (PNoLeLt_tra)

∀α β γ, ordinal α → ordinal β → ordinal γ → ∀p q r : set → prop, PNoLe α p β q → PNoLt β q γ r → PNoLt α p γ r

Click to Load Proof

Theorem. (PNoEqLe_tra)

∀α β, ordinal α → ordinal β → ∀p q r : set → prop, PNoEq_ α p q → PNoLe α q β r → PNoLe α p β r

Click to Load Proof

Theorem. (PNoLe_tra)

∀α β γ, ordinal α → ordinal β → ordinal γ → ∀p q r : set → prop, PNoLe α p β q → PNoLe β q γ r → PNoLe α p γ r

Click to Load Proof

Definition. We define PNo_downc to be λL α p ⇒ ∃β, ordinal β ∧ ∃q : set → prop, L β q ∧ PNoLe α p β q of type (set → (set → prop) → prop) → set → (set → prop) → prop.

Definition. We define PNo_upc to be λR α p ⇒ ∃β, ordinal β ∧ ∃q : set → prop, R β q ∧ PNoLe β q α p of type (set → (set → prop) → prop) → set → (set → prop) → prop.

Theorem. (PNoLe_downc)

∀L : set → (set → prop) → prop, ∀α β, ∀p q : set → prop, ordinal α → ordinal β → PNo_downc L α p → PNoLe β q α p → PNo_downc L β q

Click to Load Proof

Theorem. (PNo_downc_ref)

∀L : set → (set → prop) → prop, ∀α, ordinal α → ∀p : set → prop, L α p → PNo_downc L α p

Click to Load Proof

Theorem. (PNo_upc_ref)

∀R : set → (set → prop) → prop, ∀α, ordinal α → ∀p : set → prop, R α p → PNo_upc R α p

Click to Load Proof

Theorem. (PNoLe_upc)

∀R : set → (set → prop) → prop, ∀α β, ∀p q : set → prop, ordinal α → ordinal β → PNo_upc R α p → PNoLe α p β q → PNo_upc R β q

Click to Load Proof

Definition. We define PNoLt_pwise to be λL R ⇒ ∀γ, ordinal γ → ∀p : set → prop, L γ p → ∀δ, ordinal δ → ∀q : set → prop, R δ q → PNoLt γ p δ q of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → prop.

Theorem. (PNoLt_pwise_downc_upc)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → PNoLt_pwise (PNo_downc L) (PNo_upc R)

Click to Load Proof

Definition. We define PNo_rel_strict_upperbd to be λL α p ⇒ ∀β ∈ α, ∀q : set → prop, PNo_downc L β q → PNoLt β q α p of type (set → (set → prop) → prop) → set → (set → prop) → prop.

Definition. We define PNo_rel_strict_lowerbd to be λR α p ⇒ ∀β ∈ α, ∀q : set → prop, PNo_upc R β q → PNoLt α p β q of type (set → (set → prop) → prop) → set → (set → prop) → prop.

Definition. We define PNo_rel_strict_imv to be λL R α p ⇒ PNo_rel_strict_upperbd L α p ∧ PNo_rel_strict_lowerbd R α p of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.

Theorem. (PNoEq_rel_strict_upperbd)

∀L : set → (set → prop) → prop, ∀α, ordinal α → ∀p q : set → prop, PNoEq_ α p q → PNo_rel_strict_upperbd L α p → PNo_rel_strict_upperbd L α q

Click to Load Proof

Theorem. (PNo_rel_strict_upperbd_antimon)

∀L : set → (set → prop) → prop, ∀α, ordinal α → ∀p : set → prop, ∀β ∈ α, PNo_rel_strict_upperbd L α p → PNo_rel_strict_upperbd L β p

Click to Load Proof

Theorem. (PNoEq_rel_strict_lowerbd)

∀R : set → (set → prop) → prop, ∀α, ordinal α → ∀p q : set → prop, PNoEq_ α p q → PNo_rel_strict_lowerbd R α p → PNo_rel_strict_lowerbd R α q

Click to Load Proof

Theorem. (PNo_rel_strict_lowerbd_antimon)

∀R : set → (set → prop) → prop, ∀α, ordinal α → ∀p : set → prop, ∀β ∈ α, PNo_rel_strict_lowerbd R α p → PNo_rel_strict_lowerbd R β p

Click to Load Proof

Theorem. (PNoEq_rel_strict_imv)

∀L R : set → (set → prop) → prop, ∀α, ordinal α → ∀p q : set → prop, PNoEq_ α p q → PNo_rel_strict_imv L R α p → PNo_rel_strict_imv L R α q

Click to Load Proof

Theorem. (PNo_rel_strict_imv_antimon)

∀L R : set → (set → prop) → prop, ∀α, ordinal α → ∀p : set → prop, ∀β ∈ α, PNo_rel_strict_imv L R α p → PNo_rel_strict_imv L R β p

Click to Load Proof

Definition. We define PNo_rel_strict_uniq_imv to be λL R α p ⇒ PNo_rel_strict_imv L R α p ∧ ∀q : set → prop, PNo_rel_strict_imv L R α q → PNoEq_ α 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 α p ⇒ PNo_rel_strict_imv L R (ordsucc α) (λδ ⇒ p δ ∧ δ ≠ α) ∧ PNo_rel_strict_imv L R (ordsucc α) (λδ ⇒ p δ ∨ δ = α) of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.

Theorem. (PNo_extend0_eq)

∀α, ∀p : set → prop, PNoEq_ α p (λδ ⇒ p δ ∧ δ ≠ α)

Click to Load Proof

Theorem. (PNo_extend1_eq)

∀α, ∀p : set → prop, PNoEq_ α p (λδ ⇒ p δ ∨ δ = α)

Click to Load Proof

Theorem. (PNo_rel_imv_ex)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀α, ordinal α → (∃p : set → prop, PNo_rel_strict_uniq_imv L R α p) ∨ (∃tau ∈ α, ∃p : set → prop, PNo_rel_strict_split_imv L R tau p)

Click to Load Proof

Definition. We define PNo_lenbdd to be λα L ⇒ ∀β, ∀p : set → prop, L β p → β ∈ α of type set → (set → (set → prop) → prop) → prop.

Theorem. (PNo_lenbdd_strict_imv_extend0)

∀L R : set → (set → prop) → prop, ∀α, ordinal α → PNo_lenbdd α L → PNo_lenbdd α R → ∀p : set → prop, PNo_rel_strict_imv L R α p → PNo_rel_strict_imv L R (ordsucc α) (λδ ⇒ p δ ∧ δ ≠ α)

Click to Load Proof

Theorem. (PNo_lenbdd_strict_imv_extend1)

∀L R : set → (set → prop) → prop, ∀α, ordinal α → PNo_lenbdd α L → PNo_lenbdd α R → ∀p : set → prop, PNo_rel_strict_imv L R α p → PNo_rel_strict_imv L R (ordsucc α) (λδ ⇒ p δ ∨ δ = α)

Click to Load Proof

Theorem. (PNo_lenbdd_strict_imv_split)

∀L R : set → (set → prop) → prop, ∀α, ordinal α → PNo_lenbdd α L → PNo_lenbdd α R → ∀p : set → prop, PNo_rel_strict_imv L R α p → PNo_rel_strict_split_imv L R α p

Click to Load Proof

Theorem. (PNo_rel_imv_bdd_ex)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀α, ordinal α → PNo_lenbdd α L → PNo_lenbdd α R → ∃β ∈ ordsucc α, ∃p : set → prop, PNo_rel_strict_split_imv L R β p

Click to Load Proof

Definition. We define PNo_strict_upperbd to be λL α p ⇒ ∀β, ordinal β → ∀q : set → prop, L β q → PNoLt β q α p of type (set → (set → prop) → prop) → set → (set → prop) → prop.

Definition. We define PNo_strict_lowerbd to be λR α p ⇒ ∀β, ordinal β → ∀q : set → prop, R β q → PNoLt α p β q of type (set → (set → prop) → prop) → set → (set → prop) → prop.

Definition. We define PNo_strict_imv to be λL R α p ⇒ PNo_strict_upperbd L α p ∧ PNo_strict_lowerbd R α p of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.

Theorem. (PNoEq_strict_upperbd)

∀L : set → (set → prop) → prop, ∀α, ordinal α → ∀p q : set → prop, PNoEq_ α p q → PNo_strict_upperbd L α p → PNo_strict_upperbd L α q

Click to Load Proof

Theorem. (PNoEq_strict_lowerbd)

∀R : set → (set → prop) → prop, ∀α, ordinal α → ∀p q : set → prop, PNoEq_ α p q → PNo_strict_lowerbd R α p → PNo_strict_lowerbd R α q

Click to Load Proof

Theorem. (PNoEq_strict_imv)

∀L R : set → (set → prop) → prop, ∀α, ordinal α → ∀p q : set → prop, PNoEq_ α p q → PNo_strict_imv L R α p → PNo_strict_imv L R α q

Click to Load Proof

Theorem. (PNo_strict_upperbd_imp_rel_strict_upperbd)

∀L : set → (set → prop) → prop, ∀α, ordinal α → ∀β ∈ ordsucc α, ∀p : set → prop, PNo_strict_upperbd L α p → PNo_rel_strict_upperbd L β p

Click to Load Proof

Theorem. (PNo_strict_lowerbd_imp_rel_strict_lowerbd)

∀R : set → (set → prop) → prop, ∀α, ordinal α → ∀β ∈ ordsucc α, ∀p : set → prop, PNo_strict_lowerbd R α p → PNo_rel_strict_lowerbd R β p

Click to Load Proof

Theorem. (PNo_strict_imv_imp_rel_strict_imv)

∀L R : set → (set → prop) → prop, ∀α, ordinal α → ∀β ∈ ordsucc α, ∀p : set → prop, PNo_strict_imv L R α p → PNo_rel_strict_imv L R β p

Click to Load Proof

Theorem. (PNo_rel_split_imv_imp_strict_imv)

∀L R : set → (set → prop) → prop, ∀α, ordinal α → ∀p : set → prop, PNo_rel_strict_split_imv L R α p → PNo_strict_imv L R α p

Click to Load Proof

Theorem. (PNo_lenbdd_strict_imv_ex)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀α, ordinal α → PNo_lenbdd α L → PNo_lenbdd α R → ∃β ∈ ordsucc α, ∃p : set → prop, PNo_strict_imv L R β p

Click to Load Proof

Definition. We define PNo_least_rep to be λL R β p ⇒ ordinal β ∧ PNo_strict_imv L R β p ∧ ∀γ ∈ β, ∀q : set → prop, ¬ PNo_strict_imv L R γ 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 β p ⇒ PNo_least_rep L R β p ∧ ∀x, x ∉ β → ¬ p x of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.

Theorem. (PNo_strict_imv_pred_eq)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀α, ordinal α → ∀p q : set → prop, PNo_least_rep L R α p → PNo_strict_imv L R α q → ∀β ∈ α, p β ↔ q β

Click to Load Proof

Theorem. (PNo_lenbdd_least_rep2_exuniq2)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀α, ordinal α → PNo_lenbdd α L → PNo_lenbdd α R → ∃β, (∃p : set → prop, PNo_least_rep2 L R β p) ∧ (∀p q : set → prop, PNo_least_rep2 L R β p → PNo_least_rep2 L R β q → p = q)

Click to Load Proof

Definition. We define PNo_bd to be λL R ⇒ DescrR_i_io_1 (PNo_least_rep2 L R) of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set.

Definition. We define PNo_pred to be λL R ⇒ DescrR_i_io_2 (PNo_least_rep2 L R) of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → prop.

Theorem. (PNo_bd_pred_lem)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀α, ordinal α → PNo_lenbdd α L → PNo_lenbdd α R → PNo_least_rep2 L R (PNo_bd L R) (PNo_pred L R)

Click to Load Proof

Theorem. (PNo_bd_pred)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀α, ordinal α → PNo_lenbdd α L → PNo_lenbdd α R → PNo_least_rep L R (PNo_bd L R) (PNo_pred L R)

Click to Load Proof

Theorem. (PNo_bd_In)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀α, ordinal α → PNo_lenbdd α L → PNo_lenbdd α R → PNo_bd L R ∈ ordsucc α

Click to Load Proof

Beginning of Section TaggedSets

Let tag : set → set ≝ λα ⇒ SetAdjoin α {1}

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.

Theorem. (not_TransSet_Sing1)

¬ TransSet {1}

Click to Load Proof

Theorem. (not_ordinal_Sing1)

¬ ordinal {1}

Click to Load Proof

Theorem. (tagged_not_ordinal)

∀y, ¬ ordinal (y ')

Click to Load Proof

Theorem. (tagged_notin_ordinal)

∀α y, ordinal α → (y ') ∉ α

Click to Load Proof

Theorem. (tagged_eqE_Subq)

∀α β, ordinal α → α ' = β ' → α ⊆ β

Click to Load Proof

Theorem. (tagged_eqE_eq)

∀α β, ordinal α → ordinal β → α ' = β ' → α = β

Click to Load Proof

Theorem. (tagged_ReplE)

∀α β, ordinal α → ordinal β → β ' ∈ {γ '|γ ∈ α} → β ∈ α

Click to Load Proof

Theorem. (ordinal_notin_tagged_Repl)

∀α Y, ordinal α → α ∉ {y '|y ∈ Y}

Click to Load Proof

Definition. We define SNoElts_ to be λα ⇒ α ∪ {β '|β ∈ α} of type set → set.

Theorem. (SNoElts_mon)

∀α β, α ⊆ β → SNoElts_ α ⊆ SNoElts_ β

Click to Load Proof

Definition. We define SNo_ to be λα x ⇒ x ⊆ SNoElts_ α ∧ ∀β ∈ α, exactly1of2 (β ' ∈ x) (β ∈ x) of type set → set → prop.

Definition. We define PSNo to be λα p ⇒ {β ∈ α|p β} ∪ {β '|β ∈ α, ¬ p β} of type set → (set → prop) → set.

Theorem. (PNoEq_PSNo)

∀α, ordinal α → ∀p : set → prop, PNoEq_ α (λβ ⇒ β ∈ PSNo α p) p

Click to Load Proof

Theorem. (SNo_PSNo)

∀α, ordinal α → ∀p : set → prop, SNo_ α (PSNo α p)

Click to Load Proof

Theorem. (SNo_PSNo_eta_)

∀α x, ordinal α → SNo_ α x → x = PSNo α (λβ ⇒ β ∈ x)

Click to Load Proof

Definition. We define SNo to be λx ⇒ ∃α, ordinal α ∧ SNo_ α x of type set → prop.

Theorem. (SNo_SNo)

∀α, ordinal α → ∀z, SNo_ α z → SNo z

Click to Load Proof

Definition. We define SNoLev to be λx ⇒ Eps_i (λα ⇒ ordinal α ∧ SNo_ α x) of type set → set.

Theorem. (SNoLev_uniq_Subq)

∀x α β, ordinal α → ordinal β → SNo_ α x → SNo_ β x → α ⊆ β

Click to Load Proof

Theorem. (SNoLev_uniq)

∀x α β, ordinal α → ordinal β → SNo_ α x → SNo_ β x → α = β

Click to Load Proof

Theorem. (SNoLev_prop)

∀x, SNo x → ordinal (SNoLev x) ∧ SNo_ (SNoLev x) x

Click to Load Proof

Theorem. (SNoLev_ordinal)

∀x, SNo x → ordinal (SNoLev x)

Click to Load Proof

Theorem. (SNoLev_)

∀x, SNo x → SNo_ (SNoLev x) x

Click to Load Proof

Theorem. (SNo_PSNo_eta)

∀x, SNo x → x = PSNo (SNoLev x) (λβ ⇒ β ∈ x)

Click to Load Proof

Theorem. (SNoLev_PSNo)

∀α, ordinal α → ∀p : set → prop, SNoLev (PSNo α p) = α

Click to Load Proof

Theorem. (SNo_Subq)

∀x y, SNo x → SNo y → SNoLev x ⊆ SNoLev y → (∀α ∈ SNoLev x, α ∈ x ↔ α ∈ y) → x ⊆ y

Click to Load Proof

Definition. We define SNoEq_ to be λα x y ⇒ PNoEq_ α (λβ ⇒ β ∈ x) (λβ ⇒ β ∈ y) of type set → set → set → prop.

Theorem. (SNoEq_I)

∀α x y, (∀β ∈ α, β ∈ x ↔ β ∈ y) → SNoEq_ α x y

Click to Load Proof

Theorem. (SNo_eq)

∀x y, SNo x → SNo y → SNoLev x = SNoLev y → SNoEq_ (SNoLev x) x y → x = y

Click to Load Proof

End of Section TaggedSets

Definition. We define SNoLt to be λx y ⇒ PNoLt (SNoLev x) (λβ ⇒ β ∈ x) (SNoLev y) (λβ ⇒ β ∈ 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) (λβ ⇒ β ∈ x) (SNoLev y) (λβ ⇒ β ∈ y) of type set → set → prop.

Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.

Theorem. (SNoLtLe)

∀x y, x < y → x ≤ y

Click to Load Proof

Theorem. (SNoLeE)

∀x y, SNo x → SNo y → x ≤ y → x < y ∨ x = y

Click to Load Proof

Theorem. (SNoEq_sym_)

∀α x y, SNoEq_ α x y → SNoEq_ α y x

Click to Load Proof

Theorem. (SNoEq_tra_)

∀α x y z, SNoEq_ α x y → SNoEq_ α y z → SNoEq_ α x z

Click to Load Proof

Theorem. (SNoLtE)

∀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

Click to Load Proof

Theorem. (SNoLtI2)

∀x y, SNoLev x ∈ SNoLev y → SNoEq_ (SNoLev x) x y → SNoLev x ∈ y → x < y

Click to Load Proof

Theorem. (SNoLtI3)

∀x y, SNoLev y ∈ SNoLev x → SNoEq_ (SNoLev y) x y → SNoLev y ∉ x → x < y

Click to Load Proof

Theorem. (SNoLt_irref)

∀x, ¬ SNoLt x x

Click to Load Proof

Theorem. (SNoLt_trichotomy_or)

∀x y, SNo x → SNo y → x < y ∨ x = y ∨ y < x

Click to Load Proof

Theorem. (SNoLt_trichotomy_or_impred)

∀x y, SNo x → SNo y → ∀p : prop, (x < y → p) → (x = y → p) → (y < x → p) → p

Click to Load Proof

Theorem. (SNoLt_tra)

∀x y z, SNo x → SNo y → SNo z → x < y → y < z → x < z

Click to Load Proof

Theorem. (SNoLe_ref)

∀x, SNoLe x x

Click to Load Proof

Theorem. (SNoLe_antisym)

∀x y, SNo x → SNo y → x ≤ y → y ≤ x → x = y

Click to Load Proof

Theorem. (SNoLtLe_tra)

∀x y z, SNo x → SNo y → SNo z → x < y → y ≤ z → x < z

Click to Load Proof

Theorem. (SNoLeLt_tra)

∀x y z, SNo x → SNo y → SNo z → x ≤ y → y < z → x < z

Click to Load Proof

Theorem. (SNoLe_tra)

∀x y z, SNo x → SNo y → SNo z → x ≤ y → y ≤ z → x ≤ z

Click to Load Proof

Theorem. (SNoLtLe_or)

∀x y, SNo x → SNo y → x < y ∨ y ≤ x

Click to Load Proof

Theorem. (SNoLt_PSNo_PNoLt)

∀α β, ∀p q : set → prop, ordinal α → ordinal β → PSNo α p < PSNo β q → PNoLt α p β q

Click to Load Proof

Theorem. (PNoLt_SNoLt_PSNo)

∀α β, ∀p q : set → prop, ordinal α → ordinal β → PNoLt α p β q → PSNo α p < PSNo β q

Click to Load Proof

Definition. We define SNoCut to be λL R ⇒ PSNo (PNo_bd (λα p ⇒ ordinal α ∧ PSNo α p ∈ L) (λα p ⇒ ordinal α ∧ PSNo α p ∈ R)) (PNo_pred (λα p ⇒ ordinal α ∧ PSNo α p ∈ L) (λα p ⇒ ordinal α ∧ PSNo α 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.

Theorem. (SNoCutP_SNoCut)

∀L R, SNoCutP L R → SNo (SNoCut L R) ∧ SNoLev (SNoCut L R) ∈ ordsucc ((⋃_{x ∈ L}ordsucc (SNoLev x)) ∪ (⋃_{y ∈ R}ordsucc (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)

Click to Load Proof

Theorem. (SNoCutP_SNoCut_impred)

∀L R, SNoCutP L R → ∀p : prop, (SNo (SNoCut L R) → SNoLev (SNoCut L R) ∈ ordsucc ((⋃_{x ∈ L}ordsucc (SNoLev x)) ∪ (⋃_{y ∈ R}ordsucc (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

Click to Load Proof

Theorem. (SNoCutP_L_0)

∀L, (∀x ∈ L, SNo x) → SNoCutP L 0

Click to Load Proof

Theorem. (SNoCutP_0_0)

SNoCutP 0 0

Click to Load Proof

Definition. We define SNoS_ to be λα ⇒ {x ∈ 𝒫 (SNoElts_ α)|∃β ∈ α, SNo_ β x} of type set → set.

Theorem. (SNoS_E)

∀α, ordinal α → ∀x ∈ SNoS_ α, ∃β ∈ α, SNo_ β x

Click to Load Proof

Beginning of Section TaggedSets2

Let tag : set → set ≝ λα ⇒ SetAdjoin α {1}

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.

Theorem. (SNoS_I)

∀α, ordinal α → ∀x, ∀β ∈ α, SNo_ β x → x ∈ SNoS_ α

Click to Load Proof

Theorem. (SNoS_I2)

∀x y, SNo x → SNo y → SNoLev x ∈ SNoLev y → x ∈ SNoS_ (SNoLev y)

Click to Load Proof

Theorem. (SNoS_Subq)

∀α β, ordinal α → ordinal β → α ⊆ β → SNoS_ α ⊆ SNoS_ β

Click to Load Proof

Theorem. (SNoLev_uniq2)

∀α, ordinal α → ∀x, SNo_ α x → SNoLev x = α

Click to Load Proof

Theorem. (SNoS_E2)

∀α, ordinal α → ∀x ∈ SNoS_ α, ∀p : prop, (SNoLev x ∈ α → ordinal (SNoLev x) → SNo x → SNo_ (SNoLev x) x → p) → p

Click to Load Proof

Theorem. (SNoS_In_neq)

∀w, SNo w → ∀x ∈ SNoS_ (SNoLev w), x ≠ w

Click to Load Proof

Theorem. (SNoS_SNoLev)

∀z, SNo z → z ∈ SNoS_ (ordsucc (SNoLev z))

Click to Load Proof

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.

Theorem. (SNoCutP_SNoL_SNoR)

∀z, SNo z → SNoCutP (SNoL z) (SNoR z)

Click to Load Proof

Theorem. (SNoL_E)

∀x, SNo x → ∀w ∈ SNoL x, ∀p : prop, (SNo w → SNoLev w ∈ SNoLev x → w < x → p) → p

Click to Load Proof

Theorem. (SNoR_E)

∀x, SNo x → ∀z ∈ SNoR x, ∀p : prop, (SNo z → SNoLev z ∈ SNoLev x → x < z → p) → p

Click to Load Proof

Theorem. (SNoL_SNoS_)

∀z, SNoL z ⊆ SNoS_ (SNoLev z)

Click to Load Proof

Theorem. (SNoR_SNoS_)

∀z, SNoR z ⊆ SNoS_ (SNoLev z)

Click to Load Proof

Theorem. (SNoL_SNoS)

∀x, SNo x → ∀w ∈ SNoL x, w ∈ SNoS_ (SNoLev x)

Click to Load Proof

Theorem. (SNoR_SNoS)

∀x, SNo x → ∀z ∈ SNoR x, z ∈ SNoS_ (SNoLev x)

Click to Load Proof

Theorem. (SNoL_I)

∀z, SNo z → ∀x, SNo x → SNoLev x ∈ SNoLev z → x < z → x ∈ SNoL z

Click to Load Proof

Theorem. (SNoR_I)

∀z, SNo z → ∀y, SNo y → SNoLev y ∈ SNoLev z → z < y → y ∈ SNoR z

Click to Load Proof

Theorem. (SNo_eta)

∀z, SNo z → z = SNoCut (SNoL z) (SNoR z)

Click to Load Proof

Theorem. (SNoCutP_SNo_SNoCut)

∀L R, SNoCutP L R → SNo (SNoCut L R)

Click to Load Proof

Theorem. (SNoCutP_SNoCut_L)

∀L R, SNoCutP L R → ∀x ∈ L, x < SNoCut L R

Click to Load Proof

Theorem. (SNoCutP_SNoCut_R)

∀L R, SNoCutP L R → ∀y ∈ R, SNoCut L R < y

Click to Load Proof

Theorem. (SNoCutP_SNoCut_fst)

∀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

Click to Load Proof

Theorem. (SNoCut_Le)

∀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

Click to Load Proof

Theorem. (SNoCut_ext)

∀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

Click to Load Proof

Theorem. (SNoLt_SNoL_or_SNoR_impred)

∀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

Click to Load Proof

Theorem. (SNoL_or_SNoR_impred)

∀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

Click to Load Proof

Theorem. (SNoL_SNoCutP_ex)

∀L R, SNoCutP L R → ∀w ∈ SNoL (SNoCut L R), ∃w' ∈ L, w ≤ w'

Click to Load Proof

Theorem. (SNoR_SNoCutP_ex)

∀L R, SNoCutP L R → ∀z ∈ SNoR (SNoCut L R), ∃z' ∈ R, z' ≤ z

Click to Load Proof

Theorem. (ordinal_SNo_)

∀α, ordinal α → SNo_ α α

Click to Load Proof

Theorem. (ordinal_SNo)

∀α, ordinal α → SNo α

Click to Load Proof

Theorem. (ordinal_SNoLev)

∀α, ordinal α → SNoLev α = α

Click to Load Proof

Theorem. (ordinal_SNoLev_max)

∀α, ordinal α → ∀z, SNo z → SNoLev z ∈ α → z < α

Click to Load Proof

Theorem. (ordinal_SNoL)

∀α, ordinal α → SNoL α = SNoS_ α

Click to Load Proof

Theorem. (ordinal_SNoR)

∀α, ordinal α → SNoR α = Empty

Click to Load Proof

Theorem. (nat_p_SNo)

∀n, nat_p n → SNo n

Click to Load Proof

Theorem. (omega_SNo)

∀n ∈ ω, SNo n

Click to Load Proof

Theorem. (omega_SNoS_omega)

ω ⊆ SNoS_ ω

Click to Load Proof

Theorem. (ordinal_In_SNoLt)

∀α, ordinal α → ∀β ∈ α, β < α

Click to Load Proof

Theorem. (ordinal_SNoLev_max_2)

∀α, ordinal α → ∀z, SNo z → SNoLev z ∈ ordsucc α → z ≤ α

Click to Load Proof

Theorem. (ordinal_Subq_SNoLe)

∀α β, ordinal α → ordinal β → α ⊆ β → α ≤ β

Click to Load Proof

Theorem. (ordinal_SNoLt_In)

∀α β, ordinal α → ordinal β → α < β → α ∈ β

Click to Load Proof

Theorem. (omega_nonneg)

∀m ∈ ω, 0 ≤ m

Click to Load Proof

Theorem. (SNo_0)

SNo 0

Click to Load Proof

Theorem. (SNo_1)

SNo 1

Click to Load Proof

Theorem. (SNo_2)

SNo 2

Click to Load Proof

Theorem. (SNoLev_0)

SNoLev 0 = 0

Click to Load Proof

Theorem. (SNoCut_0_0)

SNoCut 0 0 = 0

Click to Load Proof

Theorem. (SNoL_0)

SNoL 0 = 0

Click to Load Proof

Theorem. (SNoR_0)

SNoR 0 = 0

Click to Load Proof

Theorem. (SNoL_1)

SNoL 1 = 1

Click to Load Proof

Theorem. (SNoR_1)

SNoR 1 = 0

Click to Load Proof

Theorem. (SNo_max_SNoLev)

∀x, SNo x → (∀y ∈ SNoS_ (SNoLev x), y < x) → SNoLev x = x

Click to Load Proof

Theorem. (SNo_max_ordinal)

∀x, SNo x → (∀y ∈ SNoS_ (SNoLev x), y < x) → ordinal x

Click to Load Proof

Theorem. (pos_low_eq_one)

∀x, SNo x → 0 < x → SNoLev x ⊆ 1 → x = 1

Click to Load Proof

Definition. We define SNo_extend0 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λδ ⇒ δ ∈ x ∧ δ ≠ SNoLev x) of type set → set.

Definition. We define SNo_extend1 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λδ ⇒ δ ∈ x ∨ δ = SNoLev x) of type set → set.

Theorem. (SNo_extend0_SNo_)

∀x, SNo x → SNo_ (ordsucc (SNoLev x)) (SNo_extend0 x)

Click to Load Proof

Theorem. (SNo_extend1_SNo_)

∀x, SNo x → SNo_ (ordsucc (SNoLev x)) (SNo_extend1 x)

Click to Load Proof

Theorem. (SNo_extend0_SNo)

∀x, SNo x → SNo (SNo_extend0 x)

Click to Load Proof

Theorem. (SNo_extend1_SNo)

∀x, SNo x → SNo (SNo_extend1 x)

Click to Load Proof

Theorem. (SNo_extend0_SNoLev)

∀x, SNo x → SNoLev (SNo_extend0 x) = ordsucc (SNoLev x)

Click to Load Proof

Theorem. (SNo_extend1_SNoLev)

∀x, SNo x → SNoLev (SNo_extend1 x) = ordsucc (SNoLev x)

Click to Load Proof

Theorem. (SNo_extend0_nIn)

∀x, SNo x → SNoLev x ∉ SNo_extend0 x

Click to Load Proof

Theorem. (SNo_extend1_In)

∀x, SNo x → SNoLev x ∈ SNo_extend1 x

Click to Load Proof

Theorem. (SNo_extend0_SNoEq)

∀x, SNo x → SNoEq_ (SNoLev x) (SNo_extend0 x) x

Click to Load Proof

Theorem. (SNo_extend1_SNoEq)

∀x, SNo x → SNoEq_ (SNoLev x) (SNo_extend1 x) x

Click to Load Proof

Theorem. (SNoLev_0_eq_0)

∀x, SNo x → SNoLev x = 0 → x = 0

Click to Load Proof

Definition. We define eps_ to be λn ⇒ {0} ∪ {(ordsucc m) '|m ∈ n} of type set → set.

Theorem. (eps_ordinal_In_eq_0)

∀n α, ordinal α → α ∈ eps_ n → α = 0

Click to Load Proof

Theorem. (eps_0_1)

eps_ 0 = 1

Click to Load Proof

Theorem. (SNo__eps_)

∀n ∈ ω, SNo_ (ordsucc n) (eps_ n)

Click to Load Proof

Theorem. (SNo_eps_)

∀n ∈ ω, SNo (eps_ n)

Click to Load Proof

Theorem. (SNo_eps_1)

SNo (eps_ 1)

Click to Load Proof

Theorem. (SNoLev_eps_)

∀n ∈ ω, SNoLev (eps_ n) = ordsucc n

Click to Load Proof

Theorem. (SNo_eps_SNoS_omega)

∀n ∈ ω, eps_ n ∈ SNoS_ ω

Click to Load Proof

Theorem. (SNo_eps_decr)

∀n ∈ ω, ∀m ∈ n, eps_ n < eps_ m

Click to Load Proof

Theorem. (SNo_eps_pos)

∀n ∈ ω, 0 < eps_ n

Click to Load Proof

Theorem. (SNo_pos_eps_Lt)

∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc n), 0 < x → eps_ n < x

Click to Load Proof

Theorem. (SNo_pos_eps_Le)

∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc (ordsucc n)), 0 < x → eps_ n ≤ x

Click to Load Proof

Theorem. (eps_SNo_eq)

∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc n), 0 < x → SNoEq_ (SNoLev x) (eps_ n) x → ∃m ∈ n, x = eps_ m

Click to Load Proof

Theorem. (eps_SNoCutP)

∀n ∈ ω, SNoCutP {0} {eps_ m|m ∈ n}

Click to Load Proof

Theorem. (eps_SNoCut)

∀n ∈ ω, eps_ n = SNoCut {0} {eps_ m|m ∈ n}

Click to Load Proof

End of Section TaggedSets2

Theorem. (SNo_etaE)

∀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

Click to Load Proof

Theorem. (SNo_ind)

∀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

Click to Load Proof

Beginning of Section SurrealRecI

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

Let default : set ≝ Eps_i (λ_ ⇒ True)

Let G : set → (set → set → set) → set → set ≝ λα g ⇒ If_ii (ordinal α) (λz : set ⇒ if z ∈ SNoS_ (ordsucc α) then F z (λw ⇒ g (SNoLev w) w) else default) (λz : set ⇒ default)

Definition. We define SNo_rec_i to be λz ⇒ In_rec_ii G (SNoLev z) z of type set → set.

Hypothesis Fr : ∀z, SNo z → ∀g h : set → set, (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h

Theorem. (SNo_rec_i_eq)

∀z, SNo z → SNo_rec_i z = F z SNo_rec_i

Click to Load Proof

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) ≝ λα g ⇒ If_iii (ordinal α) (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc α)) (F z (λw ⇒ g (SNoLev w) w)) default) (λz : set ⇒ default)

Definition. We define SNo_rec_ii to be λz ⇒ In_rec_iii G (SNoLev z) z of type set → (set → set).

Hypothesis Fr : ∀z, SNo z → ∀g h : set → (set → set), (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h

Theorem. (SNo_rec_ii_eq)

∀z, SNo z → SNo_rec_ii z = F z SNo_rec_ii

Click to Load Proof

End of Section SurrealRecII

Beginning of Section SurrealRec2

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

Let G : set → (set → set → set) → set → (set → set) → set ≝ λw f z g ⇒ F w z (λx y ⇒ if x = w then g y else f x y)

Let H : set → (set → set → set) → set → set ≝ λw f z ⇒ if SNo z then SNo_rec_i (G w f) z else Empty

Definition. We define SNo_rec2 to be SNo_rec_ii H of type set → set → set.

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

Theorem. (SNo_rec2_G_prop)

∀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

Click to Load Proof

Theorem. (SNo_rec2_eq_1)

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

Click to Load Proof

Theorem. (SNo_rec2_eq)

∀w, SNo w → ∀z, SNo z → SNo_rec2 w z = F w z SNo_rec2

Click to Load Proof

End of Section SurrealRec2

Theorem. (SNo_ordinal_ind)

∀P : set → prop, (∀α, ordinal α → ∀x ∈ SNoS_ α, P x) → (∀x, SNo x → P x)

Click to Load Proof

Theorem. (SNo_ordinal_ind2)

∀P : set → set → prop, (∀α, ordinal α → ∀β, ordinal β → ∀x ∈ SNoS_ α, ∀y ∈ SNoS_ β, P x y) → (∀x y, SNo x → SNo y → P x y)

Click to Load Proof

Theorem. (SNo_ordinal_ind3)

∀P : set → set → set → prop, (∀α, ordinal α → ∀β, ordinal β → ∀γ, ordinal γ → ∀x ∈ SNoS_ α, ∀y ∈ SNoS_ β, ∀z ∈ SNoS_ γ, P x y z) → (∀x y z, SNo x → SNo y → SNo z → P x y z)

Click to Load Proof

Theorem. (SNoLev_ind)

∀P : set → prop, (∀x, SNo x → (∀w ∈ SNoS_ (SNoLev x), P w) → P x) → (∀x, SNo x → P x)

Click to Load Proof

Theorem. (SNoLev_ind2)

∀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

Click to Load Proof

Theorem. (SNoLev_ind3)

∀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

Click to Load Proof

Theorem. (SNo_omega)

SNo ω

Click to Load Proof

Theorem. (SNoLt_0_1)

0 < 1

Click to Load Proof

Theorem. (SNoLt_0_2)

0 < 2

Click to Load Proof

Theorem. (SNoLt_1_2)

1 < 2

Click to Load Proof

Theorem. (restr_SNo_)

∀x, SNo x → ∀α ∈ SNoLev x, SNo_ α (x ∩ SNoElts_ α)

Click to Load Proof

Theorem. (restr_SNo)

∀x, SNo x → ∀α ∈ SNoLev x, SNo (x ∩ SNoElts_ α)

Click to Load Proof

Theorem. (restr_SNoLev)

∀x, SNo x → ∀α ∈ SNoLev x, SNoLev (x ∩ SNoElts_ α) = α

Click to Load Proof

Theorem. (restr_SNoEq)

∀x, SNo x → ∀α ∈ SNoLev x, SNoEq_ α (x ∩ SNoElts_ α) x

Click to Load Proof

Theorem. (SNo_extend0_restr_eq)

∀x, SNo x → x = SNo_extend0 x ∩ SNoElts_ (SNoLev x)

Click to Load Proof

Theorem. (SNo_extend1_restr_eq)

∀x, SNo x → x = SNo_extend1 x ∩ SNoElts_ (SNoLev x)

Click to Load Proof

Beginning of Section SurrealMinus

Definition. We define minus_SNo to be SNo_rec_i (λx m ⇒ SNoCut {m z|z ∈ SNoR x} {m w|w ∈ SNoL x}) of type set → set.

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.

Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.

Theorem. (minus_SNo_eq)

∀x, SNo x → - x = SNoCut {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}

Click to Load Proof

Theorem. (minus_SNo_prop1)

∀x, SNo x → SNo (- x) ∧ (∀u ∈ SNoL x, - x < - u) ∧ (∀u ∈ SNoR x, - u < - x) ∧ SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}

Click to Load Proof

Theorem. (SNo_minus_SNo)

∀x, SNo x → SNo (- x)

Click to Load Proof

Theorem. (minus_SNo_Lt_contra)

∀x y, SNo x → SNo y → x < y → - y < - x

Click to Load Proof

Theorem. (minus_SNo_Le_contra)

∀x y, SNo x → SNo y → x ≤ y → - y ≤ - x

Click to Load Proof

Theorem. (minus_SNo_SNoCutP)

∀x, SNo x → SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}

Click to Load Proof

Theorem. (minus_SNo_SNoCutP_gen)

∀L R, SNoCutP L R → SNoCutP {- z|z ∈ R} {- w|w ∈ L}

Click to Load Proof

Theorem. (minus_SNo_Lev_lem1)

∀α, ordinal α → ∀x ∈ SNoS_ α, SNoLev (- x) ⊆ SNoLev x

Click to Load Proof

Theorem. (minus_SNo_Lev_lem2)

∀x, SNo x → SNoLev (- x) ⊆ SNoLev x

Click to Load Proof

Theorem. (minus_SNo_invol)

∀x, SNo x → - - x = x

Click to Load Proof

Theorem. (minus_SNo_Lev)

∀x, SNo x → SNoLev (- x) = SNoLev x

Click to Load Proof

Theorem. (minus_SNo_SNo_)

∀α, ordinal α → ∀x, SNo_ α x → SNo_ α (- x)

Click to Load Proof

Theorem. (minus_SNo_SNoS_)

∀α, ordinal α → ∀x, x ∈ SNoS_ α → - x ∈ SNoS_ α

Click to Load Proof

Theorem. (minus_SNoCut_eq_lem)

∀v, SNo v → ∀L R, SNoCutP L R → v = SNoCut L R → - v = SNoCut {- z|z ∈ R} {- w|w ∈ L}

Click to Load Proof

Theorem. (minus_SNoCut_eq)

∀L R, SNoCutP L R → - SNoCut L R = SNoCut {- z|z ∈ R} {- w|w ∈ L}

Click to Load Proof

Theorem. (minus_SNo_Lt_contra1)

∀x y, SNo x → SNo y → - x < y → - y < x

Click to Load Proof

Theorem. (minus_SNo_Lt_contra2)

∀x y, SNo x → SNo y → x < - y → y < - x

Click to Load Proof

Theorem. (mordinal_SNoLev_min_2)

∀α, ordinal α → ∀z, SNo z → SNoLev z ∈ ordsucc α → - α ≤ z

Click to Load Proof

Theorem. (minus_SNo_SNoS_omega)

∀x ∈ SNoS_ ω, - x ∈ SNoS_ ω

Click to Load Proof

Theorem. (SNoL_minus_SNoR)

∀x, SNo x → SNoL (- x) = {- w|w ∈ SNoR x}

Click to Load Proof

End of Section SurrealMinus

Beginning of Section SurrealAdd

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.

Definition. We define add_SNo to be SNo_rec2 (λx y a ⇒ SNoCut ({a w y|w ∈ SNoL x} ∪ {a x w|w ∈ SNoL y}) ({a z y|z ∈ SNoR x} ∪ {a x z|z ∈ SNoR y})) of type set → set → set.

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

Theorem. (add_SNo_eq)

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

Click to Load Proof

Theorem. (add_SNo_prop1)

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

Click to Load Proof

Theorem. (SNo_add_SNo)

∀x y, SNo x → SNo y → SNo (x + y)

Click to Load Proof

Theorem. (SNo_add_SNo_3)

∀x y z, SNo x → SNo y → SNo z → SNo (x + y + z)

Click to Load Proof

Theorem. (SNo_add_SNo_3c)

∀x y z, SNo x → SNo y → SNo z → SNo (x + y + - z)

Click to Load Proof

Theorem. (SNo_add_SNo_4)

∀x y z w, SNo x → SNo y → SNo z → SNo w → SNo (x + y + z + w)

Click to Load Proof

Theorem. (add_SNo_Lt1)

∀x y z, SNo x → SNo y → SNo z → x < z → x + y < z + y

Click to Load Proof

Theorem. (add_SNo_Le1)

∀x y z, SNo x → SNo y → SNo z → x ≤ z → x + y ≤ z + y

Click to Load Proof

Theorem. (add_SNo_Lt2)

∀x y z, SNo x → SNo y → SNo z → y < z → x + y < x + z

Click to Load Proof

Theorem. (add_SNo_Le2)

∀x y z, SNo x → SNo y → SNo z → y ≤ z → x + y ≤ x + z

Click to Load Proof

Theorem. (add_SNo_Lt3a)

∀x y z w, SNo x → SNo y → SNo z → SNo w → x < z → y ≤ w → x + y < z + w

Click to Load Proof

Theorem. (add_SNo_Lt3b)

∀x y z w, SNo x → SNo y → SNo z → SNo w → x ≤ z → y < w → x + y < z + w

Click to Load Proof

Theorem. (add_SNo_Lt3)

∀x y z w, SNo x → SNo y → SNo z → SNo w → x < z → y < w → x + y < z + w

Click to Load Proof

Theorem. (add_SNo_Le3)

∀x y z w, SNo x → SNo y → SNo z → SNo w → x ≤ z → y ≤ w → x + y ≤ z + w

Click to Load Proof

Theorem. (add_SNo_SNoCutP)

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

Click to Load Proof

Theorem. (add_SNo_com)

∀x y, SNo x → SNo y → x + y = y + x

Click to Load Proof

Theorem. (add_SNo_0L)

∀x, SNo x → 0 + x = x

Click to Load Proof

Theorem. (add_SNo_0R)

∀x, SNo x → x + 0 = x

Click to Load Proof

Theorem. (add_SNo_minus_SNo_linv)

∀x, SNo x → - x + x = 0

Click to Load Proof

Theorem. (add_SNo_minus_SNo_rinv)

∀x, SNo x → x + - x = 0

Click to Load Proof

Theorem. (add_SNo_ordinal_SNoCutP)

∀α, ordinal α → ∀β, ordinal β → SNoCutP ({x + β|x ∈ SNoS_ α} ∪ {α + x|x ∈ SNoS_ β}) Empty

Click to Load Proof

Theorem. (add_SNo_ordinal_eq)

∀α, ordinal α → ∀β, ordinal β → α + β = SNoCut ({x + β|x ∈ SNoS_ α} ∪ {α + x|x ∈ SNoS_ β}) Empty

Click to Load Proof

Theorem. (add_SNo_ordinal_ordinal)

∀α, ordinal α → ∀β, ordinal β → ordinal (α + β)

Click to Load Proof

Theorem. (add_SNo_ordinal_SL)

∀α, ordinal α → ∀β, ordinal β → ordsucc α + β = ordsucc (α + β)

Click to Load Proof

Theorem. (add_SNo_ordinal_SR)

∀α, ordinal α → ∀β, ordinal β → α + ordsucc β = ordsucc (α + β)

Click to Load Proof

Theorem. (add_SNo_ordinal_InL)

∀α, ordinal α → ∀β, ordinal β → ∀γ ∈ α, γ + β ∈ α + β

Click to Load Proof

Theorem. (add_SNo_ordinal_InR)

∀α, ordinal α → ∀β, ordinal β → ∀γ ∈ β, α + γ ∈ α + β

Click to Load Proof

Theorem. (add_nat_add_SNo)

∀n m ∈ ω, add_nat n m = n + m

Click to Load Proof

Theorem. (add_SNo_In_omega)

∀n m ∈ ω, n + m ∈ ω

Click to Load Proof

Theorem. (add_SNo_1_1_2)

1 + 1 = 2

Click to Load Proof

Theorem. (add_SNo_SNoL_interpolate)

∀x y, SNo x → SNo y → ∀u ∈ SNoL (x + y), (∃v ∈ SNoL x, u ≤ v + y) ∨ (∃v ∈ SNoL y, u ≤ x + v)

Click to Load Proof

Theorem. (add_SNo_SNoR_interpolate)

∀x y, SNo x → SNo y → ∀u ∈ SNoR (x + y), (∃v ∈ SNoR x, v + y ≤ u) ∨ (∃v ∈ SNoR y, x + v ≤ u)

Click to Load Proof

Theorem. (add_SNo_assoc)

∀x y z, SNo x → SNo y → SNo z → x + (y + z) = (x + y) + z

Click to Load Proof

Theorem. (add_SNo_minus_R2)

∀x y, SNo x → SNo y → (x + y) + - y = x

Click to Load Proof

Theorem. (add_SNo_minus_R2')

∀x y, SNo x → SNo y → (x + - y) + y = x

Click to Load Proof

Theorem. (add_SNo_minus_L2)

∀x y, SNo x → SNo y → - x + (x + y) = y

Click to Load Proof

Theorem. (add_SNo_minus_L2')

∀x y, SNo x → SNo y → x + (- x + y) = y

Click to Load Proof

Theorem. (add_SNo_cancel_L)

∀x y z, SNo x → SNo y → SNo z → x + y = x + z → y = z

Click to Load Proof

Theorem. (add_SNo_cancel_R)

∀x y z, SNo x → SNo y → SNo z → x + y = z + y → x = z

Click to Load Proof

Theorem. (minus_SNo_0)

- 0 = 0

Click to Load Proof

Theorem. (minus_add_SNo_distr)

∀x y, SNo x → SNo y → - (x + y) = (- x) + (- y)

Click to Load Proof

Theorem. (minus_add_SNo_distr_3)

∀x y z, SNo x → SNo y → SNo z → - (x + y + z) = - x + - y + - z

Click to Load Proof

Theorem. (add_SNo_Lev_bd)

∀x y, SNo x → SNo y → SNoLev (x + y) ⊆ SNoLev x + SNoLev y

Click to Load Proof

Theorem. (add_SNo_SNoS_omega)

∀x y ∈ SNoS_ ω, x + y ∈ SNoS_ ω

Click to Load Proof

Theorem. (add_SNo_Lt1_cancel)

∀x y z, SNo x → SNo y → SNo z → x + y < z + y → x < z

Click to Load Proof

Theorem. (add_SNo_Lt2_cancel)

∀x y z, SNo x → SNo y → SNo z → x + y < x + z → y < z

Click to Load Proof

Theorem. (add_SNo_Le1_cancel)

∀x y z, SNo x → SNo y → SNo z → x + y ≤ z + y → x ≤ z

Click to Load Proof

Theorem. (add_SNo_assoc_4)

∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y + z + w = (x + y + z) + w

Click to Load Proof

Theorem. (add_SNo_com_3_0_1)

∀x y z, SNo x → SNo y → SNo z → x + y + z = y + x + z

Click to Load Proof

Theorem. (add_SNo_com_3b_1_2)

∀x y z, SNo x → SNo y → SNo z → (x + y) + z = (x + z) + y

Click to Load Proof

Theorem. (add_SNo_com_4_inner_mid)

∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y) + (z + w) = (x + z) + (y + w)

Click to Load Proof

Theorem. (add_SNo_rotate_3_1)

∀x y z, SNo x → SNo y → SNo z → x + y + z = z + x + y

Click to Load Proof

Theorem. (add_SNo_rotate_4_1)

∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y + z + w = w + x + y + z

Click to Load Proof

Theorem. (add_SNo_rotate_5_1)

∀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

Click to Load Proof

Theorem. (add_SNo_rotate_5_2)

∀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

Click to Load Proof

Theorem. (add_SNo_minus_SNo_prop2)

∀x y, SNo x → SNo y → x + - x + y = y

Click to Load Proof

Theorem. (add_SNo_minus_SNo_prop3)

∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y + z) + (- z + w) = x + y + w

Click to Load Proof

Theorem. (add_SNo_minus_SNo_prop5)

∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y + - z) + (z + w) = x + y + w

Click to Load Proof

Theorem. (add_SNo_minus_Lt1)

∀x y z, SNo x → SNo y → SNo z → x + - y < z → x < z + y

Click to Load Proof

Theorem. (add_SNo_minus_Lt2)

∀x y z, SNo x → SNo y → SNo z → z < x + - y → z + y < x

Click to Load Proof

Theorem. (add_SNo_minus_Lt1b)

∀x y z, SNo x → SNo y → SNo z → x < z + y → x + - y < z

Click to Load Proof

Theorem. (add_SNo_minus_Lt2b)

∀x y z, SNo x → SNo y → SNo z → z + y < x → z < x + - y

Click to Load Proof

Theorem. (add_SNo_minus_Lt1b3)

∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y < w + z → x + y + - z < w

Click to Load Proof

Theorem. (add_SNo_minus_Lt2b3)

∀x y z w, SNo x → SNo y → SNo z → SNo w → w + z < x + y → w < x + y + - z

Click to Load Proof

Theorem. (add_SNo_minus_Lt_lem)

∀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

Click to Load Proof

Theorem. (add_SNo_minus_Le2)

∀x y z, SNo x → SNo y → SNo z → z ≤ x + - y → z + y ≤ x

Click to Load Proof

Theorem. (add_SNo_minus_Le2b)

∀x y z, SNo x → SNo y → SNo z → z + y ≤ x → z ≤ x + - y

Click to Load Proof

Theorem. (add_SNo_Lt_subprop2)

∀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

Click to Load Proof

Theorem. (add_SNo_Lt_subprop3a)

∀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

Click to Load Proof

Theorem. (add_SNo_Lt_subprop3b)

∀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

Click to Load Proof

Theorem. (add_SNo_Lt_subprop3c)

∀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

Click to Load Proof

Theorem. (add_SNo_Lt_subprop3d)

∀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

Click to Load Proof

Theorem. (ordinal_ordsucc_SNo_eq)

∀α, ordinal α → ordsucc α = 1 + α

Click to Load Proof

Theorem. (add_SNo_3a_2b)

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

Click to Load Proof

Theorem. (add_SNo_1_ordsucc)

∀n ∈ ω, n + 1 = ordsucc n

Click to Load Proof

Theorem. (add_SNo_eps_Lt)

∀x, SNo x → ∀n ∈ ω, x < x + eps_ n

Click to Load Proof

Theorem. (add_SNo_eps_Lt')

∀x y, SNo x → SNo y → ∀n ∈ ω, x < y → x < y + eps_ n

Click to Load Proof

Theorem. (SNoLt_minus_pos)

∀x y, SNo x → SNo y → x < y → 0 < y + - x

Click to Load Proof

Theorem. (add_SNo_omega_In_cases)

∀m, ∀n ∈ ω, ∀k, nat_p k → m ∈ n + k → m ∈ n ∨ m + - n ∈ k

Click to Load Proof

Theorem. (add_SNo_Lt4)

∀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

Click to Load Proof

Theorem. (add_SNo_3_3_3_Lt1)

∀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

Click to Load Proof

Theorem. (add_SNo_3_2_3_Lt1)

∀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

Click to Load Proof

Theorem. (add_SNo_minus_Lt12b3)

∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x + y + v < w + u + z → x + y + - z < w + u + - v

Click to Load Proof

Theorem. (add_SNo_minus_Le1b)

∀x y z, SNo x → SNo y → SNo z → x ≤ z + y → x + - y ≤ z

Click to Load Proof

Theorem. (add_SNo_minus_Le1b3)

∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y ≤ w + z → x + y + - z ≤ w

Click to Load Proof

Theorem. (add_SNo_minus_Le12b3)

∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x + y + v ≤ w + u + z → x + y + - z ≤ w + u + - v

Click to Load Proof

End of Section SurrealAdd

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)

∀x, 0 ≤ x → abs_SNo x = x

Click to Load Proof

Theorem. (not_nonneg_abs_SNo)

∀x, ¬ (0 ≤ x) → abs_SNo x = - x

Click to Load Proof

Theorem. (pos_abs_SNo)

∀x, 0 < x → abs_SNo x = x

Click to Load Proof

Theorem. (neg_abs_SNo)

∀x, SNo x → x < 0 → abs_SNo x = - x

Click to Load Proof

Theorem. (SNo_abs_SNo)

∀x, SNo x → SNo (abs_SNo x)

Click to Load Proof

Theorem. (abs_SNo_minus)

∀x, SNo x → abs_SNo (- x) = abs_SNo x

Click to Load Proof

Theorem. (abs_SNo_dist_swap)

∀x y, SNo x → SNo y → abs_SNo (x + - y) = abs_SNo (y + - x)

Click to Load Proof

End of Section SurrealAbs

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.

Theorem. (mul_SNo_eq)

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

Click to Load Proof

Theorem. (mul_SNo_eq_2)

∀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

Click to Load Proof

Theorem. (mul_SNo_prop_1)

∀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

Click to Load Proof

Theorem. (SNo_mul_SNo)

∀x y, SNo x → SNo y → SNo (x * y)

Click to Load Proof

Theorem. (SNo_mul_SNo_lem)

∀x y u v, SNo x → SNo y → SNo u → SNo v → SNo (u * y + x * v + - (u * v))

Click to Load Proof

Theorem. (SNo_mul_SNo_3)

∀x y z, SNo x → SNo y → SNo z → SNo (x * y * z)

Click to Load Proof

Theorem. (mul_SNo_eq_3)

∀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

Click to Load Proof

Theorem. (mul_SNo_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

Click to Load Proof

Theorem. (mul_SNo_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

Click to Load Proof

Theorem. (mul_SNo_SNoL_interpolate)

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

Click to Load Proof

Theorem. (mul_SNo_SNoL_interpolate_impred)

∀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

Click to Load Proof

Theorem. (mul_SNo_SNoR_interpolate)

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

Click to Load Proof

Theorem. (mul_SNo_SNoR_interpolate_impred)

∀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

Click to Load Proof

Theorem. (mul_SNo_Subq_lem)

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

Click to Load Proof

Theorem. (mul_SNo_zeroR)

∀x, SNo x → x * 0 = 0

Click to Load Proof

Theorem. (mul_SNo_oneR)

∀x, SNo x → x * 1 = x

Click to Load Proof

Theorem. (mul_SNo_com)

∀x y, SNo x → SNo y → x * y = y * x

Click to Load Proof

Theorem. (mul_SNo_minus_distrL)

∀x y, SNo x → SNo y → (- x) * y = - x * y

Click to Load Proof

Theorem. (mul_SNo_minus_distrR)

∀x y, SNo x → SNo y → x * (- y) = - (x * y)

Click to Load Proof

Theorem. (mul_SNo_distrR)

∀x y z, SNo x → SNo y → SNo z → (x + y) * z = x * z + y * z

Click to Load Proof

Theorem. (mul_SNo_distrL)

∀x y z, SNo x → SNo y → SNo z → x * (y + z) = x * y + x * z

Click to Load Proof

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

Theorem. (mul_SNo_assoc_lem1)

∀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

Click to Load Proof

Theorem. (mul_SNo_assoc_lem2)

∀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

Click to Load Proof

End of Section mul_SNo_assoc_lems

Theorem. (mul_SNo_assoc)

∀x y z, SNo x → SNo y → SNo z → x * (y * z) = (x * y) * z

Click to Load Proof

Theorem. (mul_nat_mul_SNo)

∀n m ∈ ω, mul_nat n m = n * m

Click to Load Proof

Theorem. (mul_SNo_In_omega)

∀n m ∈ ω, n * m ∈ ω

Click to Load Proof

Theorem. (mul_SNo_zeroL)

∀x, SNo x → 0 * x = 0

Click to Load Proof

Theorem. (mul_SNo_oneL)

∀x, SNo x → 1 * x = x

Click to Load Proof

Theorem. (mul_SNo_rotate_3_1)

∀x y z, SNo x → SNo y → SNo z → x * y * z = z * x * y

Click to Load Proof

Theorem. (pos_mul_SNo_Lt)

∀x y z, SNo x → 0 < x → SNo y → SNo z → y < z → x * y < x * z

Click to Load Proof

Theorem. (nonneg_mul_SNo_Le)

∀x y z, SNo x → 0 ≤ x → SNo y → SNo z → y ≤ z → x * y ≤ x * z

Click to Load Proof

Theorem. (neg_mul_SNo_Lt)

∀x y z, SNo x → x < 0 → SNo y → SNo z → z < y → x * y < x * z

Click to Load Proof

Theorem. (pos_mul_SNo_Lt')

∀x y z, SNo x → SNo y → SNo z → 0 < z → x < y → x * z < y * z

Click to Load Proof

Theorem. (mul_SNo_Lt1_pos_Lt)

∀x y, SNo x → SNo y → x < 1 → 0 < y → x * y < y

Click to Load Proof

Theorem. (nonneg_mul_SNo_Le')

∀x y z, SNo x → SNo y → SNo z → 0 ≤ z → x ≤ y → x * z ≤ y * z

Click to Load Proof

Theorem. (mul_SNo_Le1_nonneg_Le)

∀x y, SNo x → SNo y → x ≤ 1 → 0 ≤ y → x * y ≤ y

Click to Load Proof

Theorem. (pos_mul_SNo_Lt2)

∀x y z w, SNo x → SNo y → SNo z → SNo w → 0 < x → 0 < y → x < z → y < w → x * y < z * w

Click to Load Proof

Theorem. (nonneg_mul_SNo_Le2)

∀x y z w, SNo x → SNo y → SNo z → SNo w → 0 ≤ x → 0 ≤ y → x ≤ z → y ≤ w → x * y ≤ z * w

Click to Load Proof

Theorem. (mul_SNo_pos_pos)

∀x y, SNo x → SNo y → 0 < x → 0 < y → 0 < x * y

Click to Load Proof

Theorem. (mul_SNo_pos_neg)

∀x y, SNo x → SNo y → 0 < x → y < 0 → x * y < 0

Click to Load Proof

Theorem. (mul_SNo_neg_pos)

∀x y, SNo x → SNo y → x < 0 → 0 < y → x * y < 0

Click to Load Proof

Theorem. (mul_SNo_neg_neg)

∀x y, SNo x → SNo y → x < 0 → y < 0 → 0 < x * y

Click to Load Proof

Theorem. (mul_SNo_nonneg_nonneg)

∀x y, SNo x → SNo y → 0 ≤ x → 0 ≤ y → 0 ≤ x * y

Click to Load Proof

Theorem. (mul_SNo_nonpos_pos)

∀x y, SNo x → SNo y → x ≤ 0 → 0 < y → x * y ≤ 0

Click to Load Proof

Theorem. (mul_SNo_nonpos_neg)

∀x y, SNo x → SNo y → x ≤ 0 → y < 0 → 0 ≤ x * y

Click to Load Proof

Theorem. (nonpos_mul_SNo_Le)

∀x y z, SNo x → x ≤ 0 → SNo y → SNo z → z ≤ y → x * y ≤ x * z

Click to Load Proof

Theorem. (SNo_zero_or_sqr_pos)

∀x, SNo x → x = 0 ∨ 0 < x * x

Click to Load Proof

Theorem. (SNo_pos_sqr_uniq)

∀x y, SNo x → SNo y → 0 < x → 0 < y → x * x = y * y → x = y

Click to Load Proof

Theorem. (SNo_nonneg_sqr_uniq)

∀x y, SNo x → SNo y → 0 ≤ x → 0 ≤ y → x * x = y * y → x = y

Click to Load Proof

Theorem. (SNo_foil)

∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y) * (z + w) = x * z + x * w + y * z + y * w

Click to Load Proof

Theorem. (mul_SNo_minus_minus)

∀x y, SNo x → SNo y → (- x) * (- y) = x * y

Click to Load Proof

Theorem. (mul_SNo_com_3_0_1)

∀x y z, SNo x → SNo y → SNo z → x * y * z = y * x * z

Click to Load Proof

Theorem. (mul_SNo_com_3b_1_2)

∀x y z, SNo x → SNo y → SNo z → (x * y) * z = (x * z) * y

Click to Load Proof

Theorem. (mul_SNo_com_4_inner_mid)

∀x y z w, SNo x → SNo y → SNo z → SNo w → (x * y) * (z * w) = (x * z) * (y * w)

Click to Load Proof

Theorem. (SNo_foil_mm)

∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + - y) * (z + - w) = x * z + - x * w + - y * z + y * w

Click to Load Proof

Theorem. (mul_SNo_nonzero_cancel)

∀x y z, SNo x → x ≠ 0 → SNo y → SNo z → x * y = x * z → y = z

Click to Load Proof

Theorem. (mul_SNoCutP_lem)

∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → SNoCutP ({w 0 * y + x * w 1 + - w 0 * w 1|w ∈ Lx ⨯ Ly} ∪ {z 0 * y + x * z 1 + - z 0 * z 1|z ∈ Rx ⨯ Ry}) ({w 0 * y + x * w 1 + - w 0 * w 1|w ∈ Lx ⨯ Ry} ∪ {z 0 * y + x * z 1 + - z 0 * z 1|z ∈ Rx ⨯ Ly}) ∧ x * y = SNoCut ({w 0 * y + x * w 1 + - w 0 * w 1|w ∈ Lx ⨯ Ly} ∪ {z 0 * y + x * z 1 + - z 0 * z 1|z ∈ Rx ⨯ Ry}) ({w 0 * y + x * w 1 + - w 0 * w 1|w ∈ Lx ⨯ Ry} ∪ {z 0 * y + x * z 1 + - z 0 * z 1|z ∈ Rx ⨯ Ly}) ∧ ∀q : prop, (∀LxLy' RxRy' LxRy' RxLy', (∀u ∈ LxLy', ∀p : prop, (∀w ∈ Lx, ∀w' ∈ Ly, SNo w → SNo w' → w < x → w' < y → u = w * y + x * w' + - w * w' → p) → p) → (∀w ∈ Lx, ∀w' ∈ Ly, w * y + x * w' + - w * w' ∈ LxLy') → (∀u ∈ RxRy', ∀p : prop, (∀z ∈ Rx, ∀z' ∈ Ry, SNo z → SNo z' → x < z → y < z' → u = z * y + x * z' + - z * z' → p) → p) → (∀z ∈ Rx, ∀z' ∈ Ry, z * y + x * z' + - z * z' ∈ RxRy') → (∀u ∈ LxRy', ∀p : prop, (∀w ∈ Lx, ∀z ∈ Ry, SNo w → SNo z → w < x → y < z → u = w * y + x * z + - w * z → p) → p) → (∀w ∈ Lx, ∀z ∈ Ry, w * y + x * z + - w * z ∈ LxRy') → (∀u ∈ RxLy', ∀p : prop, (∀z ∈ Rx, ∀w ∈ Ly, SNo z → SNo w → x < z → w < y → u = z * y + x * w + - z * w → p) → p) → (∀z ∈ Rx, ∀w ∈ Ly, z * y + x * w + - z * w ∈ RxLy') → SNoCutP (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') → x * y = SNoCut (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') → q) → q

Click to Load Proof

Theorem. (mul_SNoCut_abs)

∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀q : prop, (∀LxLy' RxRy' LxRy' RxLy', (∀u ∈ LxLy', ∀p : prop, (∀w ∈ Lx, ∀w' ∈ Ly, SNo w → SNo w' → w < x → w' < y → u = w * y + x * w' + - w * w' → p) → p) → (∀w ∈ Lx, ∀w' ∈ Ly, w * y + x * w' + - w * w' ∈ LxLy') → (∀u ∈ RxRy', ∀p : prop, (∀z ∈ Rx, ∀z' ∈ Ry, SNo z → SNo z' → x < z → y < z' → u = z * y + x * z' + - z * z' → p) → p) → (∀z ∈ Rx, ∀z' ∈ Ry, z * y + x * z' + - z * z' ∈ RxRy') → (∀u ∈ LxRy', ∀p : prop, (∀w ∈ Lx, ∀z ∈ Ry, SNo w → SNo z → w < x → y < z → u = w * y + x * z + - w * z → p) → p) → (∀w ∈ Lx, ∀z ∈ Ry, w * y + x * z + - w * z ∈ LxRy') → (∀u ∈ RxLy', ∀p : prop, (∀z ∈ Rx, ∀w ∈ Ly, SNo z → SNo w → x < z → w < y → u = z * y + x * w + - z * w → p) → p) → (∀z ∈ Rx, ∀w ∈ Ly, z * y + x * w + - z * w ∈ RxLy') → SNoCutP (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') → x * y = SNoCut (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') → q) → q

Click to Load Proof

Theorem. (mul_SNo_SNoCut_SNoL_interpolate)

∀Lx Rx Ly Ry, SNoCutP Lx Rx → SNoCutP Ly Ry → ∀x y, x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀u ∈ SNoL (x * y), (∃v ∈ Lx, ∃w ∈ Ly, u + v * w ≤ v * y + x * w) ∨ (∃v ∈ Rx, ∃w ∈ Ry, u + v * w ≤ v * y + x * w)

Click to Load Proof

Theorem. (mul_SNo_SNoCut_SNoL_interpolate_impred)

∀Lx Rx Ly Ry, SNoCutP Lx Rx → SNoCutP Ly Ry → ∀x y, x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀u ∈ SNoL (x * y), ∀p : prop, (∀v ∈ Lx, ∀w ∈ Ly, u + v * w ≤ v * y + x * w → p) → (∀v ∈ Rx, ∀w ∈ Ry, u + v * w ≤ v * y + x * w → p) → p

Click to Load Proof

Theorem. (mul_SNo_SNoCut_SNoR_interpolate)

∀Lx Rx Ly Ry, SNoCutP Lx Rx → SNoCutP Ly Ry → ∀x y, x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀u ∈ SNoR (x * y), (∃v ∈ Lx, ∃w ∈ Ry, v * y + x * w ≤ u + v * w) ∨ (∃v ∈ Rx, ∃w ∈ Ly, v * y + x * w ≤ u + v * w)

Click to Load Proof

Theorem. (mul_SNo_SNoCut_SNoR_interpolate_impred)

∀Lx Rx Ly Ry, SNoCutP Lx Rx → SNoCutP Ly Ry → ∀x y, x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀u ∈ SNoR (x * y), ∀p : prop, (∀v ∈ Lx, ∀w ∈ Ry, v * y + x * w ≤ u + v * w → p) → (∀v ∈ Rx, ∀w ∈ Ly, v * y + x * w ≤ u + v * w → p) → p

Click to Load Proof

Theorem. (nonpos_nonneg_0)

∀m n ∈ ω, m = - n → m = 0 ∧ n = 0

Click to Load Proof

Theorem. (mul_minus_SNo_distrR)

∀x y, SNo x → SNo y → x * (- y) = - (x * y)

Click to Load Proof

End of Section SurrealMul

Beginning of Section Int

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.

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

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

Definition. We define int to be ω ∪ {- n|n ∈ ω} of type set.

Theorem. (int_SNo_cases)

∀p : set → prop, (∀n ∈ ω, p n) → (∀n ∈ ω, p (- n)) → ∀x ∈ int, p x

Click to Load Proof

Theorem. (int_3_cases)

∀n ∈ int, ∀p : prop, (∀m ∈ ω, n = - ordsucc m → p) → (n = 0 → p) → (∀m ∈ ω, n = ordsucc m → p) → p

Click to Load Proof

Theorem. (int_SNo)

∀x ∈ int, SNo x

Click to Load Proof

Theorem. (Subq_omega_int)

ω ⊆ int

Click to Load Proof

Theorem. (int_minus_SNo_omega)

∀n ∈ ω, - n ∈ int

Click to Load Proof

Theorem. (int_add_SNo_lem)

∀n ∈ ω, ∀m, nat_p m → - n + m ∈ int

Click to Load Proof

Theorem. (int_add_SNo)

∀x y ∈ int, x + y ∈ int

Click to Load Proof

Theorem. (int_minus_SNo)

∀x ∈ int, - x ∈ int

Click to Load Proof

Theorem. (int_mul_SNo)

∀x y ∈ int, x * y ∈ int

Click to Load Proof

Theorem. (nonneg_int_nat_p)

∀n ∈ int, 0 ≤ n → nat_p n

Click to Load Proof

End of Section Int

Beginning of Section BezoutAndGCD

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

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

Theorem. (quotient_remainder_nat)

∀n ∈ ω ∖ {0}, ∀m, nat_p m → ∃q ∈ ω, ∃r ∈ n, m = q * n + r

Click to Load Proof

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.

Theorem. (mul_SNo_nonpos_nonneg)

∀x y, SNo x → SNo y → x ≤ 0 → 0 ≤ y → x * y ≤ 0

Click to Load Proof

Theorem. (ordinal_0_In_ordsucc)

∀α, ordinal α → 0 ∈ ordsucc α

Click to Load Proof

Theorem. (ordinal_ordsucc_pos)

∀α, ordinal α → 0 < ordsucc α

Click to Load Proof

Theorem. (quotient_remainder_int)

∀n ∈ ω ∖ {0}, ∀m ∈ int, ∃q ∈ int, ∃r ∈ n, m = q * n + r

Click to Load Proof

Definition. We define divides_int to be λm n ⇒ m ∈ int ∧ n ∈ int ∧ ∃k ∈ int, m * k = n of type set → set → prop.

Theorem. (divides_int_ref)

∀n ∈ int, divides_int n n

Click to Load Proof

Theorem. (divides_int_0)

∀n ∈ int, divides_int n 0

Click to Load Proof

Theorem. (divides_int_add_SNo)

∀m n k, divides_int m n → divides_int m k → divides_int m (n + k)

Click to Load Proof

Theorem. (divides_int_mul_SNo)

∀m n m' n', divides_int m m' → divides_int n n' → divides_int (m * n) (m' * n')

Click to Load Proof

Theorem. (divides_nat_divides_int)

∀m n, divides_nat m n → divides_int m n

Click to Load Proof

Theorem. (divides_int_divides_nat)

∀m n ∈ ω, divides_int m n → divides_nat m n

Click to Load Proof

Theorem. (divides_int_minus_SNo)

∀m n, divides_int m n → divides_int m (- n)

Click to Load Proof

Theorem. (divides_int_mul_SNo_L)

∀m n, ∀k ∈ int, divides_int m n → divides_int m (n * k)

Click to Load Proof

Theorem. (divides_int_mul_SNo_R)

∀m n, ∀k ∈ int, divides_int m n → divides_int m (k * n)

Click to Load Proof

Theorem. (divides_int_1)

∀n ∈ int, divides_int 1 n

Click to Load Proof

Theorem. (divides_int_pos_Le)

∀m n, divides_int m n → 0 < n → m ≤ n

Click to Load Proof

Definition. We define gcd_reln to be λm n d ⇒ divides_int d m ∧ divides_int d n ∧ ∀d', divides_int d' m → divides_int d' n → d' ≤ d of type set → set → set → prop.

Theorem. (gcd_reln_uniq)

∀a b c d, gcd_reln a b c → gcd_reln a b d → c = d

Click to Load Proof

Definition. We define int_lin_comb to be λa b c ⇒ a ∈ int ∧ b ∈ int ∧ c ∈ int ∧ ∃m n ∈ int, m * a + n * b = c of type set → set → set → prop.

Theorem. (int_lin_comb_I)

∀a b c ∈ int, (∃m n ∈ int, m * a + n * b = c) → int_lin_comb a b c

Click to Load Proof

Theorem. (int_lin_comb_E)

∀a b c, int_lin_comb a b c → ∀p : prop, (a ∈ int → b ∈ int → c ∈ int → ∀m n ∈ int, m * a + n * b = c → p) → p

Click to Load Proof

Theorem. (int_lin_comb_E1)

∀a b c, int_lin_comb a b c → a ∈ int

Click to Load Proof

Theorem. (int_lin_comb_E2)

∀a b c, int_lin_comb a b c → b ∈ int

Click to Load Proof

Theorem. (int_lin_comb_E3)

∀a b c, int_lin_comb a b c → c ∈ int

Click to Load Proof

Theorem. (int_lin_comb_E4)

∀a b c, int_lin_comb a b c → ∀p : prop, (∀m n ∈ int, m * a + n * b = c → p) → p

Click to Load Proof

Theorem. (least_pos_int_lin_comb_ex)

∀a b ∈ int, ¬ (a = 0 ∧ b = 0) → ∃c, int_lin_comb a b c ∧ 0 < c ∧ ∀c', int_lin_comb a b c' → 0 < c' → c ≤ c'

Click to Load Proof

Theorem. (int_lin_comb_sym)

∀a b d, int_lin_comb a b d → int_lin_comb b a d

Click to Load Proof

Theorem. (least_pos_int_lin_comb_divides_int)

∀a b d, int_lin_comb a b d → 0 < d → (∀c, int_lin_comb a b c → 0 < c → d ≤ c) → divides_int d a

Click to Load Proof

Theorem. (least_pos_int_lin_comb_gcd)

∀a b d, int_lin_comb a b d → 0 < d → (∀c, int_lin_comb a b c → 0 < c → d ≤ c) → gcd_reln a b d

Click to Load Proof

Theorem. (BezoutThm)

∀a b ∈ int, ¬ (a = 0 ∧ b = 0) → ∀d, gcd_reln a b d ↔ int_lin_comb a b d ∧ 0 < d ∧ ∀d', int_lin_comb a b d' → 0 < d' → d ≤ d'

Click to Load Proof

Theorem. (gcd_id)

∀m ∈ ω ∖ {0}, gcd_reln m m m

Click to Load Proof

Theorem. (gcd_0)

∀m ∈ ω ∖ {0}, gcd_reln 0 m m

Click to Load Proof

Theorem. (gcd_sym)

∀m n d, gcd_reln m n d → gcd_reln n m d

Click to Load Proof

Theorem. (gcd_minus)

∀m n d, gcd_reln m n d → gcd_reln m (- n) d

Click to Load Proof

Theorem. (euclidean_algorithm_prop_1)

∀m n d, n ∈ int → gcd_reln m (n + - m) d → gcd_reln m n d

Click to Load Proof

Theorem. (euclidean_algorithm)

(∀m ∈ ω ∖ {0}, gcd_reln m m m) ∧ (∀m ∈ ω ∖ {0}, gcd_reln 0 m m) ∧ (∀m ∈ ω ∖ {0}, gcd_reln m 0 m) ∧ (∀m n ∈ ω, m < n → ∀d, gcd_reln m (n + - m) d → gcd_reln m n d) ∧ (∀m n ∈ ω, n < m → ∀d, gcd_reln n m d → gcd_reln m n d) ∧ (∀m ∈ ω, ∀n ∈ int, n < 0 → ∀d, gcd_reln m (- n) d → gcd_reln m n d) ∧ (∀m n ∈ int, m < 0 → ∀d, gcd_reln (- m) n d → gcd_reln m n d)

Click to Load Proof

Theorem. (Euclid_lemma)

∀p, prime_nat p → ∀a b ∈ int, divides_int p (a * b) → divides_int p a ∨ divides_int p b

Click to Load Proof

End of Section BezoutAndGCD

Beginning of Section PrimeFactorization

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.

Theorem. (prime_not_divides_int_1)

∀p, prime_nat p → ¬ divides_int p 1

Click to Load Proof

Definition. We define Pi_SNo to be λf n ⇒ nat_primrec 1 (λi r ⇒ r * f i) n of type (set → set) → set → set.

Theorem. (Pi_SNo_0)

∀f : set → set, Pi_SNo f 0 = 1

Click to Load Proof

Theorem. (Pi_SNo_S)

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

Click to Load Proof

Theorem. (Pi_SNo_In_omega)

∀f : set → set, ∀n, nat_p n → (∀i ∈ n, f i ∈ ω) → Pi_SNo f n ∈ ω

Click to Load Proof

Theorem. (Pi_SNo_In_int)

∀f : set → set, ∀n, nat_p n → (∀i ∈ n, f i ∈ int) → Pi_SNo f n ∈ int

Click to Load Proof

Theorem. (divides_int_prime_nat_eq)

∀p q, prime_nat p → prime_nat q → divides_int p q → p = q

Click to Load Proof

Theorem. (Euclid_lemma_Pi_SNo)

∀f : set → set, ∀p, prime_nat p → ∀n, nat_p n → (∀i ∈ n, f i ∈ int) → divides_int p (Pi_SNo f n) → ∃i ∈ n, divides_int p (f i)

Click to Load Proof

Theorem. (divides_nat_mul_SNo_R)

∀m n ∈ ω, divides_nat m (m * n)

Click to Load Proof

Theorem. (divides_nat_mul_SNo_L)

∀m n ∈ ω, divides_nat n (m * n)

Click to Load Proof

Theorem. (Pi_SNo_divides)

∀f : set → set, ∀n, nat_p n → (∀i ∈ n, f i ∈ ω) → (∀i ∈ n, divides_nat (f i) (Pi_SNo f n))

Click to Load Proof

Definition. We define nonincrfinseq to be λA n f ⇒ ∀i ∈ n, A (f i) ∧ ∀j ∈ i, f i ≤ f j of type (set → prop) → set → (set → set) → prop.

Theorem. (Pi_SNo_eq)

∀f g : set → set, ∀m, nat_p m → (∀i ∈ m, f i = g i) → Pi_SNo f m = Pi_SNo g m

Click to Load Proof

Theorem. (prime_factorization_ex_uniq)

∀n, nat_p n → 0 ∈ n → ∃k ∈ ω, ∃f : set → set, nonincrfinseq prime_nat k f ∧ Pi_SNo f k = n ∧ ∀k' ∈ ω, ∀f' : set → set, nonincrfinseq prime_nat k' f' → Pi_SNo f' k' = n → k' = k ∧ ∀i ∈ k, f' i = f i

Click to Load Proof

End of Section PrimeFactorization

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.

Theorem. (exp_SNo_nat_0)

∀x, SNo x → x ^ 0 = 1

Click to Load Proof

Theorem. (exp_SNo_nat_S)

∀x, SNo x → ∀n, nat_p n → x ^ (ordsucc n) = x * x ^ n

Click to Load Proof

Theorem. (exp_SNo_nat_1)

∀x, SNo x → x ^ 1 = x

Click to Load Proof

Theorem. (SNo_exp_SNo_nat)

∀x, SNo x → ∀n, nat_p n → SNo (x ^ n)

Click to Load Proof

Theorem. (nat_exp_SNo_nat)

∀x, nat_p x → ∀n, nat_p n → nat_p (x ^ n)

Click to Load Proof

Theorem. (eps_ordsucc_half_add)

∀n, nat_p n → eps_ (ordsucc n) + eps_ (ordsucc n) = eps_ n

Click to Load Proof

Theorem. (eps_1_half_eq1)

eps_ 1 + eps_ 1 = 1

Click to Load Proof

Theorem. (eps_1_half_eq2)

2 * eps_ 1 = 1

Click to Load Proof

Theorem. (double_eps_1)

∀x y z, SNo x → SNo y → SNo z → x + x = y + z → x = eps_ 1 * (y + z)

Click to Load Proof

Theorem. (exp_SNo_1_bd)

∀x, SNo x → 1 ≤ x → ∀n, nat_p n → 1 ≤ x ^ n

Click to Load Proof

Theorem. (exp_SNo_2_bd)

∀n, nat_p n → n < 2 ^ n

Click to Load Proof

Theorem. (mul_SNo_eps_power_2)

∀n, nat_p n → eps_ n * 2 ^ n = 1

Click to Load Proof

Theorem. (eps_bd_1)

∀n ∈ ω, eps_ n ≤ 1

Click to Load Proof

Theorem. (mul_SNo_eps_power_2')

∀n, nat_p n → 2 ^ n * eps_ n = 1

Click to Load Proof

Theorem. (exp_SNo_nat_mul_add)

∀x, SNo x → ∀m, nat_p m → ∀n, nat_p n → x ^ m * x ^ n = x ^ (m + n)

Click to Load Proof

Theorem. (exp_SNo_nat_mul_add')

∀x, SNo x → ∀m n ∈ ω, x ^ m * x ^ n = x ^ (m + n)

Click to Load Proof

Theorem. (exp_SNo_nat_pos)

∀x, SNo x → 0 < x → ∀n, nat_p n → 0 < x ^ n

Click to Load Proof

Theorem. (mul_SNo_eps_eps_add_SNo)

∀m n ∈ ω, eps_ m * eps_ n = eps_ (m + n)

Click to Load Proof

Theorem. (SNoS_omega_Lev_equip)

∀n, nat_p n → equip {x ∈ SNoS_ ω|SNoLev x = n} (2 ^ n)

Click to Load Proof

Theorem. (SNoS_finite)

∀n ∈ ω, finite (SNoS_ n)

Click to Load Proof

Theorem. (SNoS_omega_SNoL_finite)

∀x ∈ SNoS_ ω, finite (SNoL x)

Click to Load Proof

Theorem. (SNoS_omega_SNoR_finite)

∀x ∈ SNoS_ ω, finite (SNoR x)

Click to Load Proof

End of Section SurrealExp

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)

∀X y, (∀x ∈ X, SNo x) → SNo_max_of X y → SNo_min_of {- x|x ∈ X} (- y)

Click to Load Proof

Theorem. (minus_SNo_max_min')

∀X y, (∀x ∈ X, SNo x) → SNo_max_of {- x|x ∈ X} y → SNo_min_of X (- y)

Click to Load Proof

Theorem. (minus_SNo_min_max)

∀X y, (∀x ∈ X, SNo x) → SNo_min_of X y → SNo_max_of {- x|x ∈ X} (- y)

Click to Load Proof

Theorem. (double_SNo_max_1)

∀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

Click to Load Proof

Theorem. (double_SNo_min_1)

∀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

Click to Load Proof

Theorem. (finite_max_exists)

∀X, (∀x ∈ X, SNo x) → finite X → X ≠ 0 → ∃x, SNo_max_of X x

Click to Load Proof

Theorem. (finite_min_exists)

∀X, (∀x ∈ X, SNo x) → finite X → X ≠ 0 → ∃x, SNo_min_of X x

Click to Load Proof

Theorem. (SNoS_omega_SNoL_max_exists)

∀x ∈ SNoS_ ω, SNoL x = 0 ∨ ∃y, SNo_max_of (SNoL x) y

Click to Load Proof

Theorem. (SNoS_omega_SNoR_min_exists)

∀x ∈ SNoS_ ω, SNoR x = 0 ∨ ∃y, SNo_min_of (SNoR x) y

Click to Load Proof

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)

∀k ∈ ω, ∀n, nat_p n → eps_ k * n ∈ SNoS_ ω

Click to Load Proof

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)

∀x, diadic_rational_p x → x ∈ SNoS_ ω

Click to Load Proof

Theorem. (int_diadic_rational_p)

∀m ∈ int, diadic_rational_p m

Click to Load Proof

Theorem. (omega_diadic_rational_p)

∀m ∈ ω, diadic_rational_p m

Click to Load Proof

Theorem. (eps_diadic_rational_p)

∀k ∈ ω, diadic_rational_p (eps_ k)

Click to Load Proof

Theorem. (minus_SNo_diadic_rational_p)

∀x, diadic_rational_p x → diadic_rational_p (- x)

Click to Load Proof

Theorem. (mul_SNo_diadic_rational_p)

∀x y, diadic_rational_p x → diadic_rational_p y → diadic_rational_p (x * y)

Click to Load Proof

Theorem. (add_SNo_diadic_rational_p)

∀x y, diadic_rational_p x → diadic_rational_p y → diadic_rational_p (x + y)

Click to Load Proof

Theorem. (SNoS_omega_diadic_rational_p_lem)

∀n, nat_p n → ∀x, SNo x → SNoLev x = n → diadic_rational_p x

Click to Load Proof

Theorem. (SNoS_omega_diadic_rational_p)

∀x ∈ SNoS_ ω, diadic_rational_p x

Click to Load Proof

Theorem. (mul_SNo_SNoS_omega)

∀x y ∈ SNoS_ ω, x * y ∈ SNoS_ ω

Click to Load Proof

End of Section DiadicRationals

Beginning of Section SurrealDiv

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.

Definition. We define SNoL_pos to be λx ⇒ {w ∈ SNoL x|0 < w} of type set → set.

Theorem. (SNo_recip_pos_pos)

∀x xi, SNo x → SNo xi → 0 < x → x * xi = 1 → 0 < xi

Click to Load Proof

Theorem. (SNo_recip_lem1)

∀x x' x'i y y', SNo x → 0 < x → x' ∈ SNoL_pos x → SNo x'i → x' * x'i = 1 → SNo y → x * y < 1 → SNo y' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i → 1 < x * y'

Click to Load Proof

Theorem. (SNo_recip_lem2)

∀x x' x'i y y', SNo x → 0 < x → x' ∈ SNoL_pos x → SNo x'i → x' * x'i = 1 → SNo y → 1 < x * y → SNo y' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i → x * y' < 1

Click to Load Proof

Theorem. (SNo_recip_lem3)

∀x x' x'i y y', SNo x → 0 < x → x' ∈ SNoR x → SNo x'i → x' * x'i = 1 → SNo y → x * y < 1 → SNo y' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i → x * y' < 1

Click to Load Proof

Theorem. (SNo_recip_lem4)

∀x x' x'i y y', SNo x → 0 < x → x' ∈ SNoR x → SNo x'i → x' * x'i = 1 → SNo y → 1 < x * y → SNo y' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i → 1 < x * y'

Click to Load Proof

Definition. We define SNo_recipauxset to be λY x X g ⇒ ⋃_{y ∈ Y}{(1 + (x' + - x) * y) * g x'|x' ∈ X} of type set → set → set → (set → set) → set.

Theorem. (SNo_recipauxset_I)

∀Y x X, ∀g : set → set, ∀y ∈ Y, ∀x' ∈ X, (1 + (x' + - x) * y) * g x' ∈ SNo_recipauxset Y x X g

Click to Load Proof

Theorem. (SNo_recipauxset_E)

∀Y x X, ∀g : set → set, ∀z ∈ SNo_recipauxset Y x X g, ∀p : prop, (∀y ∈ Y, ∀x' ∈ X, z = (1 + (x' + - x) * y) * g x' → p) → p

Click to Load Proof

Theorem. (SNo_recipauxset_ext)

∀Y x X, ∀g h : set → set, (∀x' ∈ X, g x' = h x') → SNo_recipauxset Y x X g = SNo_recipauxset Y x X h

Click to Load Proof

Definition. We define SNo_recipaux to be λx g ⇒ nat_primrec ({0},0) (λk p ⇒ (p 0 ∪ SNo_recipauxset (p 0) x (SNoR x) g ∪ SNo_recipauxset (p 1) x (SNoL_pos x) g,p 1 ∪ SNo_recipauxset (p 0) x (SNoL_pos x) g ∪ SNo_recipauxset (p 1) x (SNoR x) g)) of type set → (set → set) → set → set.

Theorem. (SNo_recipaux_0)

∀x, ∀g : set → set, SNo_recipaux x g 0 = ({0},0)

Click to Load Proof

Theorem. (SNo_recipaux_S)

∀x, ∀g : set → set, ∀n, nat_p n → SNo_recipaux x g (ordsucc n) = (SNo_recipaux x g n 0 ∪ SNo_recipauxset (SNo_recipaux x g n 0) x (SNoR x) g ∪ SNo_recipauxset (SNo_recipaux x g n 1) x (SNoL_pos x) g,SNo_recipaux x g n 1 ∪ SNo_recipauxset (SNo_recipaux x g n 0) x (SNoL_pos x) g ∪ SNo_recipauxset (SNo_recipaux x g n 1) x (SNoR x) g)

Click to Load Proof

Theorem. (SNo_recipaux_lem1)

∀x, SNo x → 0 < x → ∀g : set → set, (∀x' ∈ SNoS_ (SNoLev x), 0 < x' → SNo (g x') ∧ x' * g x' = 1) → ∀k, nat_p k → (∀y ∈ SNo_recipaux x g k 0, SNo y ∧ x * y < 1) ∧ (∀y ∈ SNo_recipaux x g k 1, SNo y ∧ 1 < x * y)

Click to Load Proof

Theorem. (SNo_recipaux_lem2)

∀x, SNo x → 0 < x → ∀g : set → set, (∀x' ∈ SNoS_ (SNoLev x), 0 < x' → SNo (g x') ∧ x' * g x' = 1) → SNoCutP (⋃_{k ∈ ω}SNo_recipaux x g k 0) (⋃_{k ∈ ω}SNo_recipaux x g k 1)

Click to Load Proof

Theorem. (SNo_recipaux_ext)

∀x, SNo x → ∀g h : set → set, (∀x' ∈ SNoS_ (SNoLev x), g x' = h x') → ∀k, nat_p k → SNo_recipaux x g k = SNo_recipaux x h k

Click to Load Proof

Beginning of Section recip_SNo_pos

Let G : set → (set → set) → set ≝ λx g ⇒ SNoCut (⋃_{k ∈ ω}SNo_recipaux x g k 0) (⋃_{k ∈ ω}SNo_recipaux x g k 1)

Definition. We define recip_SNo_pos to be SNo_rec_i G of type set → set.

Theorem. (recip_SNo_pos_eq)

∀x, SNo x → recip_SNo_pos x = G x recip_SNo_pos

Click to Load Proof

Theorem. (recip_SNo_pos_prop1)

∀x, SNo x → 0 < x → SNo (recip_SNo_pos x) ∧ x * recip_SNo_pos x = 1

Click to Load Proof

Theorem. (SNo_recip_SNo_pos)

∀x, SNo x → 0 < x → SNo (recip_SNo_pos x)

Click to Load Proof

Theorem. (recip_SNo_pos_invR)

∀x, SNo x → 0 < x → x * recip_SNo_pos x = 1

Click to Load Proof

Theorem. (recip_SNo_pos_is_pos)

∀x, SNo x → 0 < x → 0 < recip_SNo_pos x

Click to Load Proof

Theorem. (recip_SNo_pos_invol)

∀x, SNo x → 0 < x → recip_SNo_pos (recip_SNo_pos x) = x

Click to Load Proof

Theorem. (recip_SNo_pos_eps_)

∀n, nat_p n → recip_SNo_pos (eps_ n) = 2 ^ n

Click to Load Proof

Theorem. (recip_SNo_pos_pow_2)

∀n, nat_p n → recip_SNo_pos (2 ^ n) = eps_ n

Click to Load Proof

Theorem. (recip_SNo_pos_2)

recip_SNo_pos 2 = eps_ 1

Click to Load Proof

End of Section recip_SNo_pos

Definition. We define recip_SNo to be λx ⇒ if 0 < x then recip_SNo_pos x else if x < 0 then - recip_SNo_pos (- x) else 0 of type set → set.

Theorem. (recip_SNo_poscase)

∀x, 0 < x → recip_SNo x = recip_SNo_pos x

Click to Load Proof

Theorem. (recip_SNo_negcase)

∀x, SNo x → x < 0 → recip_SNo x = - recip_SNo_pos (- x)

Click to Load Proof

Theorem. (recip_SNo_0)

recip_SNo 0 = 0

Click to Load Proof

Theorem. (SNo_recip_SNo)

∀x, SNo x → SNo (recip_SNo x)

Click to Load Proof

Theorem. (recip_SNo_invR)

∀x, SNo x → x ≠ 0 → x * recip_SNo x = 1

Click to Load Proof

Theorem. (recip_SNo_invL)

∀x, SNo x → x ≠ 0 → recip_SNo x * x = 1

Click to Load Proof

Theorem. (mul_SNo_nonzero_cancel_L)

∀x y z, SNo x → x ≠ 0 → SNo y → SNo z → x * y = x * z → y = z

Click to Load Proof

Theorem. (recip_SNo_pow_2)

∀n, nat_p n → recip_SNo (2 ^ n) = eps_ n

Click to Load Proof

Theorem. (recip_SNo_of_pos_is_pos)

∀x, SNo x → 0 < x → 0 < recip_SNo x

Click to Load Proof

Definition. We define div_SNo to be λx y ⇒ x * recip_SNo y of type set → set → set.

Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.

Theorem. (SNo_div_SNo)

∀x y, SNo x → SNo y → SNo (x :/: y)

Click to Load Proof

Theorem. (div_SNo_0_num)

∀x, SNo x → 0 :/: x = 0

Click to Load Proof

Theorem. (div_SNo_0_denum)

∀x, SNo x → x :/: 0 = 0

Click to Load Proof

Theorem. (mul_div_SNo_invL)

∀x y, SNo x → SNo y → y ≠ 0 → (x :/: y) * y = x

Click to Load Proof

Theorem. (mul_div_SNo_invR)

∀x y, SNo x → SNo y → y ≠ 0 → y * (x :/: y) = x

Click to Load Proof

Theorem. (mul_div_SNo_R)

∀x y z, SNo x → SNo y → SNo z → (x :/: y) * z = (x * z) :/: y

Click to Load Proof

Theorem. (mul_div_SNo_L)

∀x y z, SNo x → SNo y → SNo z → z * (x :/: y) = (z * x) :/: y

Click to Load Proof

Theorem. (div_mul_SNo_invL)

∀x y, SNo x → SNo y → y ≠ 0 → (x * y) :/: y = x

Click to Load Proof

Theorem. (div_div_SNo)

∀x y z, SNo x → SNo y → SNo z → (x :/: y) :/: z = x :/: (y * z)

Click to Load Proof

Theorem. (mul_div_SNo_both)

∀x y z w, SNo x → SNo y → SNo z → SNo w → (x :/: y) * (z :/: w) = (x * z) :/: (y * w)

Click to Load Proof

Theorem. (recip_SNo_pos_pos)

∀x, SNo x → 0 < x → 0 < recip_SNo_pos x

Click to Load Proof

Theorem. (div_SNo_pos_pos)

∀x y, SNo x → SNo y → 0 < x → 0 < y → 0 < x :/: y

Click to Load Proof

Theorem. (div_SNo_neg_pos)

∀x y, SNo x → SNo y → x < 0 → 0 < y → x :/: y < 0

Click to Load Proof

Theorem. (div_SNo_pos_LtL)

∀x y z, SNo x → SNo y → SNo z → 0 < y → x < z * y → x :/: y < z

Click to Load Proof

Theorem. (div_SNo_pos_LtR)

∀x y z, SNo x → SNo y → SNo z → 0 < y → z * y < x → z < x :/: y

Click to Load Proof

Theorem. (div_SNo_pos_LtL')

∀x y z, SNo x → SNo y → SNo z → 0 < y → x :/: y < z → x < z * y

Click to Load Proof

Theorem. (div_SNo_pos_LtR')

∀x y z, SNo x → SNo y → SNo z → 0 < y → z < x :/: y → z * y < x

Click to Load Proof

Theorem. (mul_div_SNo_nonzero_eq)

∀x y z, SNo x → SNo y → SNo z → y ≠ 0 → x = y * z → x :/: y = z

Click to Load Proof

End of Section SurrealDiv

Beginning of Section Reals

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 353 and no associativity corresponding to applying term div_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.

Theorem. (SNoS_omega_drat_intvl)

∀x ∈ SNoS_ ω, ∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k

Click to Load Proof

Theorem. (SNoS_ordsucc_omega_bdd_above)

∀x ∈ SNoS_ (ordsucc ω), x < ω → ∃N ∈ ω, x < N

Click to Load Proof

Theorem. (SNoS_ordsucc_omega_bdd_below)

∀x ∈ SNoS_ (ordsucc ω), - ω < x → ∃N ∈ ω, - N < x

Click to Load Proof

Theorem. (SNoS_ordsucc_omega_bdd_drat_intvl)

∀x ∈ SNoS_ (ordsucc ω), - ω < x → x < ω → ∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k

Click to Load Proof

Definition. We define real to be {x ∈ SNoS_ (ordsucc ω)|x ≠ ω ∧ x ≠ - ω ∧ (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x)} of type set.

Theorem. (real_I)

∀x ∈ SNoS_ (ordsucc ω), x ≠ ω → x ≠ - ω → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → x ∈ real

Click to Load Proof

Theorem. (real_E)

∀x ∈ real, ∀p : prop, (SNo x → SNoLev x ∈ ordsucc ω → x ∈ SNoS_ (ordsucc ω) → - ω < x → x < ω → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → p) → p

Click to Load Proof

Theorem. (real_SNo)

∀x ∈ real, SNo x

Click to Load Proof

Theorem. (real_SNoS_omega_prop)

∀x ∈ real, ∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x

Click to Load Proof

Theorem. (SNoS_omega_real)

SNoS_ ω ⊆ real

Click to Load Proof

Theorem. (real_0)

0 ∈ real

Click to Load Proof

Theorem. (real_1)

1 ∈ real

Click to Load Proof

Theorem. (SNoLev_In_real_SNoS_omega)

∀x ∈ real, ∀w, SNo w → SNoLev w ∈ SNoLev x → w ∈ SNoS_ ω

Click to Load Proof

Theorem. (real_SNoCut_SNoS_omega)

∀L R ⊆ SNoS_ ω, SNoCutP L R → L ≠ 0 → R ≠ 0 → (∀w ∈ L, ∃w' ∈ L, w < w') → (∀z ∈ R, ∃z' ∈ R, z' < z) → SNoCut L R ∈ real

Click to Load Proof

Theorem. (real_SNoCut)

∀L R ⊆ real, SNoCutP L R → L ≠ 0 → R ≠ 0 → (∀w ∈ L, ∃w' ∈ L, w < w') → (∀z ∈ R, ∃z' ∈ R, z' < z) → SNoCut L R ∈ real

Click to Load Proof

Theorem. (minus_SNo_prereal_1)

∀x, SNo x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - - x) < eps_ k) → q = - x)

Click to Load Proof

Theorem. (minus_SNo_prereal_2)

∀x, SNo x → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < - x ∧ - x < q + eps_ k)

Click to Load Proof

Theorem. (SNo_prereal_incr_lower_pos)

∀x, SNo x → 0 < x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → ∀k ∈ ω, ∀p : prop, (∀q ∈ SNoS_ ω, 0 < q → q < x → x < q + eps_ k → p) → p

Click to Load Proof

Theorem. (real_minus_SNo)

∀x ∈ real, - x ∈ real

Click to Load Proof

Theorem. (SNo_prereal_incr_lower_approx)

∀x, SNo x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → ∃f ∈ SNoS_ ω^ω, ∀n ∈ ω, f n < x ∧ x < f n + eps_ n ∧ ∀i ∈ n, f i < f n

Click to Load Proof

Theorem. (SNo_prereal_decr_upper_approx)

∀x, SNo x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → ∃g ∈ SNoS_ ω^ω, ∀n ∈ ω, g n + - eps_ n < x ∧ x < g n ∧ ∀i ∈ n, g n < g i

Click to Load Proof

Theorem. (SNoCutP_SNoCut_lim)

∀lambda, ordinal lambda → (∀α ∈ lambda, ordsucc α ∈ lambda) → ∀L R ⊆ SNoS_ lambda, SNoCutP L R → SNoLev (SNoCut L R) ∈ ordsucc lambda

Click to Load Proof

Theorem. (SNoCutP_SNoCut_omega)

∀L R ⊆ SNoS_ ω, SNoCutP L R → SNoLev (SNoCut L R) ∈ ordsucc ω

Click to Load Proof

Theorem. (SNo_approx_real_lem)

∀f g ∈ SNoS_ ω^ω, (∀n m ∈ ω, f n < g m) → ∀p : prop, (SNoCutP {f n|n ∈ ω} {g n|n ∈ ω} → SNo (SNoCut {f n|n ∈ ω} {g n|n ∈ ω}) → SNoLev (SNoCut {f n|n ∈ ω} {g n|n ∈ ω}) ∈ ordsucc ω → SNoCut {f n|n ∈ ω} {g n|n ∈ ω} ∈ SNoS_ (ordsucc ω) → (∀n ∈ ω, f n < SNoCut {f n|n ∈ ω} {g n|n ∈ ω}) → (∀n ∈ ω, SNoCut {f n|n ∈ ω} {g n|n ∈ ω} < g n) → p) → p

Click to Load Proof

Theorem. (SNo_approx_real)

∀x, SNo x → ∀f g ∈ SNoS_ ω^ω, (∀n ∈ ω, f n < x) → (∀n ∈ ω, x < f n + eps_ n) → (∀n ∈ ω, ∀i ∈ n, f i < f n) → (∀n ∈ ω, x < g n) → (∀n ∈ ω, ∀i ∈ n, g n < g i) → x = SNoCut {f n|n ∈ ω} {g n|n ∈ ω} → x ∈ real

Click to Load Proof

Theorem. (SNo_approx_real_rep)

∀x ∈ real, ∀p : prop, (∀f g ∈ SNoS_ ω^ω, (∀n ∈ ω, f n < x) → (∀n ∈ ω, x < f n + eps_ n) → (∀n ∈ ω, ∀i ∈ n, f i < f n) → (∀n ∈ ω, g n + - eps_ n < x) → (∀n ∈ ω, x < g n) → (∀n ∈ ω, ∀i ∈ n, g n < g i) → SNoCutP {f n|n ∈ ω} {g n|n ∈ ω} → x = SNoCut {f n|n ∈ ω} {g n|n ∈ ω} → p) → p

Click to Load Proof

Theorem. (real_add_SNo)

∀x y ∈ real, x + y ∈ real

Click to Load Proof

Theorem. (SNoS_ordsucc_omega_bdd_eps_pos)

∀x ∈ SNoS_ (ordsucc ω), 0 < x → x < ω → ∃N ∈ ω, eps_ N * x < 1

Click to Load Proof

Theorem. (real_mul_SNo_pos)

∀x y ∈ real, 0 < x → 0 < y → x * y ∈ real

Click to Load Proof

Theorem. (real_mul_SNo)

∀x y ∈ real, x * y ∈ real

Click to Load Proof

Theorem. (nonneg_real_nat_interval)

∀x ∈ real, 0 ≤ x → ∃n ∈ ω, n ≤ x ∧ x < ordsucc n

Click to Load Proof

Theorem. (pos_real_left_approx_double)

∀x ∈ real, 0 < x → x ≠ 2 → (∀m ∈ ω, x ≠ eps_ m) → ∃w ∈ SNoL_pos x, x < 2 * w

Click to Load Proof

Theorem. (real_recip_SNo_lem1)

∀x, SNo x → x ∈ real → 0 < x → recip_SNo_pos x ∈ real ∧ ∀k, nat_p k → (SNo_recipaux x recip_SNo_pos k 0 ⊆ real) ∧ (SNo_recipaux x recip_SNo_pos k 1 ⊆ real)

Click to Load Proof

Theorem. (real_recip_SNo_pos)

∀x ∈ real, 0 < x → recip_SNo_pos x ∈ real

Click to Load Proof

Theorem. (real_recip_SNo)

∀x ∈ real, recip_SNo x ∈ real

Click to Load Proof

Theorem. (real_div_SNo)

∀x y ∈ real, x :/: y ∈ real

Click to Load Proof

End of Section Reals

Beginning of Section even_odd

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

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

Theorem. (nat_le2_cases)

∀m, nat_p m → m ⊆ 2 → m = 0 ∨ m = 1 ∨ m = 2

Click to Load Proof

Theorem. (prime_nat_2_lem)

∀m, nat_p m → ∀n, nat_p n → m * n = 2 → m = 1 ∨ m = 2

Click to Load Proof

Theorem. (prime_nat_2)

prime_nat 2

Click to Load Proof

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.

Theorem. (not_eq_2m_2n1)

∀m n ∈ int, 2 * m ≠ 2 * n + 1

Click to Load Proof

End of Section even_odd

Beginning of Section form100_22b

Let tag : set → set ≝ λα ⇒ SetAdjoin α {1}

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.

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.

Theorem. (atleastp_SNoS_ordsucc_omega_Power_omega)

atleastp (SNoS_ (ordsucc ω)) (𝒫 ω)

Click to Load Proof

Theorem. (Repl_finite)

∀f : set → set, ∀X, finite X → finite {f x|x ∈ X}

Click to Load Proof

Theorem. (infinite_bigger)

∀X ⊆ ω, infinite X → ∀m ∈ ω, ∃n ∈ X, m ∈ n

Click to Load Proof

Theorem. (equip_real_Power_omega)

equip real (𝒫 ω)

Click to Load Proof

Theorem. (form100_22_real_uncountable_atleastp)

¬ atleastp real ω

Click to Load Proof

Theorem. (form100_22_real_uncountable_equip)

¬ equip real ω

Click to Load Proof

Theorem. (form100_22_real_uncountable)

atleastp ω real ∧ ¬ equip real ω

Click to Load Proof

End of Section form100_22b

Beginning of Section rational

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 353 and no associativity corresponding to applying term div_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.

Definition. We define rational to be {x ∈ real|∃m ∈ int, ∃n ∈ ω ∖ {0}, x = m :/: n} of type set.

End of Section rational

Beginning of Section form100_3

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 353 and no associativity corresponding to applying term div_SNo.

Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.

Theorem. (Subq_int_SNoS_omega)

int ⊆ SNoS_ ω

Click to Load Proof

Theorem. (Subq_SNoS_omega_rational)

SNoS_ ω ⊆ rational

Click to Load Proof

Theorem. (Subq_rational_real)

rational ⊆ real

Click to Load Proof

Theorem. (rational_minus_SNo)

∀q ∈ rational, - q ∈ rational

Click to Load Proof

Definition. We define nat_pair to be λm n ⇒ 2 ^ m * (2 * n + 1) of type set → set → set.

Theorem. (nat_pair_In_omega)

∀m n ∈ ω, nat_pair m n ∈ ω

Click to Load Proof

Theorem. (nat_pair_0)

∀m n m' n' ∈ ω, nat_pair m n = nat_pair m' n' → m = m'

Click to Load Proof

Theorem. (nat_pair_1)

∀m n m' n' ∈ ω, nat_pair m n = nat_pair m' n' → n = n'

Click to Load Proof

Theorem. (form100_3)

equip ω rational

Click to Load Proof

End of Section form100_3

Beginning of Section SurrealSqrt

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 353 and no associativity corresponding to applying term div_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.

Definition. We define SNoL_nonneg to be λx ⇒ {w ∈ SNoL x|0 ≤ w} of type set → set.

Theorem. (SNoL_nonneg_0)

SNoL_nonneg 0 = 0

Click to Load Proof

Theorem. (SNoL_nonneg_1)

SNoL_nonneg 1 = 1

Click to Load Proof

Definition. We define SNo_sqrtauxset to be λY Z x ⇒ ⋃_{y ∈ Y}{(x + y * z) :/: (y + z)|z ∈ Z, 0 < y + z} of type set → set → set → set.

Theorem. (SNo_sqrtauxset_I)

∀Y Z x, ∀y ∈ Y, ∀z ∈ Z, 0 < y + z → (x + y * z) :/: (y + z) ∈ SNo_sqrtauxset Y Z x

Click to Load Proof

Theorem. (SNo_sqrtauxset_E)

∀Y Z x, ∀u ∈ SNo_sqrtauxset Y Z x, ∀p : prop, (∀y ∈ Y, ∀z ∈ Z, 0 < y + z → u = (x + y * z) :/: (y + z) → p) → p

Click to Load Proof

Theorem. (SNo_sqrtauxset_0)

∀Z x, SNo_sqrtauxset 0 Z x = 0

Click to Load Proof

Theorem. (SNo_sqrtauxset_0')

∀Y x, SNo_sqrtauxset Y 0 x = 0

Click to Load Proof

Definition. We define SNo_sqrtaux to be λx g ⇒ nat_primrec ({g w|w ∈ SNoL_nonneg x},{g z|z ∈ SNoR x}) (λk p ⇒ (p 0 ∪ SNo_sqrtauxset (p 0) (p 1) x,p 1 ∪ SNo_sqrtauxset (p 0) (p 0) x ∪ SNo_sqrtauxset (p 1) (p 1) x)) of type set → (set → set) → set → set.

Theorem. (SNo_sqrtaux_0)

∀x, ∀g : set → set, SNo_sqrtaux x g 0 = ({g w|w ∈ SNoL_nonneg x},{g z|z ∈ SNoR x})

Click to Load Proof

Theorem. (SNo_sqrtaux_S)

∀x, ∀g : set → set, ∀n, nat_p n → SNo_sqrtaux x g (ordsucc n) = (SNo_sqrtaux x g n 0 ∪ SNo_sqrtauxset (SNo_sqrtaux x g n 0) (SNo_sqrtaux x g n 1) x,SNo_sqrtaux x g n 1 ∪ SNo_sqrtauxset (SNo_sqrtaux x g n 0) (SNo_sqrtaux x g n 0) x ∪ SNo_sqrtauxset (SNo_sqrtaux x g n 1) (SNo_sqrtaux x g n 1) x)

Click to Load Proof

Theorem. (SNo_sqrtaux_mon_lem)

∀x, ∀g : set → set, ∀m, nat_p m → ∀n, nat_p n → SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g (add_nat m n) 0 ∧ SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g (add_nat m n) 1

Click to Load Proof

Theorem. (SNo_sqrtaux_mon)

∀x, ∀g : set → set, ∀m, nat_p m → ∀n, nat_p n → m ⊆ n → SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g n 0 ∧ SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g n 1

Click to Load Proof

Theorem. (SNo_sqrtaux_ext)

∀x, SNo x → ∀g h : set → set, (∀x' ∈ SNoS_ (SNoLev x), g x' = h x') → ∀k, nat_p k → SNo_sqrtaux x g k = SNo_sqrtaux x h k

Click to Load Proof

Beginning of Section sqrt_SNo_nonneg

Let G : set → (set → set) → set ≝ λx g ⇒ SNoCut (⋃_{k ∈ ω}SNo_sqrtaux x g k 0) (⋃_{k ∈ ω}SNo_sqrtaux x g k 1)

Definition. We define sqrt_SNo_nonneg to be SNo_rec_i G of type set → set.

Theorem. (sqrt_SNo_nonneg_eq)

∀x, SNo x → sqrt_SNo_nonneg x = G x sqrt_SNo_nonneg

Click to Load Proof

Theorem. (sqrt_SNo_nonneg_prop1a)

∀x, SNo x → 0 ≤ x → (∀w ∈ SNoS_ (SNoLev x), 0 ≤ w → SNo (sqrt_SNo_nonneg w) ∧ 0 ≤ sqrt_SNo_nonneg w ∧ sqrt_SNo_nonneg w * sqrt_SNo_nonneg w = w) → ∀k, nat_p k → (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y ∧ 0 ≤ y ∧ x < y * y)

Click to Load Proof

Theorem. (sqrt_SNo_nonneg_prop1b)

∀x, SNo x → 0 ≤ x → (∀k, nat_p k → (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y ∧ 0 ≤ y ∧ x < y * y)) → SNoCutP (⋃_{k ∈ ω}SNo_sqrtaux x sqrt_SNo_nonneg k 0) (⋃_{k ∈ ω}SNo_sqrtaux x sqrt_SNo_nonneg k 1)

Click to Load Proof

Theorem. (sqrt_SNo_nonneg_prop1c)

∀x, SNo x → 0 ≤ x → SNoCutP (⋃_{k ∈ ω}SNo_sqrtaux x sqrt_SNo_nonneg k 0) (⋃_{k ∈ ω}SNo_sqrtaux x sqrt_SNo_nonneg k 1) → (∀z ∈ (⋃_{k ∈ ω}SNo_sqrtaux x sqrt_SNo_nonneg k 1), ∀p : prop, (SNo z → 0 ≤ z → x < z * z → p) → p) → 0 ≤ G x sqrt_SNo_nonneg

Click to Load Proof

Theorem. (sqrt_SNo_nonneg_prop1d)

∀x, SNo x → 0 ≤ x → (∀w ∈ SNoS_ (SNoLev x), 0 ≤ w → SNo (sqrt_SNo_nonneg w) ∧ 0 ≤ sqrt_SNo_nonneg w ∧ sqrt_SNo_nonneg w * sqrt_SNo_nonneg w = w) → SNoCutP (⋃_{k ∈ ω}SNo_sqrtaux x sqrt_SNo_nonneg k 0) (⋃_{k ∈ ω}SNo_sqrtaux x sqrt_SNo_nonneg k 1) → 0 ≤ G x sqrt_SNo_nonneg → G x sqrt_SNo_nonneg * G x sqrt_SNo_nonneg < x → False

Click to Load Proof

Theorem. (sqrt_SNo_nonneg_prop1e)

∀x, SNo x → 0 ≤ x → (∀w ∈ SNoS_ (SNoLev x), 0 ≤ w → SNo (sqrt_SNo_nonneg w) ∧ 0 ≤ sqrt_SNo_nonneg w ∧ sqrt_SNo_nonneg w * sqrt_SNo_nonneg w = w) → SNoCutP (⋃_{k ∈ ω}SNo_sqrtaux x sqrt_SNo_nonneg k 0) (⋃_{k ∈ ω}SNo_sqrtaux x sqrt_SNo_nonneg k 1) → 0 ≤ G x sqrt_SNo_nonneg → x < G x sqrt_SNo_nonneg * G x sqrt_SNo_nonneg → False

Click to Load Proof

Theorem. (sqrt_SNo_nonneg_prop1)

∀x, SNo x → 0 ≤ x → SNo (sqrt_SNo_nonneg x) ∧ 0 ≤ sqrt_SNo_nonneg x ∧ sqrt_SNo_nonneg x * sqrt_SNo_nonneg x = x

Click to Load Proof

End of Section sqrt_SNo_nonneg

Theorem. (SNo_sqrtaux_0_1_prop)

∀x, SNo x → 0 ≤ x → ∀k, nat_p k → (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y ∧ 0 ≤ y ∧ x < y * y)

Click to Load Proof

Theorem. (SNo_sqrtaux_0_prop)

∀x, SNo x → 0 ≤ x → ∀k, nat_p k → ∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y ∧ 0 ≤ y ∧ y * y < x

Click to Load Proof

Theorem. (SNo_sqrtaux_1_prop)

∀x, SNo x → 0 ≤ x → ∀k, nat_p k → ∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y ∧ 0 ≤ y ∧ x < y * y

Click to Load Proof

Theorem. (SNo_sqrt_SNo_SNoCutP)

∀x, SNo x → 0 ≤ x → SNoCutP (⋃_{k ∈ ω}SNo_sqrtaux x sqrt_SNo_nonneg k 0) (⋃_{k ∈ ω}SNo_sqrtaux x sqrt_SNo_nonneg k 1)

Click to Load Proof

Theorem. (SNo_sqrt_SNo_nonneg)

∀x, SNo x → 0 ≤ x → SNo (sqrt_SNo_nonneg x)

Click to Load Proof

Theorem. (sqrt_SNo_nonneg_nonneg)

∀x, SNo x → 0 ≤ x → 0 ≤ sqrt_SNo_nonneg x

Click to Load Proof

Theorem. (sqrt_SNo_nonneg_sqr)

∀x, SNo x → 0 ≤ x → sqrt_SNo_nonneg x * sqrt_SNo_nonneg x = x

Click to Load Proof

Theorem. (sqrt_SNo_nonneg_0)

sqrt_SNo_nonneg 0 = 0

Click to Load Proof

Theorem. (sqrt_SNo_nonneg_1)

sqrt_SNo_nonneg 1 = 1

Click to Load Proof

Theorem. (sqrt_SNo_nonneg_0inL0)

∀x, SNo x → 0 ≤ x → 0 ∈ SNoLev x → 0 ∈ SNo_sqrtaux x sqrt_SNo_nonneg 0 0

Click to Load Proof

Theorem. (sqrt_SNo_nonneg_Lnonempty)

∀x, SNo x → 0 ≤ x → 0 ∈ SNoLev x → (⋃_{k ∈ ω}SNo_sqrtaux x sqrt_SNo_nonneg k 0) ≠ 0

Click to Load Proof

Theorem. (sqrt_SNo_nonneg_Rnonempty)

∀x, SNo x → 0 ≤ x → 1 ∈ SNoLev x → (⋃_{k ∈ ω}SNo_sqrtaux x sqrt_SNo_nonneg k 1) ≠ 0

Click to Load Proof

Theorem. (SNo_sqrtauxset_real)

∀Y Z x, Y ⊆ real → Z ⊆ real → x ∈ real → SNo_sqrtauxset Y Z x ⊆ real

Click to Load Proof

Theorem. (SNo_sqrtauxset_real_nonneg)

∀Y Z x, Y ⊆ {w ∈ real|0 ≤ w} → Z ⊆ {z ∈ real|0 ≤ z} → x ∈ real → 0 ≤ x → SNo_sqrtauxset Y Z x ⊆ {w ∈ real|0 ≤ w}

Click to Load Proof

Theorem. (sqrt_SNo_nonneg_SNoS_omega)

∀x ∈ SNoS_ ω, 0 ≤ x → sqrt_SNo_nonneg x ∈ real

Click to Load Proof

Theorem. (sqrt_SNo_nonneg_real)

∀x ∈ real, 0 ≤ x → sqrt_SNo_nonneg x ∈ real

Click to Load Proof

End of Section SurrealSqrt

Beginning of Section form100_1

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 353 and no associativity corresponding to applying term div_SNo.

Theorem. (divides_int_div_SNo_int)

∀m n, divides_int m n → n :/: m ∈ int

Click to Load Proof

Theorem. (form100_1_lem1)

∀m, nat_p m → ∀n, nat_p n → m * m = 2 * n * n → n = 0

Click to Load Proof

Theorem. (form100_1_lem2)

∀m ∈ ω, ∀n ∈ ω ∖ 1, m * m ≠ 2 * n * n

Click to Load Proof

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 353 and no associativity corresponding to applying term div_SNo.

Theorem. (sqrt_2_irrational)

sqrt_SNo_nonneg 2 ∈ real ∖ rational

Click to Load Proof

End of Section form100_1