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:

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.

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.


Primitives and Axioms

Primitive. The name Eps_i is a term of type (setprop)set.
Axiom. (Eps_i_ax) We take the following as an axiom:
∀P : setprop, ∀x : set, P xP (Eps_i P)
Definition. We define True to be ∀p : prop, pp of type prop.
Definition. We define False to be ∀p : prop, p of type prop.
Definition. We define not to be λA : propAFalse of type propprop.
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, (ABp)p of type proppropprop.
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, (Ap)(Bp)p of type proppropprop.
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 : propand (AB) (BA) of type proppropprop.
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 : AAprop, Q x yQ y x of type AAprop.
Definition. We define neq to be λx y : A¬ eq x y of type AAprop.
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 : AB, (∀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 : Aprop∀P : prop, (∀x : A, Q xP)P of type (Aprop)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 qp = q
Primitive. The name In is a term of type setsetprop.
Notation. We use as an infix operator with priority 500 and no associativity corresponding to applying term In. Furthermore, we may write xA, B to mean x : set, xAB.
Definition. We define Subq to be λA B ⇒ xA, x B of type setsetprop.
Notation. We use as an infix operator with priority 500 and no associativity corresponding to applying term Subq. Furthermore, we may write xA, B to mean x : set, xAB.
Axiom. (set_ext) We take the following as an axiom:
∀X Y : set, X YY XX = Y
Axiom. (In_ind) We take the following as an axiom:
∀P : setprop, (∀X : set, (xX, 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 setset.
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 setset.
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(setset)set.
Notation. {B| xA} is notation for Repl Ax . B).
Axiom. (ReplEq) We take the following as an axiom:
∀A : set, ∀F : setset, ∀y : set, y {F x|xA} xA, y = F x
Definition. We define TransSet to be λU : setxU, x U of type setprop.
Definition. We define Union_closed to be λU : set∀X : set, X U X U of type setprop.
Definition. We define Power_closed to be λU : set∀X : set, X U𝒫 X U of type setprop.
Definition. We define Repl_closed to be λU : set∀X : set, X U∀F : setset, (∀x : set, x XF x U){F x|xX} U of type setprop.
Definition. We define ZF_closed to be λU : setUnion_closed U Power_closed U Repl_closed U of type setprop.
Primitive. The name UnivOf is a term of type setset.
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 UTransSet UZF_closed UUnivOf N U

First Theorems Up To Excluded Middle

Theorem. (andI)
∀A B : prop, ABA B
Click to Load Proof
Theorem. (orIL)
∀A B : prop, AA B
Click to Load Proof
Theorem. (orIR)
∀A B : prop, BA B
Click to Load Proof
Theorem. (iffI)
∀A B : prop, (AB)(BA)(A B)
Click to Load Proof
Theorem. (pred_ext)
∀P Q : setprop, (∀x, P x Q x)P = Q
Click to Load Proof
Definition. We define nIn to be λx X ⇒ ¬ In x X of type setsetprop.
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 XY 𝒫 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 BA
Click to Load Proof
Theorem. (andER)
∀A B : prop, A BB
Click to Load Proof
Beginning of Section PropN
Variable P1 P2 P3 : prop
Theorem. (and3I)
P1P2P3P1 P2 P3
Click to Load Proof
Theorem. (and3E)
P1 P2 P3(∀p : prop, (P1P2P3p)p)
Click to Load Proof
Theorem. (or3I1)
P1P1 P2 P3
Click to Load Proof
Theorem. (or3I2)
P2P1 P2 P3
Click to Load Proof
Theorem. (or3I3)
P3P1 P2 P3
Click to Load Proof
Theorem. (or3E)
P1 P2 P3(∀p : prop, (P1p)(P2p)(P3p)p)
Click to Load Proof
Variable P4 : prop
Theorem. (and4I)
P1P2P3P4P1 P2 P3 P4
Click to Load Proof
Variable P5 : prop
Theorem. (and5I)
P1P2P3P4P5P1 P2 P3 P4 P5
Click to Load Proof
Variable P6 : prop
Theorem. (and6I)
P1P2P3P4P5P6P1 P2 P3 P4 P5 P6
Click to Load Proof
Variable P7 : prop
Theorem. (and7I)
P1P2P3P4P5P6P7P1 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 : setprop, (¬ x, P x)∀x, ¬ P x
Click to Load Proof
Theorem. (iffEL)
∀A B : prop, (A B)AB
Click to Load Proof
Theorem. (iffER)
∀A B : prop, (A B)BA
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 = yy = zx = z
Click to Load Proof
Theorem. (neq_i_sym)
∀x y, x yy x
Click to Load Proof
Theorem. (Eps_i_ex)
∀P : setprop, (x, P x)P (Eps_i P)
Click to Load Proof
Theorem. (prop_ext_2)
∀p q : prop, (pq)(qp)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 YY ZX Z
Click to Load Proof
Theorem. (Empty_Subq_eq)
∀X : set, X EmptyX = 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 YY Xx X
Click to Load Proof
Theorem. (UnionE)
∀X x : set, x XY : set, x Y Y X
Click to Load Proof
Theorem. (UnionE_impred)
∀X x : set, x X∀p : prop, (∀Y : set, x YY Xp)p
Click to Load Proof
Theorem. (PowerE)
∀X Y : set, Y 𝒫 XY X
Click to Load Proof
Theorem. (Self_In_Power)
∀X : set, X 𝒫 X
Click to Load Proof
Theorem. (dneg)
∀P : prop, ¬ ¬ PP
Click to Load Proof
Theorem. (not_all_ex_demorgan_i)
∀P : setprop, ¬ (∀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 : propA ¬ B ¬ A B of type proppropprop.
Theorem. (exactly1of2_I1)
∀A B : prop, A¬ Bexactly1of2 A B
Click to Load Proof
Theorem. (exactly1of2_I2)
∀A B : prop, ¬ ABexactly1of2 A B
Click to Load Proof
Theorem. (exactly1of2_E)
∀A B : prop, exactly1of2 A B∀p : prop, (A¬ Bp)(¬ ABp)p
Click to Load Proof
Theorem. (exactly1of2_or)
∀A B : prop, exactly1of2 A BA B
Click to Load Proof
Theorem. (ReplI)
∀A : set, ∀F : setset, ∀x : set, x AF x {F x|xA}
Click to Load Proof
Theorem. (ReplE)
∀A : set, ∀F : setset, ∀y : set, y {F x|xA}xA, y = F x
Click to Load Proof
Theorem. (ReplE_impred)
∀A : set, ∀F : setset, ∀y : set, y {F x|xA}∀p : prop, (∀x : set, x Ay = F xp)p
Click to Load Proof
Theorem. (ReplE')
∀X, ∀f : setset, ∀p : setprop, (xX, p (f x))y{f x|xX}, p y
Click to Load Proof
Theorem. (Repl_Empty)
∀F : setset, {F x|xEmpty} = Empty
Click to Load Proof
Theorem. (ReplEq_ext_sub)
∀X, ∀F G : setset, (xX, F x = G x){F x|xX} {G x|xX}
Click to Load Proof
Theorem. (ReplEq_ext)
∀X, ∀F G : setset, (xX, F x = G x){F x|xX} = {G x|xX}
Click to Load Proof
Theorem. (Repl_inv_eq)
∀P : setprop, ∀f g : setset, (∀x, P xg (f x) = x)∀X, (xX, P x){g y|y{f x|xX}} = X
Click to Load Proof
Theorem. (Repl_invol_eq)
∀P : setprop, ∀f : setset, (∀x, P xf (f x) = x)∀X, (xX, P x){f y|y{f x|xX}} = X
Click to Load Proof
Definition. We define If_i to be (λp x y ⇒ Eps_i (λz : setp z = x ¬ p z = y)) of type propsetsetset.
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 setsetset.
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 setset.
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 setsetset.
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 Xz X Y
Click to Load Proof
Theorem. (binunionI2)
∀X Y z : set, z Yz X Y
Click to Load Proof
Theorem. (binunionE)
∀X Y z : set, z X Yz X z Y
Click to Load Proof
Theorem. (binunionE')
∀X Y z, ∀p : prop, (z Xp)(z Yp)(z X Yp)
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 ZY ZX 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 setsetset.
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|xX} of type set(setset)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 : (setset), ∀x y : set, x Xy F xy xXF x
Click to Load Proof
Theorem. (famunionE)
∀X : set, ∀F : (setset), ∀y : set, y (xXF x)xX, y F x
Click to Load Proof
Theorem. (famunionE_impred)
∀X : set, ∀F : (setset), ∀y : set, y (xXF x)∀p : prop, (∀x, x Xy F xp)p
Click to Load Proof
Theorem. (famunion_Empty)
∀F : setset, (xEmptyF x) = Empty
Click to Load Proof
Theorem. (famunion_Subq)
∀X, ∀f g : setset, (xX, f x g x)famunion X f famunion X g
Click to Load Proof
Theorem. (famunion_ext)
∀X, ∀f g : setset, (xX, f x = g x)famunion X f = famunion X g
Click to Load Proof
Beginning of Section SepSec
Variable X : set
Variable P : setprop
Let z : setEps_i (λz ⇒ z X P z)
Let F : setsetλx ⇒ if P x then x else z
Definition. We define Sep to be if (zX, P z) then {F x|xX} else Empty of type set.
End of Section SepSec
Notation. {xA | B} is notation for Sep Ax . B).
Theorem. (SepI)
∀X : set, ∀P : (setprop), ∀x : set, x XP xx {xX|P x}
Click to Load Proof
Theorem. (SepE)
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}x X P x
Click to Load Proof
Theorem. (SepE1)
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}x X
Click to Load Proof
Theorem. (SepE2)
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}P x
Click to Load Proof
Theorem. (Sep_Empty)
∀P : setprop, {xEmpty|P x} = Empty
Click to Load Proof
Theorem. (Sep_Subq)
∀X : set, ∀P : setprop, {xX|P x} X
Click to Load Proof
Theorem. (Sep_In_Power)
∀X : set, ∀P : setprop, {xX|P x} 𝒫 X
Click to Load Proof
Definition. We define ReplSep to be λX P F ⇒ {F x|x{zX|P z}} of type set(setprop)(setset)set.
Notation. {B| xA, C} is notation for ReplSep Ax . C) (λ x . B).
Theorem. (ReplSepI)
∀X : set, ∀P : setprop, ∀F : setset, ∀x : set, x XP xF x {F x|xX, P x}
Click to Load Proof
Theorem. (ReplSepE)
∀X : set, ∀P : setprop, ∀F : setset, ∀y : set, y {F x|xX, P x}x : set, x X P x y = F x
Click to Load Proof
Theorem. (ReplSepE_impred)
∀X : set, ∀P : setprop, ∀F : setset, ∀y : set, y {F x|xX, P x}∀p : prop, (xX, P xy = F xp)p
Click to Load Proof
Definition. We define binintersect to be λX Y ⇒ {xX|x Y} of type setsetset.
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 Xz Yz X Y
Click to Load Proof
Theorem. (binintersectE)
∀X Y z, z X Yz X z Y
Click to Load Proof
Theorem. (binintersectE1)
∀X Y z, z X Yz X
Click to Load Proof
Theorem. (binintersectE2)
∀X Y z, z X Yz 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 YX Y = X
Click to Load Proof
Theorem. (binintersect_Subq_max)
∀X Y Z : set, Z XZ YZ 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 setsetset.
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, xX, X = (X {x}) {x}
Click to Load Proof
Theorem. (In_irref)
∀x, x x
Click to Load Proof
Theorem. (In_no2cycle)
∀x y, x yy xFalse
Click to Load Proof
Definition. We define ordsucc to be λx : setx {x} of type setset.
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 xy 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 ba = b
Click to Load Proof
Theorem. (In_0_1)
Click to Load Proof
Theorem. (In_0_2)
Click to Load Proof
Theorem. (In_1_2)
Click to Load Proof
Definition. We define nat_p to be λn : set∀p : setprop, p 0(∀x : set, p xp (ordsucc x))p n of type setprop.
Theorem. (nat_0)
Click to Load Proof
Theorem. (nat_ordsucc)
∀n : set, nat_p nnat_p (ordsucc n)
Click to Load Proof
Theorem. (nat_1)
Click to Load Proof
Theorem. (nat_2)
Click to Load Proof
Theorem. (nat_0_in_ordsucc)
∀n, nat_p n0 ordsucc n
Click to Load Proof
Theorem. (nat_ordsucc_in_ordsucc)
Click to Load Proof
Theorem. (nat_ind)
∀p : setprop, p 0(∀n, nat_p np np (ordsucc n))∀n, nat_p np n
Click to Load Proof
Theorem. (nat_complete_ind)
∀p : setprop, (∀n, nat_p n(mn, p m)p n)∀n, nat_p np n
Click to Load Proof
Theorem. (nat_inv_impred)
∀p : setprop, p 0(∀n, nat_p np (ordsucc n))∀n, nat_p np n
Click to Load Proof
Theorem. (nat_inv)
∀n, nat_p nn = 0 x, nat_p x n = ordsucc x
Click to Load Proof
Theorem. (nat_p_trans)
∀n, nat_p nmn, nat_p m
Click to Load Proof
Theorem. (nat_trans)
∀n, nat_p nmn, m n
Click to Load Proof
Theorem. (nat_ordsucc_trans)
∀n, nat_p nmordsucc n, m n
Click to Load Proof
Definition. We define surj to be λX Y f ⇒ (uX, f u Y) (wY, uX, f u = w) of type setset(setset)prop.
Theorem. (form100_63_surjCantor)
∀A : set, ∀f : setset, ¬ surj A (𝒫 A) f
Click to Load Proof
Definition. We define inj to be λX Y f ⇒ (uX, f u Y) (u vX, f u = f vu = v) of type setset(setset)prop.
Theorem. (form100_63_injCantor)
∀A : set, ∀f : setset, ¬ inj (𝒫 A) A f
Click to Load Proof
Theorem. (injI)
∀X Y, ∀f : setset, (xX, f x Y)(x zX, f x = f zx = z)inj X Y f
Click to Load Proof
Theorem. (inj_comp)
∀X Y Z : set, ∀f g : setset, inj X Y finj Y Z ginj X Z (λx ⇒ g (f x))
Click to Load Proof
Definition. We define bij to be λX Y f ⇒ (uX, f u Y) (u vX, f u = f vu = v) (wY, uX, f u = w) of type setset(setset)prop.
Theorem. (bijI)
∀X Y, ∀f : setset, (uX, f u Y)(u vX, f u = f vu = v)(wY, uX, f u = w)bij X Y f
Click to Load Proof
Theorem. (bijE)
∀X Y, ∀f : setset, bij X Y f∀p : prop, ((uX, f u Y)(u vX, f u = f vu = v)(wY, uX, f u = w)p)p
Click to Load Proof
Theorem. (bij_inj)
∀X Y, ∀f : setset, bij X Y finj 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 : setset, bij X Y fbij Y Z gbij X Z (λx ⇒ g (f x))
Click to Load Proof
Theorem. (bij_surj)
∀X Y, ∀f : setset, bij X Y fsurj X Y f
Click to Load Proof
Definition. We define inv to be λX f ⇒ λy : setEps_i (λx ⇒ x X f x = y) of type set(setset)setset.
Theorem. (surj_rinv)
∀X Y, ∀f : setset, (wY, uX, f u = w)yY, inv X f y X f (inv X f y) = y
Click to Load Proof
Theorem. (inj_linv)
∀X, ∀f : setset, (u vX, f u = f vu = v)xX, inv X f (f x) = x
Click to Load Proof
Theorem. (bij_inv)
∀X Y, ∀f : setset, bij X Y fbij Y X (inv X f)
Click to Load Proof
Definition. We define atleastp to be λX Y : setf : setset, inj X Y f of type setsetprop.
Theorem. (atleastp_tra)
∀X Y Z, atleastp X Yatleastp Y Zatleastp X Z
Click to Load Proof
Theorem. (Subq_atleastp)
∀X Y, X Yatleastp X Y
Click to Load Proof
Definition. We define equip to be λX Y : setf : setset, bij X Y f of type setsetprop.
Theorem. (equip_atleastp)
∀X Y, equip X Yatleastp X Y
Click to Load Proof
Theorem. (equip_ref)
∀X, equip X X
Click to Load Proof
Theorem. (equip_sym)
∀X Y, equip X Yequip Y X
Click to Load Proof
Theorem. (equip_tra)
∀X Y Z, equip X Yequip Y Zequip X Z
Click to Load Proof
Theorem. (equip_0_Empty)
∀X, equip X 0X = 0
Click to Load Proof
Theorem. (equip_adjoin_ordsucc)
∀N X y, y Xequip N Xequip (ordsucc N) (X {y})
Click to Load Proof
Theorem. (equip_ordsucc_remove1)
∀X N, xX, equip X (ordsucc N)equip (X {x}) N
Click to Load Proof
Beginning of Section SchroederBernstein
Theorem. (KnasterTarski_set)
∀A, ∀F : setset, (U𝒫 A, F U 𝒫 A)(U V𝒫 A, U VF U F V)Y𝒫 A, F Y = Y
Click to Load Proof
Theorem. (image_In_Power)
∀A B, ∀f : setset, (xA, f x B)U𝒫 A, {f x|xU} 𝒫 B
Click to Load Proof
Theorem. (image_monotone)
∀f : setset, ∀U V, U V{f x|xU} {f x|xV}
Click to Load Proof
Theorem. (setminus_antimonotone)
∀A U V, U VA V A U
Click to Load Proof
Theorem. (SchroederBernstein)
∀A B, ∀f g : setset, inj A B finj B A gequip A B
Click to Load Proof
Click to Load Proof
End of Section SchroederBernstein
Beginning of Section PigeonHole
Theorem. (PigeonHole_nat)
∀n, nat_p n∀f : setset, (iordsucc n, f i n)¬ (i jordsucc n, f i = f ji = j)
Click to Load Proof
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)
i1, ∀p : setprop, p 0p i
Click to Load Proof
Theorem. (cases_2)
i2, ∀p : setprop, p 0p 1p i
Click to Load Proof
Theorem. (neq_0_1)
Click to Load Proof
Theorem. (neq_1_0)
Click to Load Proof
Theorem. (neq_0_2)
Click to Load Proof
Theorem. (neq_2_0)
Click to Load Proof
Definition. We define ordinal to be λα : setTransSet α βα, TransSet β of type setprop.
Theorem. (ordinal_TransSet)
∀α : set, ordinal αTransSet α
Click to Load Proof
Theorem. (ordinal_Empty)
Click to Load Proof
Theorem. (ordinal_Hered)
∀α : set, ordinal αβα, ordinal β
Click to Load Proof
Theorem. (TransSet_ordsucc)
∀X : set, TransSet XTransSet (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 nordinal n
Click to Load Proof
Theorem. (ordinal_1)
Click to Load Proof
Theorem. (ordinal_2)
Click to Load Proof
Theorem. (TransSet_ordsucc_In_Subq)
∀X : set, TransSet XxX, 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 : setset, (xX, ordinal (F x))ordinal (xXF 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 : setprop, (∀α, ordinal α(βα, p β)p α)∀α, ordinal αp α
Click to Load Proof
Theorem. (least_ordinal_ex)
∀p : setprop, (α, 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 yx ordsucc yx y
Click to Load Proof
Theorem. (exandE_i)
∀P Q : setprop, (x, P x Q x)∀r : prop, (∀x, P xQ xr)r
Click to Load Proof
Theorem. (exandE_ii)
∀P Q : (setset)prop, (x : setset, P x Q x)∀p : prop, (∀x : setset, P xQ xp)p
Click to Load Proof
Theorem. (exandE_iii)
∀P Q : (setsetset)prop, (x : setsetset, P x Q x)∀p : prop, (∀x : setsetset, P xQ xp)p
Click to Load Proof
Theorem. (exandE_iiii)
∀P Q : (setsetsetset)prop, (x : setsetsetset, P x Q x)∀p : prop, (∀x : setsetsetset, P xQ xp)p
Click to Load Proof
Beginning of Section Descr_ii
Variable P : (setset)prop
Definition. We define Descr_ii to be λx : setEps_i (λy ⇒ ∀h : setset, P hh x = y) of type setset.
Hypothesis Pex : f : setset, P f
Hypothesis Puniq : ∀f g : setset, P fP gf = g
Click to Load Proof
End of Section Descr_ii
Beginning of Section Descr_iii
Variable P : (setsetset)prop
Definition. We define Descr_iii to be λx y : setEps_i (λz ⇒ ∀h : setsetset, P hh x y = z) of type setsetset.
Hypothesis Pex : f : setsetset, P f
Hypothesis Puniq : ∀f g : setsetset, P fP gf = g
Click to Load Proof
End of Section Descr_iii
Beginning of Section Descr_Vo1
Variable P : Vo 1prop
Definition. We define Descr_Vo1 to be λx : set∀h : setprop, P hh x of type Vo 1.
Hypothesis Pex : f : Vo 1, P f
Hypothesis Puniq : ∀f g : Vo 1, P fP gf = g
Click to Load Proof
End of Section Descr_Vo1
Beginning of Section If_ii
Variable p : prop
Variable f g : setset
Definition. We define If_ii to be λx ⇒ if p then f x else g x of type setset.
Click to Load Proof
Click to Load Proof
End of Section If_ii
Beginning of Section If_iii
Variable p : prop
Variable f g : setsetset
Definition. We define If_iii to be λx y ⇒ if p then f x y else g x y of type setsetset.
Click to Load Proof
Click to Load Proof
End of Section If_iii
Beginning of Section EpsilonRec_i
Variable F : set(setset)set
Definition. We define In_rec_i_G to be λX Y ⇒ ∀R : setsetprop, (∀X : set, ∀f : setset, (xX, R x (f x))R X (F X f))R X Y of type setsetprop.
Definition. We define In_rec_i to be λX ⇒ Eps_i (In_rec_i_G X) of type setset.
Theorem. (In_rec_i_G_c)
∀X : set, ∀f : setset, (xX, 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 Yf : setset, (xX, In_rec_i_G x (f x)) Y = F X f
Click to Load Proof
Hypothesis Fr : ∀X : set, ∀g h : setset, (xX, 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 YIn_rec_i_G X ZY = Z
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
Variable F : set(set(setset))(setset)
Definition. We define In_rec_G_ii to be λX Y ⇒ ∀R : set(setset)prop, (∀X : set, ∀f : set(setset), (xX, R x (f x))R X (F X f))R X Y of type set(setset)prop.
Definition. We define In_rec_ii to be λX ⇒ Descr_ii (In_rec_G_ii X) of type set(setset).
Theorem. (In_rec_G_ii_c)
∀X : set, ∀f : set(setset), (xX, 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 : (setset), In_rec_G_ii X Yf : set(setset), (xX, In_rec_G_ii x (f x)) Y = F X f
Click to Load Proof
Hypothesis Fr : ∀X : set, ∀g h : set(setset), (xX, g x = h x)F X g = F X h
Theorem. (In_rec_G_ii_f)
∀X : set, ∀Y Z : (setset), In_rec_G_ii X YIn_rec_G_ii X ZY = Z
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
Variable F : set(set(setsetset))(setsetset)
Definition. We define In_rec_G_iii to be λX Y ⇒ ∀R : set(setsetset)prop, (∀X : set, ∀f : set(setsetset), (xX, R x (f x))R X (F X f))R X Y of type set(setsetset)prop.
Definition. We define In_rec_iii to be λX ⇒ Descr_iii (In_rec_G_iii X) of type set(setsetset).
Theorem. (In_rec_G_iii_c)
∀X : set, ∀f : set(setsetset), (xX, 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 : (setsetset), In_rec_G_iii X Yf : set(setsetset), (xX, In_rec_G_iii x (f x)) Y = F X f
Click to Load Proof
Hypothesis Fr : ∀X : set, ∀g h : set(setsetset), (xX, g x = h x)F X g = F X h
Theorem. (In_rec_G_iii_f)
∀X : set, ∀Y Z : (setsetset), In_rec_G_iii X YIn_rec_G_iii X ZY = Z
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
End of Section EpsilonRec_iii
Beginning of Section NatRec
Variable z : set
Variable f : setsetset
Let F : set(setset)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 setset.
Theorem. (nat_primrec_r)
∀X : set, ∀g h : setset, (xX, g x = h x)F X g = F X h
Click to Load Proof
Click to Load Proof
Click to Load Proof
End of Section NatRec
Beginning of Section NatAdd
Definition. We define add_nat to be λn m : setnat_primrec n (λ_ r ⇒ ordsucc r) m of type setsetset.
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 mn + ordsucc m = ordsucc (n + m)
Click to Load Proof
Theorem. (add_nat_p)
∀n : set, nat_p n∀m : set, nat_p mnat_p (n + m)
Click to Load Proof
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 m0 + m = m
Click to Load Proof
Theorem. (add_nat_SL)
∀n : set, nat_p n∀m : set, nat_p mordsucc n + m = ordsucc (n + m)
Click to Load Proof
Theorem. (add_nat_com)
∀n : set, nat_p n∀m : set, nat_p mn + m = m + n
Click to Load Proof
Theorem. (add_nat_In_R)
∀m, nat_p mkm, ∀n, nat_p nk + n m + n
Click to Load Proof
Theorem. (add_nat_In_L)
∀n, nat_p n∀m, nat_p mkm, n + k n + m
Click to Load Proof
Theorem. (add_nat_Subq_R)
∀k, nat_p k∀m, nat_p mk m∀n, nat_p nk + n m + n
Click to Load Proof
Theorem. (add_nat_Subq_L)
∀n, nat_p n∀k, nat_p k∀m, nat_p mk mn + k n + m
Click to Load Proof
Theorem. (add_nat_Subq_R')
∀m, nat_p m∀n, nat_p nm m + n
Click to Load Proof
Theorem. (nat_Subq_add_ex)
∀n, nat_p n∀m, nat_p mn mk, 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 nk + n = m + nk = 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 : setnat_primrec 0 (λ_ r ⇒ n + r) m of type setsetset.
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 mn * ordsucc m = n + n * m
Click to Load Proof
Click to Load Proof
Theorem. (mul_nat_p)
∀n : set, nat_p n∀m : set, nat_p mnat_p (n * m)
Click to Load Proof
Theorem. (mul_nat_0L)
∀m : set, nat_p m0 * m = 0
Click to Load Proof
Theorem. (mul_nat_SL)
∀n : set, nat_p n∀m : set, nat_p mordsucc n * m = n * m + m
Click to Load Proof
Theorem. (mul_nat_com)
∀n : set, nat_p n∀m : set, nat_p mn * 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 kn * (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 mnat_p nm n∀k, nat_p km * k n * k
Click to Load Proof
Theorem. (mul_nat_Subq_L)
∀m n, nat_p mnat_p nm n∀k, nat_p kk * m k * n
Click to Load Proof
Theorem. (mul_nat_0_or_Subq)
∀m, nat_p m∀n, nat_p nn = 0 m m * n
Click to Load Proof
Theorem. (mul_nat_0_inv)
∀m, nat_p m∀n, nat_p nm * n = 0m = 0 n = 0
Click to Load Proof
Theorem. (mul_nat_0m_1n_In)
∀m, nat_p m∀n, nat_p n0 m1 nm m * n
Click to Load Proof
Theorem. (nat_le1_cases)
∀m, nat_p mm 1m = 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 (setset)setset.
Theorem. (Pi_nat_0)
∀f : setset, Pi_nat f 0 = 1
Click to Load Proof
Theorem. (Pi_nat_S)
∀f : setset, ∀n, nat_p nPi_nat f (ordsucc n) = Pi_nat f n * f n
Click to Load Proof
Theorem. (Pi_nat_p)
∀f : setset, ∀n, nat_p n(in, nat_p (f i))nat_p (Pi_nat f n)
Click to Load Proof
Theorem. (Pi_nat_0_inv)
∀f : setset, ∀n, nat_p n(in, nat_p (f i))Pi_nat f n = 0(in, f i = 0)
Click to Load Proof
Definition. We define exp_nat to be λn m : setnat_primrec 1 (λ_ r ⇒ n * r) m of type setsetset.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_nat.
Click to Load Proof
Theorem. (exp_nat_S)
∀n m, nat_p mn ^ (ordsucc m) = n * n ^ m
Click to Load Proof
Theorem. (exp_nat_p)
∀n, nat_p n∀m, nat_p mnat_p (n ^ m)
Click to Load Proof
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.
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Theorem. (equip_finite_Power)
∀n, nat_p n∀X, equip X nequip (𝒫 X) (2 ^ n)
Click to Load Proof
End of Section form100_52
Theorem. (ZF_closed_E)
∀U, ZF_closed U∀p : prop, (Union_closed UPower_closed URepl_closed Up)p
Click to Load Proof
Theorem. (ZF_Union_closed)
∀U, ZF_closed UXU, X U
Click to Load Proof
Theorem. (ZF_Power_closed)
∀U, ZF_closed UXU, 𝒫 X U
Click to Load Proof
Theorem. (ZF_Repl_closed)
∀U, ZF_closed UXU, ∀F : setset, (xX, F x U){F x|xX} U
Click to Load Proof
Theorem. (ZF_UPair_closed)
∀U, ZF_closed Ux yU, {x,y} U
Click to Load Proof
Theorem. (ZF_Sing_closed)
∀U, ZF_closed UxU, {x} U
Click to Load Proof
Theorem. (ZF_binunion_closed)
∀U, ZF_closed UX YU, (X Y) U
Click to Load Proof
Theorem. (ZF_ordsucc_closed)
∀U, ZF_closed UxU, ordsucc x U
Click to Load Proof
Theorem. (nat_p_UnivOf_Empty)
∀n : set, nat_p nn UnivOf Empty
Click to Load Proof
Definition. We define ω to be {nUnivOf Empty|nat_p n} of type set.
Theorem. (omega_nat_p)
Click to Load Proof
Theorem. (nat_p_omega)
∀n : set, nat_p nn ω
Click to Load Proof
Theorem. (omega_ordsucc)
Click to Load Proof
Theorem. (form100_22_v2)
∀f : setset, ¬ inj (𝒫 ω) ω f
Click to Load Proof
Theorem. (form100_22_v3)
∀g : setset, ¬ surj ω (𝒫 ω) g
Click to Load Proof
Theorem. (form100_22_v1)
Click to Load Proof
Theorem. (omega_TransSet)
Click to Load Proof
Theorem. (omega_ordinal)
Click to Load Proof
Theorem. (ordsucc_omega_ordinal)
Click to Load Proof
Definition. We define finite to be λX ⇒ nω, equip X n of type setprop.
Theorem. (nat_finite)
∀n, nat_p nfinite n
Click to Load Proof
Theorem. (finite_ind)
∀p : setprop, p Empty(∀X y, finite Xy Xp Xp (X {y}))∀X, finite Xp X
Click to Load Proof
Theorem. (finite_Empty)
Click to Load Proof
Theorem. (Sing_finite)
∀x, finite {x}
Click to Load Proof
Theorem. (adjoin_finite)
∀X y, finite Xfinite (X {y})
Click to Load Proof
Theorem. (binunion_finite)
∀X, finite X∀Y, finite Yfinite (X Y)
Click to Load Proof
Theorem. (famunion_nat_finite)
∀X : setset, ∀n, nat_p n(in, finite (X i))finite (inX i)
Click to Load Proof
Theorem. (Subq_finite)
∀X, finite X∀Y, Y Xfinite Y
Click to Load Proof
Definition. We define infinite to be λA ⇒ ¬ finite A of type setprop.
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 setsetprop.
Click to Load Proof
Click to Load Proof
Definition. We define prime_nat to be λn ⇒ n ω 1 n kω, divides_nat k nk = 1 k = n of type setprop.
Click to Load Proof
Click to Load Proof
Theorem. (Pi_nat_divides)
∀f : setset, ∀n, nat_p n(in, nat_p (f i))(in, 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 setprop.
Click to Load Proof
Click to Load Proof
Click to Load Proof
Definition. We define primes to be {nω|prime_nat n} of type set.
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.
Click to Load Proof
Click to Load Proof
Click to Load Proof
Theorem. (infiniteRamsey_lem)
∀X, ∀f g f' : setset, infinite X(ZX, infinite Zf Z Z infinite (f Z))(ZX, infinite Zg Z Z g Z f Z)f' 0 = f X(∀m, nat_p mf' (ordsucc m) = f (f' m))(∀m, nat_p mf' 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 : setset, (YX, equip Y nC Y c)HX, ic, infinite H YH, equip Y nC Y = i
Click to Load Proof
End of Section InfiniteRamsey
Definition. We define Inj1 to be In_rec_i (λX f ⇒ {0} {f x|xX}) of type setset.
Theorem. (Inj1_eq)
∀X : set, Inj1 X = {0} {Inj1 x|xX}
Click to Load Proof
Theorem. (Inj1I1)
∀X : set, 0 Inj1 X
Click to Load Proof
Theorem. (Inj1I2)
∀X x : set, x XInj1 x Inj1 X
Click to Load Proof
Theorem. (Inj1E)
∀X y : set, y Inj1 Xy = 0 xX, 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|xX} of type setset.
Theorem. (Inj0I)
∀X x : set, x XInj1 x Inj0 X
Click to Load Proof
Theorem. (Inj0E)
∀X y : set, y Inj0 Xx : set, x X y = Inj1 x
Click to Load Proof
Definition. We define Unj to be In_rec_i (λX f ⇒ {f x|xX {0}}) of type setset.
Theorem. (Unj_eq)
∀X : set, Unj X = {Unj x|xX {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 YX = 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 YX = Y
Click to Load Proof
Theorem. (Inj0_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|xX} {Inj1 y|yY} of type setsetset.
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 XInj0 x X + Y
Click to Load Proof
Theorem. (Inj1_setsum)
∀X Y y : set, y YInj1 y X + Y
Click to Load Proof
Theorem. (setsum_Inj_inv)
∀X Y z : set, z X + Y(xX, z = Inj0 x) (yY, 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|zZ, x : set, Inj0 x = z} of type setset.
Definition. We define proj1 to be λZ ⇒ {Unj z|zZ, y : set, Inj1 y = z} of type setset.
Click to Load Proof
Click to Load Proof
Theorem. (pairI0)
∀X Y x, x Xpair 0 x pair X Y
Click to Load Proof
Theorem. (pairI1)
∀X Y y, y Ypair 1 y pair X Y
Click to Load Proof
Theorem. (pairE)
∀X Y z, z pair X Y(xX, z = pair 0 x) (yY, z = pair 1 y)
Click to Load Proof
Theorem. (pairE0)
∀X Y x, pair 0 x pair X Yx X
Click to Load Proof
Theorem. (pairE1)
∀X Y y, pair 1 y pair X Yy Y
Click to Load Proof
Theorem. (proj0I)
∀w u : set, pair 0 u wu proj0 w
Click to Load Proof
Theorem. (proj0E)
∀w u : set, u proj0 wpair 0 u w
Click to Load Proof
Theorem. (proj1I)
∀w u : set, pair 1 u wu proj1 w
Click to Load Proof
Theorem. (proj1E)
∀w u : set, u proj1 wpair 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 ⇒ xX{pair x y|yY x} of type set(setset)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 : setset, z(xX, 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 : setset, ∀z : set, z (xX, Y x)proj0 z X
Click to Load Proof
Theorem. (proj1_Sigma)
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)proj1 z Y (proj0 z)
Click to Load Proof
Theorem. (pair_Sigma)
∀X : set, ∀Y : setset, xX, yY x, pair x y xX, Y x
Click to Load Proof
Theorem. (pair_Sigma_E1)
∀X : set, ∀Y : setset, ∀x y : set, pair x y (xX, Y x)y Y x
Click to Load Proof
Theorem. (Sigma_E)
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)xX, yY x, z = pair x y
Click to Load Proof
Definition. We define setprod to be λX Y : setxX, Y of type setsetset.
Notation. We use as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.
Let lam : set(setset)setSigma
Definition. We define ap to be λf x ⇒ {proj1 z|zf, y : set, z = pair x y} of type setsetset.
Notation. When x is a set, a term x y is notation for ap x y.
Notation. λ xAB is notation for the set Sigma Ax : set ⇒ B).
Notation. We now use n-tuple notation (a0,...,an-1) for n ≥ 2 for λ i ∈ n . if i = 0 then a0 else ... if i = n-2 then an-2 else an-1.
Theorem. (lamI)
∀X : set, ∀F : setset, xX, yF x, pair x y λxX F x
Click to Load Proof
Theorem. (lamE)
∀X : set, ∀F : setset, ∀z : set, z (λxX F x)xX, yF x, z = pair x y
Click to Load Proof
Theorem. (apI)
∀f x y, pair x y fy f x
Click to Load Proof
Theorem. (apE)
∀f x y, y f xpair x y f
Click to Load Proof
Theorem. (beta)
∀X : set, ∀F : setset, ∀x : set, x X(λxX F x) x = F x
Click to Load Proof
Click to Load Proof
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 : setset, ∀z : set, z (xX, Y x)(z 0) X
Click to Load Proof
Theorem. (ap1_Sigma)
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)(z 1) (Y (z 0))
Click to Load Proof
Definition. We define pair_p to be λu : setpair (u 0) (u 1) = u of type setprop.
Theorem. (pair_p_I)
∀x y, pair_p (pair x y)
Click to Load Proof
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𝒫 (xX, (Y x))|xX, f x Y x} of type set(setset)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 : setset, ∀f : set, (uf, pair_p u u 0 X)(xX, f x Y x)f xX, Y x
Click to Load Proof
Theorem. (lam_Pi)
∀X : set, ∀Y : setset, ∀F : setset, (xX, F x Y x)(λxX F x) (xX, Y x)
Click to Load Proof
Theorem. (ap_Pi)
∀X : set, ∀Y : setset, ∀f : set, ∀x : set, f (xX, Y x)x Xf x Y x
Click to Load Proof
Definition. We define setexp to be λX Y : setyY, X of type setsetset.
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
Click to Load Proof
Click to Load Proof
End of Section Tuples
Theorem. (ReplEq_setprod_ext)
∀X Y, ∀F G : setsetset, (xX, yY, F x y = G x y){F (w 0) (w 1)|wX Y} = {G (w 0) (w 1)|wX Y}
Click to Load Proof
Theorem. (lamI2)
∀X, ∀F : setset, xX, yF x, (x,y) λxX F x
Click to Load Proof
Theorem. (tuple_2_Sigma)
∀X : set, ∀Y : setset, xX, yY x, (x,y) xX, Y x
Click to Load Proof
Theorem. (tuple_2_setprod)
∀X : set, ∀Y : set, xX, yY, (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 : setprop, R x y) (∀y z : setprop, R x yR x zy = z)) of type (set(setprop)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(setprop)prop)setprop.
Theorem. (DescrR_i_io_12)
∀R : set(setprop)prop, (x, (y : setprop, R x y) (∀y z : setprop, R x yR x zy = 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(setprop)(setprop)prop.
Theorem. (PNoEq_ref_)
∀α, ∀p : setprop, PNoEq_ α p p
Click to Load Proof
Theorem. (PNoEq_sym_)
∀α, ∀p q : setprop, PNoEq_ α p qPNoEq_ α q p
Click to Load Proof
Theorem. (PNoEq_tra_)
∀α, ∀p q r : setprop, PNoEq_ α p qPNoEq_ α q rPNoEq_ α p r
Click to Load Proof
Theorem. (PNoEq_antimon_)
∀p q : setprop, ∀α, ordinal αβα, PNoEq_ α p qPNoEq_ β p q
Click to Load Proof
Definition. We define PNoLt_ to be λα p q ⇒ βα, PNoEq_ β p q ¬ p β q β of type set(setprop)(setprop)prop.
Theorem. (PNoLt_E_)
∀α, ∀p q : setprop, PNoLt_ α p q∀R : prop, (∀β, β αPNoEq_ β p q¬ p βq βR)R
Click to Load Proof
Theorem. (PNoLt_irref_)
∀α, ∀p : setprop, ¬ PNoLt_ α p p
Click to Load Proof
Theorem. (PNoLt_mon_)
∀p q : setprop, ∀α, ordinal αβα, PNoLt_ β p qPNoLt_ α p q
Click to Load Proof
Theorem. (PNoLt_trichotomy_or_)
∀p q : setprop, ∀α, 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(setprop)set(setprop)prop.
Theorem. (PNoLtI1)
∀α β, ∀p q : setprop, PNoLt_ (α β) p qPNoLt α p β q
Click to Load Proof
Theorem. (PNoLtI2)
∀α β, ∀p q : setprop, α βPNoEq_ α p qq αPNoLt α p β q
Click to Load Proof
Theorem. (PNoLtI3)
∀α β, ∀p q : setprop, β αPNoEq_ β p q¬ p βPNoLt α p β q
Click to Load Proof
Theorem. (PNoLtE)
∀α β, ∀p q : setprop, PNoLt α p β q∀R : prop, (PNoLt_ (α β) p qR)(α βPNoEq_ α p qq αR)(β αPNoEq_ β p q¬ p βR)R
Click to Load Proof
Theorem. (PNoLt_irref)
∀α, ∀p : setprop, ¬ PNoLt α p α p
Click to Load Proof
Theorem. (PNoLt_trichotomy_or)
∀α β, ∀p q : setprop, ordinal αordinal βPNoLt α p β q α = β PNoEq_ α p q PNoLt β q α p
Click to Load Proof
Theorem. (PNoLtEq_tra)
∀α β, ordinal αordinal β∀p q r : setprop, PNoLt α p β qPNoEq_ β q rPNoLt α p β r
Click to Load Proof
Theorem. (PNoEqLt_tra)
∀α β, ordinal αordinal β∀p q r : setprop, PNoEq_ α p qPNoLt α q β rPNoLt α p β r
Click to Load Proof
Theorem. (PNoLt_tra)
∀α β γ, ordinal αordinal βordinal γ∀p q r : setprop, PNoLt α p β qPNoLt β q γ rPNoLt α p γ r
Click to Load Proof
Definition. We define PNoLe to be λα p β q ⇒ PNoLt α p β q α = β PNoEq_ α p q of type set(setprop)set(setprop)prop.
Theorem. (PNoLeI1)
∀α β, ∀p q : setprop, PNoLt α p β qPNoLe α p β q
Click to Load Proof
Theorem. (PNoLeI2)
∀α, ∀p q : setprop, PNoEq_ α p qPNoLe α p α q
Click to Load Proof
Theorem. (PNoLe_ref)
∀α, ∀p : setprop, PNoLe α p α p
Click to Load Proof
Theorem. (PNoLe_antisym)
∀α β, ordinal αordinal β∀p q : setprop, PNoLe α p β qPNoLe β q α pα = β PNoEq_ α p q
Click to Load Proof
Theorem. (PNoLtLe_tra)
∀α β γ, ordinal αordinal βordinal γ∀p q r : setprop, PNoLt α p β qPNoLe β q γ rPNoLt α p γ r
Click to Load Proof
Theorem. (PNoLeLt_tra)
∀α β γ, ordinal αordinal βordinal γ∀p q r : setprop, PNoLe α p β qPNoLt β q γ rPNoLt α p γ r
Click to Load Proof
Theorem. (PNoEqLe_tra)
∀α β, ordinal αordinal β∀p q r : setprop, PNoEq_ α p qPNoLe α q β rPNoLe α p β r
Click to Load Proof
Theorem. (PNoLe_tra)
∀α β γ, ordinal αordinal βordinal γ∀p q r : setprop, PNoLe α p β qPNoLe β q γ rPNoLe α p γ r
Click to Load Proof
Definition. We define PNo_downc to be λL α p ⇒ β, ordinal β q : setprop, L β q PNoLe α p β q of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_upc to be λR α p ⇒ β, ordinal β q : setprop, R β q PNoLe β q α p of type (set(setprop)prop)set(setprop)prop.
Theorem. (PNoLe_downc)
∀L : set(setprop)prop, ∀α β, ∀p q : setprop, ordinal αordinal βPNo_downc L α pPNoLe β q α pPNo_downc L β q
Click to Load Proof
Theorem. (PNo_downc_ref)
∀L : set(setprop)prop, ∀α, ordinal α∀p : setprop, L α pPNo_downc L α p
Click to Load Proof
Theorem. (PNo_upc_ref)
∀R : set(setprop)prop, ∀α, ordinal α∀p : setprop, R α pPNo_upc R α p
Click to Load Proof
Theorem. (PNoLe_upc)
∀R : set(setprop)prop, ∀α β, ∀p q : setprop, ordinal αordinal βPNo_upc R α pPNoLe α p β qPNo_upc R β q
Click to Load Proof
Definition. We define PNoLt_pwise to be λL R ⇒ ∀γ, ordinal γ∀p : setprop, L γ p∀δ, ordinal δ∀q : setprop, R δ qPNoLt γ p δ q of type (set(setprop)prop)(set(setprop)prop)prop.
Theorem. (PNoLt_pwise_downc_upc)
∀L R : set(setprop)prop, PNoLt_pwise L RPNoLt_pwise (PNo_downc L) (PNo_upc R)
Click to Load Proof
Definition. We define PNo_rel_strict_upperbd to be λL α p ⇒ βα, ∀q : setprop, PNo_downc L β qPNoLt β q α p of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_rel_strict_lowerbd to be λR α p ⇒ βα, ∀q : setprop, PNo_upc R β qPNoLt α p β q of type (set(setprop)prop)set(setprop)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(setprop)prop)(set(setprop)prop)set(setprop)prop.
Theorem. (PNoEq_rel_strict_upperbd)
∀L : set(setprop)prop, ∀α, ordinal α∀p q : setprop, PNoEq_ α p qPNo_rel_strict_upperbd L α pPNo_rel_strict_upperbd L α q
Click to Load Proof
Theorem. (PNo_rel_strict_upperbd_antimon)
∀L : set(setprop)prop, ∀α, ordinal α∀p : setprop, βα, PNo_rel_strict_upperbd L α pPNo_rel_strict_upperbd L β p
Click to Load Proof
Theorem. (PNoEq_rel_strict_lowerbd)
∀R : set(setprop)prop, ∀α, ordinal α∀p q : setprop, PNoEq_ α p qPNo_rel_strict_lowerbd R α pPNo_rel_strict_lowerbd R α q
Click to Load Proof
Theorem. (PNo_rel_strict_lowerbd_antimon)
∀R : set(setprop)prop, ∀α, ordinal α∀p : setprop, βα, PNo_rel_strict_lowerbd R α pPNo_rel_strict_lowerbd R β p
Click to Load Proof
Theorem. (PNoEq_rel_strict_imv)
∀L R : set(setprop)prop, ∀α, ordinal α∀p q : setprop, PNoEq_ α p qPNo_rel_strict_imv L R α pPNo_rel_strict_imv L R α q
Click to Load Proof
Theorem. (PNo_rel_strict_imv_antimon)
∀L R : set(setprop)prop, ∀α, ordinal α∀p : setprop, βα, PNo_rel_strict_imv L R α pPNo_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 : setprop, PNo_rel_strict_imv L R α qPNoEq_ α p q of type (set(setprop)prop)(set(setprop)prop)set(setprop)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(setprop)prop)(set(setprop)prop)set(setprop)prop.
Theorem. (PNo_extend0_eq)
∀α, ∀p : setprop, PNoEq_ α p (λδ ⇒ p δ δ α)
Click to Load Proof
Theorem. (PNo_extend1_eq)
∀α, ∀p : setprop, PNoEq_ α p (λδ ⇒ p δ δ = α)
Click to Load Proof
Theorem. (PNo_rel_imv_ex)
∀L R : set(setprop)prop, PNoLt_pwise L R∀α, ordinal α(p : setprop, PNo_rel_strict_uniq_imv L R α p) (tauα, p : setprop, PNo_rel_strict_split_imv L R tau p)
Click to Load Proof
Definition. We define PNo_lenbdd to be λα L ⇒ ∀β, ∀p : setprop, L β pβ α of type set(set(setprop)prop)prop.
Theorem. (PNo_lenbdd_strict_imv_extend0)
∀L R : set(setprop)prop, ∀α, ordinal αPNo_lenbdd α LPNo_lenbdd α R∀p : setprop, PNo_rel_strict_imv L R α pPNo_rel_strict_imv L R (ordsucc α) (λδ ⇒ p δ δ α)
Click to Load Proof
Theorem. (PNo_lenbdd_strict_imv_extend1)
∀L R : set(setprop)prop, ∀α, ordinal αPNo_lenbdd α LPNo_lenbdd α R∀p : setprop, PNo_rel_strict_imv L R α pPNo_rel_strict_imv L R (ordsucc α) (λδ ⇒ p δ δ = α)
Click to Load Proof
Theorem. (PNo_lenbdd_strict_imv_split)
∀L R : set(setprop)prop, ∀α, ordinal αPNo_lenbdd α LPNo_lenbdd α R∀p : setprop, PNo_rel_strict_imv L R α pPNo_rel_strict_split_imv L R α p
Click to Load Proof
Theorem. (PNo_rel_imv_bdd_ex)
∀L R : set(setprop)prop, PNoLt_pwise L R∀α, ordinal αPNo_lenbdd α LPNo_lenbdd α Rβordsucc α, p : setprop, PNo_rel_strict_split_imv L R β p
Click to Load Proof
Definition. We define PNo_strict_upperbd to be λL α p ⇒ ∀β, ordinal β∀q : setprop, L β qPNoLt β q α p of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_strict_lowerbd to be λR α p ⇒ ∀β, ordinal β∀q : setprop, R β qPNoLt α p β q of type (set(setprop)prop)set(setprop)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(setprop)prop)(set(setprop)prop)set(setprop)prop.
Theorem. (PNoEq_strict_upperbd)
∀L : set(setprop)prop, ∀α, ordinal α∀p q : setprop, PNoEq_ α p qPNo_strict_upperbd L α pPNo_strict_upperbd L α q
Click to Load Proof
Theorem. (PNoEq_strict_lowerbd)
∀R : set(setprop)prop, ∀α, ordinal α∀p q : setprop, PNoEq_ α p qPNo_strict_lowerbd R α pPNo_strict_lowerbd R α q
Click to Load Proof
Theorem. (PNoEq_strict_imv)
∀L R : set(setprop)prop, ∀α, ordinal α∀p q : setprop, PNoEq_ α p qPNo_strict_imv L R α pPNo_strict_imv L R α q
Click to Load Proof
Theorem. (PNo_strict_upperbd_imp_rel_strict_upperbd)
∀L : set(setprop)prop, ∀α, ordinal αβordsucc α, ∀p : setprop, PNo_strict_upperbd L α pPNo_rel_strict_upperbd L β p
Click to Load Proof
Theorem. (PNo_strict_lowerbd_imp_rel_strict_lowerbd)
∀R : set(setprop)prop, ∀α, ordinal αβordsucc α, ∀p : setprop, PNo_strict_lowerbd R α pPNo_rel_strict_lowerbd R β p
Click to Load Proof
Theorem. (PNo_strict_imv_imp_rel_strict_imv)
∀L R : set(setprop)prop, ∀α, ordinal αβordsucc α, ∀p : setprop, PNo_strict_imv L R α pPNo_rel_strict_imv L R β p
Click to Load Proof
Theorem. (PNo_rel_split_imv_imp_strict_imv)
∀L R : set(setprop)prop, ∀α, ordinal α∀p : setprop, PNo_rel_strict_split_imv L R α pPNo_strict_imv L R α p
Click to Load Proof
Theorem. (PNo_lenbdd_strict_imv_ex)
∀L R : set(setprop)prop, PNoLt_pwise L R∀α, ordinal αPNo_lenbdd α LPNo_lenbdd α Rβordsucc α, p : setprop, 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 : setprop, ¬ PNo_strict_imv L R γ q of type (set(setprop)prop)(set(setprop)prop)set(setprop)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(setprop)prop)(set(setprop)prop)set(setprop)prop.
Theorem. (PNo_strict_imv_pred_eq)
∀L R : set(setprop)prop, PNoLt_pwise L R∀α, ordinal α∀p q : setprop, PNo_least_rep L R α pPNo_strict_imv L R α qβα, p β q β
Click to Load Proof
Theorem. (PNo_lenbdd_least_rep2_exuniq2)
∀L R : set(setprop)prop, PNoLt_pwise L R∀α, ordinal αPNo_lenbdd α LPNo_lenbdd α Rβ, (p : setprop, PNo_least_rep2 L R β p) (∀p q : setprop, PNo_least_rep2 L R β pPNo_least_rep2 L R β qp = 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(setprop)prop)(set(setprop)prop)set.
Definition. We define PNo_pred to be λL R ⇒ DescrR_i_io_2 (PNo_least_rep2 L R) of type (set(setprop)prop)(set(setprop)prop)setprop.
Theorem. (PNo_bd_pred_lem)
∀L R : set(setprop)prop, PNoLt_pwise L R∀α, ordinal αPNo_lenbdd α LPNo_lenbdd α RPNo_least_rep2 L R (PNo_bd L R) (PNo_pred L R)
Click to Load Proof
Theorem. (PNo_bd_pred)
∀L R : set(setprop)prop, PNoLt_pwise L R∀α, ordinal αPNo_lenbdd α LPNo_lenbdd α RPNo_least_rep L R (PNo_bd L R) (PNo_pred L R)
Click to Load Proof
Theorem. (PNo_bd_In)
∀L R : set(setprop)prop, PNoLt_pwise L R∀α, ordinal αPNo_lenbdd α LPNo_lenbdd α RPNo_bd L R ordsucc α
Click to Load Proof
Beginning of Section TaggedSets
Let tag : setsetλα ⇒ SetAdjoin α {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
Click to Load Proof
Click to Load Proof
Click to Load Proof
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
Click to Load Proof
Definition. We define SNoElts_ to be λα ⇒ α {β '|βα} of type setset.
Theorem. (SNoElts_mon)
∀α β, α βSNoElts_ α SNoElts_ β
Click to Load Proof
Definition. We define SNo_ to be λα x ⇒ x SNoElts_ α βα, exactly1of2 (β ' x) (β x) of type setsetprop.
Definition. We define PSNo to be λα p ⇒ {βα|p β} {β '|βα, ¬ p β} of type set(setprop)set.
Theorem. (PNoEq_PSNo)
∀α, ordinal α∀p : setprop, PNoEq_ α (λβ ⇒ β PSNo α p) p
Click to Load Proof
Theorem. (SNo_PSNo)
∀α, ordinal α∀p : setprop, SNo_ α (PSNo α p)
Click to Load Proof
Theorem. (SNo_PSNo_eta_)
∀α x, ordinal αSNo_ α xx = PSNo α (λβ ⇒ β x)
Click to Load Proof
Definition. We define SNo to be λx ⇒ α, ordinal α SNo_ α x of type setprop.
Theorem. (SNo_SNo)
∀α, ordinal α∀z, SNo_ α zSNo z
Click to Load Proof
Definition. We define SNoLev to be λx ⇒ Eps_i (λα ⇒ ordinal α SNo_ α x) of type setset.
Theorem. (SNoLev_uniq_Subq)
∀x α β, ordinal αordinal βSNo_ α xSNo_ β xα β
Click to Load Proof
Theorem. (SNoLev_uniq)
∀x α β, ordinal αordinal βSNo_ α xSNo_ β xα = β
Click to Load Proof
Click to Load Proof
Click to Load Proof
Theorem. (SNoLev_)
∀x, SNo xSNo_ (SNoLev x) x
Click to Load Proof
Theorem. (SNo_PSNo_eta)
∀x, SNo xx = PSNo (SNoLev x) (λβ ⇒ β x)
Click to Load Proof
Theorem. (SNoLev_PSNo)
∀α, ordinal α∀p : setprop, SNoLev (PSNo α p) = α
Click to Load Proof
Theorem. (SNo_Subq)
∀x y, SNo xSNo ySNoLev 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 setsetsetprop.
Theorem. (SNoEq_I)
∀α x y, (βα, β x β y)SNoEq_ α x y
Click to Load Proof
Theorem. (SNo_eq)
∀x y, SNo xSNo ySNoLev x = SNoLev ySNoEq_ (SNoLev x) x yx = 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 setsetprop.
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 setsetprop.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Theorem. (SNoLtLe)
∀x y, x < yx y
Click to Load Proof
Theorem. (SNoLeE)
∀x y, SNo xSNo yx yx < y x = y
Click to Load Proof
Theorem. (SNoEq_sym_)
∀α x y, SNoEq_ α x ySNoEq_ α y x
Click to Load Proof
Theorem. (SNoEq_tra_)
∀α x y z, SNoEq_ α x ySNoEq_ α y zSNoEq_ α x z
Click to Load Proof
Theorem. (SNoLtE)
∀x y, SNo xSNo yx < y∀p : prop, (∀z, SNo zSNoLev z SNoLev x SNoLev ySNoEq_ (SNoLev z) z xSNoEq_ (SNoLev z) z yx < zz < ySNoLev z xSNoLev z yp)(SNoLev x SNoLev ySNoEq_ (SNoLev x) x ySNoLev x yp)(SNoLev y SNoLev xSNoEq_ (SNoLev y) x ySNoLev y xp)p
Click to Load Proof
Theorem. (SNoLtI2)
∀x y, SNoLev x SNoLev ySNoEq_ (SNoLev x) x ySNoLev x yx < y
Click to Load Proof
Theorem. (SNoLtI3)
∀x y, SNoLev y SNoLev xSNoEq_ (SNoLev y) x ySNoLev y xx < y
Click to Load Proof
Theorem. (SNoLt_irref)
∀x, ¬ SNoLt x x
Click to Load Proof
Theorem. (SNoLt_trichotomy_or)
∀x y, SNo xSNo yx < y x = y y < x
Click to Load Proof
Theorem. (SNoLt_trichotomy_or_impred)
∀x y, SNo xSNo y∀p : prop, (x < yp)(x = yp)(y < xp)p
Click to Load Proof
Theorem. (SNoLt_tra)
∀x y z, SNo xSNo ySNo zx < yy < zx < z
Click to Load Proof
Theorem. (SNoLe_ref)
∀x, SNoLe x x
Click to Load Proof
Theorem. (SNoLe_antisym)
∀x y, SNo xSNo yx yy xx = y
Click to Load Proof
Theorem. (SNoLtLe_tra)
∀x y z, SNo xSNo ySNo zx < yy zx < z
Click to Load Proof
Theorem. (SNoLeLt_tra)
∀x y z, SNo xSNo ySNo zx yy < zx < z
Click to Load Proof
Theorem. (SNoLe_tra)
∀x y z, SNo xSNo ySNo zx yy zx z
Click to Load Proof
Theorem. (SNoLtLe_or)
∀x y, SNo xSNo yx < y y x
Click to Load Proof
Theorem. (SNoLt_PSNo_PNoLt)
∀α β, ∀p q : setprop, ordinal αordinal βPSNo α p < PSNo β qPNoLt α p β q
Click to Load Proof
Theorem. (PNoLt_SNoLt_PSNo)
∀α β, ∀p q : setprop, ordinal αordinal βPNoLt α p β qPSNo α 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 setsetset.
Definition. We define SNoCutP to be λL R ⇒ (xL, SNo x) (yR, SNo y) (xL, yR, x < y) of type setsetprop.
Theorem. (SNoCutP_SNoCut)
∀L R, SNoCutP L RSNo (SNoCut L R) SNoLev (SNoCut L R) ordsucc ((xLordsucc (SNoLev x)) (yRordsucc (SNoLev y))) (xL, x < SNoCut L R) (yR, SNoCut L R < y) (∀z, SNo z(xL, x < z)(yR, 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 ((xLordsucc (SNoLev x)) (yRordsucc (SNoLev y)))(xL, x < SNoCut L R)(yR, SNoCut L R < y)(∀z, SNo z(xL, x < z)(yR, 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, (xL, SNo x)SNoCutP L 0
Click to Load Proof
Theorem. (SNoCutP_0_0)
Click to Load Proof
Definition. We define SNoS_ to be λα ⇒ {x𝒫 (SNoElts_ α)|βα, SNo_ β x} of type setset.
Theorem. (SNoS_E)
∀α, ordinal αxSNoS_ α, βα, SNo_ β x
Click to Load Proof
Beginning of Section TaggedSets2
Let tag : setsetλα ⇒ SetAdjoin α {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
Theorem. (SNoS_I)
∀α, ordinal α∀x, βα, SNo_ β xx SNoS_ α
Click to Load Proof
Theorem. (SNoS_I2)
∀x y, SNo xSNo ySNoLev x SNoLev yx SNoS_ (SNoLev y)
Click to Load Proof
Theorem. (SNoS_Subq)
∀α β, ordinal αordinal βα βSNoS_ α SNoS_ β
Click to Load Proof
Theorem. (SNoLev_uniq2)
∀α, ordinal α∀x, SNo_ α xSNoLev x = α
Click to Load Proof
Theorem. (SNoS_E2)
∀α, ordinal αxSNoS_ α, ∀p : prop, (SNoLev x αordinal (SNoLev x)SNo xSNo_ (SNoLev x) xp)p
Click to Load Proof
Click to Load Proof
Click to Load Proof
Definition. We define SNoL to be λz ⇒ {xSNoS_ (SNoLev z)|x < z} of type setset.
Definition. We define SNoR to be λz ⇒ {ySNoS_ (SNoLev z)|z < y} of type setset.
Click to Load Proof
Theorem. (SNoL_E)
∀x, SNo xwSNoL x, ∀p : prop, (SNo wSNoLev w SNoLev xw < xp)p
Click to Load Proof
Theorem. (SNoR_E)
∀x, SNo xzSNoR x, ∀p : prop, (SNo zSNoLev z SNoLev xx < zp)p
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Theorem. (SNoL_I)
∀z, SNo z∀x, SNo xSNoLev x SNoLev zx < zx SNoL z
Click to Load Proof
Theorem. (SNoR_I)
∀z, SNo z∀y, SNo ySNoLev y SNoLev zz < yy SNoR z
Click to Load Proof
Theorem. (SNo_eta)
∀z, SNo zz = SNoCut (SNoL z) (SNoR z)
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Theorem. (SNoCutP_SNoCut_fst)
∀L R, SNoCutP L R∀z, SNo z(xL, x < z)(yR, 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 R1SNoCutP L2 R2(wL1, w < SNoCut L2 R2)(zR2, SNoCut L1 R1 < z)SNoCut L1 R1 SNoCut L2 R2
Click to Load Proof
Theorem. (SNoCut_ext)
∀L1 R1 L2 R2, SNoCutP L1 R1SNoCutP L2 R2(wL1, w < SNoCut L2 R2)(zR1, SNoCut L2 R2 < z)(wL2, w < SNoCut L1 R1)(zR2, SNoCut L1 R1 < z)SNoCut L1 R1 = SNoCut L2 R2
Click to Load Proof
Theorem. (SNoLt_SNoL_or_SNoR_impred)
∀x y, SNo xSNo yx < y∀p : prop, (zSNoL y, z SNoR xp)(x SNoL yp)(y SNoR xp)p
Click to Load Proof
Theorem. (SNoL_or_SNoR_impred)
∀x y, SNo xSNo y∀p : prop, (x = yp)(zSNoL y, z SNoR xp)(x SNoL yp)(y SNoR xp)(zSNoR y, z SNoL xp)(x SNoR yp)(y SNoL xp)p
Click to Load Proof
Click to Load Proof
Click to Load Proof
Theorem. (ordinal_SNo_)
∀α, ordinal αSNo_ α α
Click to Load Proof
Click to Load Proof
Click to Load Proof
Theorem. (ordinal_SNoLev_max)
∀α, ordinal α∀z, SNo zSNoLev z αz < α
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Theorem. (ordinal_SNoLev_max_2)
∀α, ordinal α∀z, SNo zSNoLev 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
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Theorem. (pos_low_eq_one)
∀x, SNo x0 < xSNoLev x 1x = 1
Click to Load Proof
Definition. We define SNo_extend0 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λδ ⇒ δ x δ SNoLev x) of type setset.
Definition. We define SNo_extend1 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λδ ⇒ δ x δ = SNoLev x) of type setset.
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Theorem. (SNoLev_0_eq_0)
∀x, SNo xSNoLev x = 0x = 0
Click to Load Proof
Definition. We define eps_ to be λn ⇒ {0} {(ordsucc m) '|mn} of type setset.
Theorem. (eps_ordinal_In_eq_0)
∀n α, ordinal αα eps_ nα = 0
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
End of Section TaggedSets2
Theorem. (SNo_etaE)
∀z, SNo z∀p : prop, (∀L R, SNoCutP L R(xL, SNoLev x SNoLev z)(yR, SNoLev y SNoLev z)z = SNoCut L Rp)p
Click to Load Proof
Theorem. (SNo_ind)
∀P : setprop, (∀L R, SNoCutP L R(xL, P x)(yR, P y)P (SNoCut L R))∀z, SNo zP z
Click to Load Proof
Beginning of Section SurrealRecI
Variable F : set(setset)set
Let default : setEps_i (λ_ ⇒ True)
Let G : set(setsetset)setsetλα g ⇒ If_ii (ordinal α) (λz : setif z SNoS_ (ordsucc α) then F z (λw ⇒ g (SNoLev w) w) else default) (λz : setdefault)
Definition. We define SNo_rec_i to be λz ⇒ In_rec_ii G (SNoLev z) z of type setset.
Hypothesis Fr : ∀z, SNo z∀g h : setset, (wSNoS_ (SNoLev z), g w = h w)F z g = F z h
Click to Load Proof
End of Section SurrealRecI
Beginning of Section SurrealRecII
Variable F : set(set(setset))(setset)
Let default : (setset)Descr_ii (λ_ ⇒ True)
Let G : set(setset(setset))set(setset)λα g ⇒ If_iii (ordinal α) (λz : setIf_ii (z SNoS_ (ordsucc α)) (F z (λw ⇒ g (SNoLev w) w)) default) (λz : setdefault)
Definition. We define SNo_rec_ii to be λz ⇒ In_rec_iii G (SNoLev z) z of type set(setset).
Hypothesis Fr : ∀z, SNo z∀g h : set(setset), (wSNoS_ (SNoLev z), g w = h w)F z g = F z h
Click to Load Proof
End of Section SurrealRecII
Beginning of Section SurrealRec2
Variable F : setset(setsetset)set
Let G : set(setsetset)set(setset)setλw f z g ⇒ F w z (λx y ⇒ if x = w then g y else f x y)
Let H : set(setsetset)setsetλ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 setsetset.
Hypothesis Fr : ∀w, SNo w∀z, SNo z∀g h : setsetset, (xSNoS_ (SNoLev w), ∀y, SNo yg x y = h x y)(ySNoS_ (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 : setsetset, (xSNoS_ (SNoLev w), f x = k x)∀z, SNo z∀g h : setset, (uSNoS_ (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 : setsetset, ∀z, SNo zSNo_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 zSNo_rec2 w z = F w z SNo_rec2
Click to Load Proof
End of Section SurrealRec2
Theorem. (SNo_ordinal_ind)
∀P : setprop, (∀α, ordinal αxSNoS_ α, P x)(∀x, SNo xP x)
Click to Load Proof
Theorem. (SNo_ordinal_ind2)
∀P : setsetprop, (∀α, ordinal α∀β, ordinal βxSNoS_ α, ySNoS_ β, P x y)(∀x y, SNo xSNo yP x y)
Click to Load Proof
Theorem. (SNo_ordinal_ind3)
∀P : setsetsetprop, (∀α, ordinal α∀β, ordinal β∀γ, ordinal γxSNoS_ α, ySNoS_ β, zSNoS_ γ, P x y z)(∀x y z, SNo xSNo ySNo zP x y z)
Click to Load Proof
Theorem. (SNoLev_ind)
∀P : setprop, (∀x, SNo x(wSNoS_ (SNoLev x), P w)P x)(∀x, SNo xP x)
Click to Load Proof
Theorem. (SNoLev_ind2)
∀P : setsetprop, (∀x y, SNo xSNo y(wSNoS_ (SNoLev x), P w y)(zSNoS_ (SNoLev y), P x z)(wSNoS_ (SNoLev x), zSNoS_ (SNoLev y), P w z)P x y)∀x y, SNo xSNo yP x y
Click to Load Proof
Theorem. (SNoLev_ind3)
∀P : setsetsetprop, (∀x y z, SNo xSNo ySNo z(uSNoS_ (SNoLev x), P u y z)(vSNoS_ (SNoLev y), P x v z)(wSNoS_ (SNoLev z), P x y w)(uSNoS_ (SNoLev x), vSNoS_ (SNoLev y), P u v z)(uSNoS_ (SNoLev x), wSNoS_ (SNoLev z), P u y w)(vSNoS_ (SNoLev y), wSNoS_ (SNoLev z), P x v w)(uSNoS_ (SNoLev x), vSNoS_ (SNoLev y), wSNoS_ (SNoLev z), P u v w)P x y z)∀x y z, SNo xSNo ySNo zP x y z
Click to Load Proof
Theorem. (SNo_omega)
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 xx = SNo_extend0 x SNoElts_ (SNoLev x)
Click to Load Proof
Theorem. (SNo_extend1_restr_eq)
∀x, SNo xx = 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|zSNoR x} {m w|wSNoL x}) of type setset.
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.
Click to Load Proof
Click to Load Proof
Theorem. (SNo_minus_SNo)
∀x, SNo xSNo (- x)
Click to Load Proof
Theorem. (minus_SNo_Lt_contra)
∀x y, SNo xSNo yx < y- y < - x
Click to Load Proof
Theorem. (minus_SNo_Le_contra)
∀x y, SNo xSNo yx y- y - x
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Theorem. (minus_SNo_invol)
∀x, SNo x- - x = x
Click to Load Proof
Click to Load Proof
Theorem. (minus_SNo_SNo_)
∀α, ordinal α∀x, SNo_ α xSNo_ α (- 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 Rv = SNoCut L R- v = SNoCut {- z|zR} {- w|wL}
Click to Load Proof
Click to Load Proof
Theorem. (minus_SNo_Lt_contra1)
∀x y, SNo xSNo y- x < y- y < x
Click to Load Proof
Theorem. (minus_SNo_Lt_contra2)
∀x y, SNo xSNo yx < - yy < - x
Click to Load Proof
Theorem. (mordinal_SNoLev_min_2)
∀α, ordinal α∀z, SNo zSNoLev z ordsucc α- α z
Click to Load Proof
Click to Load Proof
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|wSNoL x} {a x w|wSNoL y}) ({a z y|zSNoR x} {a x z|zSNoR y})) of type setsetset.
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 yx + y = SNoCut ({w + y|wSNoL x} {x + w|wSNoL y}) ({z + y|zSNoR x} {x + z|zSNoR y})
Click to Load Proof
Theorem. (add_SNo_prop1)
∀x y, SNo xSNo ySNo (x + y) (uSNoL x, u + y < x + y) (uSNoR x, x + y < u + y) (uSNoL y, x + u < x + y) (uSNoR y, x + y < x + u) SNoCutP ({w + y|wSNoL x} {x + w|wSNoL y}) ({z + y|zSNoR x} {x + z|zSNoR y})
Click to Load Proof
Theorem. (SNo_add_SNo)
∀x y, SNo xSNo ySNo (x + y)
Click to Load Proof
Theorem. (SNo_add_SNo_3)
∀x y z, SNo xSNo ySNo zSNo (x + y + z)
Click to Load Proof
Theorem. (SNo_add_SNo_3c)
∀x y z, SNo xSNo ySNo zSNo (x + y + - z)
Click to Load Proof
Theorem. (SNo_add_SNo_4)
∀x y z w, SNo xSNo ySNo zSNo wSNo (x + y + z + w)
Click to Load Proof
Theorem. (add_SNo_Lt1)
∀x y z, SNo xSNo ySNo zx < zx + y < z + y
Click to Load Proof
Theorem. (add_SNo_Le1)
∀x y z, SNo xSNo ySNo zx zx + y z + y
Click to Load Proof
Theorem. (add_SNo_Lt2)
∀x y z, SNo xSNo ySNo zy < zx + y < x + z
Click to Load Proof
Theorem. (add_SNo_Le2)
∀x y z, SNo xSNo ySNo zy zx + y x + z
Click to Load Proof
Theorem. (add_SNo_Lt3a)
∀x y z w, SNo xSNo ySNo zSNo wx < zy wx + y < z + w
Click to Load Proof
Theorem. (add_SNo_Lt3b)
∀x y z w, SNo xSNo ySNo zSNo wx zy < wx + y < z + w
Click to Load Proof
Theorem. (add_SNo_Lt3)
∀x y z w, SNo xSNo ySNo zSNo wx < zy < wx + y < z + w
Click to Load Proof
Theorem. (add_SNo_Le3)
∀x y z w, SNo xSNo ySNo zSNo wx zy wx + y z + w
Click to Load Proof
Click to Load Proof
Theorem. (add_SNo_com)
∀x y, SNo xSNo yx + y = y + x
Click to Load Proof
Theorem. (add_SNo_0L)
∀x, SNo x0 + x = x
Click to Load Proof
Theorem. (add_SNo_0R)
∀x, SNo xx + 0 = x
Click to Load Proof
Click to Load Proof
Click to Load Proof
Click to Load Proof
Theorem. (add_SNo_ordinal_eq)
∀α, ordinal α∀β, ordinal βα + β = SNoCut ({x + β|xSNoS_ α} {α + x|xSNoS_ β}) 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
Click to Load Proof
Click to Load Proof
Click to Load Proof