## 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 ()
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.
Definition. We define and to be λA B : prop∀p : prop, (ABp)p of type proppropprop.
Definition. We define or to be λA B : prop∀p : prop, (Ap)(Bp)p of type proppropprop.
Definition. We define iff to be λA B : propand (AB) (BA) of type proppropprop.
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
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
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,
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.
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 : set 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
Axiom. (UnivOf_TransSet) We take the following as an axiom:
∀N : set, TransSet ()
Axiom. (UnivOf_ZF_closed) We take the following as an axiom:
∀N : set, ZF_closed ()
Axiom. (UnivOf_Min) We take the following as an axiom:
∀N U : set, N U U

## First Theorems Up To Excluded Middle

Theorem. (andI)
∀A B : prop, ABA B
Theorem. (orIL)
∀A B : prop, AA B
Theorem. (orIR)
∀A B : prop, BA B
Theorem. (iffI)
∀A B : prop, (AB)(BA)(A B)
Theorem. (pred_ext)
∀P Q : setprop, (∀x, P x Q x)P = Q
Definition. We define nIn to be λx X ⇒ ¬ In x X of type setsetprop.
Theorem. (EmptyE)
∀x : set,
Theorem. (PowerI)
∀X Y : set, Y XY 𝒫 X
Theorem. (Subq_Empty)
∀X : set,
Theorem. (Empty_In_Power)
∀X : set, Empty 𝒫 X
Theorem. (xm)
∀P : prop, P ¬ P

## The Rest of the Development

Theorem. (FalseE)
False∀p : prop, p
Theorem. (andEL)
∀A B : prop, A BA
Theorem. (andER)
∀A B : prop, A BB
Beginning of Section PropN
Variable P1 P2 P3 : prop
Theorem. (and3I)
P1P2P3P1 P2 P3
Theorem. (and3E)
P1 P2 P3(∀p : prop, (P1P2P3p)p)
Theorem. (or3I1)
P1P1 P2 P3
Theorem. (or3I2)
P2P1 P2 P3
Theorem. (or3I3)
P3P1 P2 P3
Theorem. (or3E)
P1 P2 P3(∀p : prop, (P1p)(P2p)(P3p)p)
Variable P4 : prop
Theorem. (and4I)
P1P2P3P4P1 P2 P3 P4
Variable P5 : prop
Theorem. (and5I)
P1P2P3P4P5P1 P2 P3 P4 P5
Variable P6 : prop
Theorem. (and6I)
P1P2P3P4P5P6P1 P2 P3 P4 P5 P6
Variable P7 : prop
Theorem. (and7I)
P1P2P3P4P5P6P7P1 P2 P3 P4 P5 P6 P7
End of Section PropN
Theorem. (not_or_and_demorgan)
∀A B : prop, ¬ (A B)¬ A ¬ B
Theorem. (not_ex_all_demorgan_i)
∀P : setprop, (¬ x, P x)∀x, ¬ P x
Theorem. (iffEL)
∀A B : prop, (A B)AB
Theorem. (iffER)
∀A B : prop, (A B)BA
Theorem. (iff_refl)
∀A : prop, A A
Theorem. (iff_sym)
∀A B : prop, (A B)(B A)
Theorem. (iff_trans)
∀A B C : prop, (A B)(B C)(A C)
Theorem. (eq_i_tra)
∀x y z, x = yy = zx = z
Theorem. (neq_i_sym)
∀x y, x yy x
Theorem. (Eps_i_ex)
∀P : setprop, (x, P x)P ()
Theorem. (prop_ext_2)
∀p q : prop, (pq)(qp)p = q
Theorem. (Subq_ref)
∀X : set, X X
Theorem. (Subq_tra)
∀X Y Z : set, X YY ZX Z
Theorem. (Empty_Subq_eq)
∀X : set,
Theorem. (Empty_eq)
∀X : set, (∀x, x X)
Theorem. (UnionI)
∀X x Y : set, x YY Xx X
Theorem. (UnionE)
∀X x : set, x XY : set, x Y Y X
Theorem. (UnionE_impred)
∀X x : set, x X∀p : prop, (∀Y : set, x YY Xp)p
Theorem. (PowerE)
∀X Y : set, Y 𝒫 XY X
Theorem. (Self_In_Power)
∀X : set, X 𝒫 X
Theorem. (dneg)
∀P : prop, ¬ ¬ PP
Theorem. (not_all_ex_demorgan_i)
∀P : setprop, ¬ (∀x, P x)x, ¬ P x
Theorem. (eq_or_nand)
or = (λx y : prop¬ (¬ x ¬ y))
Definition. We define exactly1of2 to be λA B : propA ¬ B ¬ A B of type proppropprop.
Theorem. (exactly1of2_I1)
∀A B : prop, A¬ B B
Theorem. (exactly1of2_I2)
∀A B : prop, ¬ AB B
Theorem. (exactly1of2_E)
∀A B : prop, B∀p : prop, (A¬ Bp)(¬ ABp)p
Theorem. (exactly1of2_or)
∀A B : prop, BA B
Theorem. (ReplI)
∀A : set, ∀F : setset, ∀x : set, x AF x {F x|xA}
Theorem. (ReplE)
∀A : set, ∀F : setset, ∀y : set, y {F x|xA}xA, y = F x
Theorem. (ReplE_impred)
∀A : set, ∀F : setset, ∀y : set, y {F x|xA}∀p : prop, (∀x : set, x Ay = F xp)p
Theorem. (ReplE')
∀X, ∀f : setset, ∀p : setprop, (xX, p (f x))y{f x|xX}, p y
Theorem. (Repl_Empty)
∀F : setset, {F x|xEmpty} = Empty
Theorem. (ReplEq_ext_sub)
∀X, ∀F G : setset, (xX, F x = G x){F x|xX} {G x|xX}
Theorem. (ReplEq_ext)
∀X, ∀F G : setset, (xX, F x = G x){F x|xX} = {G x|xX}
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
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
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
Theorem. (If_i_0)
∀p : prop, ∀x y : set, ¬ p(if p then x else y) = y
Theorem. (If_i_1)
∀p : prop, ∀x y : set, p(if p then x else y) = x
Theorem. (If_i_or)
∀p : prop, ∀x y : set, (if p then x else y) = x (if p then x else y) = y
Definition. We define UPair to be λy z ⇒ {if then y else z|X𝒫 ()} of type setsetset.
Theorem. (UPairE)
∀x y z : set, x {y,z}x = y x = z
Theorem. (UPairI1)
∀y z : set, y {y,z}
Theorem. (UPairI2)
∀y z : set, z {y,z}
Definition. We define Sing to be λx ⇒ {x,x} of type setset.
Theorem. (SingI)
∀x : set, x {x}
Theorem. (SingE)
∀x y : set, y {x}y = x
Definition. We define binunion to be λX Y ⇒ {X,Y} of type setsetset.
Theorem. (binunionI1)
∀X Y z : set, z Xz X Y
Theorem. (binunionI2)
∀X Y z : set, z Yz X Y
Theorem. (binunionE)
∀X Y z : set, z X Yz X z Y
Theorem. (binunionE')
∀X Y z, ∀p : prop, (z Xp)(z Yp)(z X Yp)
Theorem. (binunion_asso)
∀X Y Z : set, X (Y Z) = (X Y) Z
Theorem. (binunion_com_Subq)
∀X Y : set, X Y Y X
Theorem. (binunion_com)
∀X Y : set, X Y = Y X
Theorem. (binunion_idl)
∀X : set, = X
Theorem. (binunion_idr)
∀X : set, = X
Theorem. (binunion_Subq_1)
∀X Y : set, X X Y
Theorem. (binunion_Subq_2)
∀X Y : set, Y X Y
Theorem. (binunion_Subq_min)
∀X Y Z : set, X ZY ZX Y Z
Theorem. (Subq_binunion_eq)
∀X Y, (X Y) = (X Y = Y)
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.
Theorem. (famunionI)
∀X : set, ∀F : (setset), ∀x y : set, x Xy F xy xXF x
Theorem. (famunionE)
∀X : set, ∀F : (setset), ∀y : set, y (xXF x)xX, y F x
Theorem. (famunionE_impred)
∀X : set, ∀F : (setset), ∀y : set, y (xXF x)∀p : prop, (∀x, x Xy F xp)p
Theorem. (famunion_Empty)
∀F : setset, (xEmptyF x) = Empty
Theorem. (famunion_Subq)
∀X, ∀f g : setset, (xX, f x g x) f g
Theorem. (famunion_ext)
∀X, ∀f g : setset, (xX, f x = g x) f = g
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
Theorem. (SepI)
∀X : set, ∀P : (setprop), ∀x : set, x XP xx {xX|P x}
Theorem. (SepE)
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}x X P x
Theorem. (SepE1)
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}x X
Theorem. (SepE2)
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}P x
Theorem. (Sep_Empty)
∀P : setprop, {xEmpty|P x} = Empty
Theorem. (Sep_Subq)
∀X : set, ∀P : setprop, {xX|P x} X
Theorem. (Sep_In_Power)
∀X : set, ∀P : setprop, {xX|P x} 𝒫 X
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}
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
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
Definition. We define binintersect to be λX Y ⇒ {xX|x Y} of type setsetset.
Theorem. (binintersectI)
∀X Y z, z Xz Yz X Y
Theorem. (binintersectE)
∀X Y z, z X Yz X z Y
Theorem. (binintersectE1)
∀X Y z, z X Yz X
Theorem. (binintersectE2)
∀X Y z, z X Yz Y
Theorem. (binintersect_Subq_1)
∀X Y : set, X Y X
Theorem. (binintersect_Subq_2)
∀X Y : set, X Y Y
Theorem. (binintersect_Subq_eq_1)
∀X Y, X YX Y = X
Theorem. (binintersect_Subq_max)
∀X Y Z : set, Z XZ YZ X Y
Theorem. (binintersect_com_Subq)
∀X Y : set, X Y Y X
Theorem. (binintersect_com)
∀X Y : set, X Y = Y X
Definition. We define setminus to be λX Y ⇒ Sep X (λx ⇒ x Y) of type setsetset.
Theorem. (setminusI)
∀X Y z, (z X)(z Y)z X Y
Theorem. (setminusE)
∀X Y z, (z X Y)z X z Y
Theorem. (setminusE1)
∀X Y z, (z X Y)z X
Theorem. (setminusE2)
∀X Y z, (z X Y)z Y
Theorem. (setminus_Subq)
∀X Y : set, X Y X
Theorem. (setminus_In_Power)
∀A U, A U 𝒫 A
Theorem. (binunion_remove1_eq)
∀X, xX, X = (X {x}) {x}
Theorem. (In_irref)
∀x, x x
Theorem. (In_no2cycle)
∀x y, x yy xFalse
Definition. We define ordsucc to be λx : setx {x} of type setset.
Theorem. (ordsuccI1)
∀x : set, x
Theorem. (ordsuccI2)
∀x : set, x
Theorem. (ordsuccE)
∀x y : set, y y x y = x
Notation. Natural numbers 0,1,2,... are notation for the terms formed using Empty as 0 and forming successors with ordsucc.
Theorem. (neq_0_ordsucc)
∀a : set,
Theorem. (neq_ordsucc_0)
∀a : set,
Theorem. (ordsucc_inj)
∀a b : set, = a = b
Theorem. (In_0_1)
Theorem. (In_0_2)
Theorem. (In_1_2)
Definition. We define nat_p to be λn : set∀p : setprop, p 0(∀x : set, p xp ())p n of type setprop.
Theorem. (nat_ordsucc)
∀n : set, nat_p ()
Theorem. (nat_0_in_ordsucc)
∀n,
Theorem. (nat_ordsucc_in_ordsucc)
∀n, mn,
Theorem. (nat_ind)
∀p : setprop, p 0(∀n, p np ())∀n, p n
Theorem. (nat_complete_ind)
∀p : setprop, (∀n, (mn, p m)p n)∀n, p n
Theorem. (nat_inv_impred)
∀p : setprop, p 0(∀n, p ())∀n, p n
Theorem. (nat_inv)
∀n, n = 0 x, n =
Theorem. (nat_p_trans)
∀n, mn,
Theorem. (nat_trans)
∀n, mn, m n
Theorem. (nat_ordsucc_trans)
∀n, m, m n
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
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
Theorem. (injI)
∀X Y, ∀f : setset, (xX, f x Y)(x zX, f x = f zx = z)inj X Y f
Theorem. (inj_comp)
∀X Y Z : set, ∀f g : setset, inj X Y finj Y Z ginj X Z (λx ⇒ g (f x))
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
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
Theorem. (bij_inj)
∀X Y, ∀f : setset, bij X Y finj X Y f
Theorem. (bij_id)
∀X, bij X X (λx ⇒ x)
Theorem. (bij_comp)
∀X Y Z : set, ∀f g : setset, bij X Y fbij Y Z gbij X Z (λx ⇒ g (f x))
Theorem. (bij_surj)
∀X Y, ∀f : setset, bij X Y fsurj X Y f
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
Theorem. (inj_linv)
∀X, ∀f : setset, (u vX, f u = f vu = v)xX, inv X f (f x) = x
Theorem. (bij_inv)
∀X Y, ∀f : setset, bij X Y fbij Y X (inv X f)
Definition. We define atleastp to be λX Y : setf : setset, inj X Y f of type setsetprop.
Theorem. (atleastp_tra)
∀X Y Z, Y Z Z
Theorem. (Subq_atleastp)
∀X Y, X Y Y
Definition. We define equip to be λX Y : setf : setset, bij X Y f of type setsetprop.
Theorem. (equip_atleastp)
∀X Y, Y Y
Theorem. (equip_ref)
∀X, X
Theorem. (equip_sym)
∀X Y, Y X
Theorem. (equip_tra)
∀X Y Z, Y Z Z
Theorem. (equip_0_Empty)
∀X, 0X = 0
∀N X y, y X Xequip () (X {y})
Theorem. (equip_ordsucc_remove1)
∀X N, xX, ()equip (X {x}) N
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
Theorem. (image_In_Power)
∀A B, ∀f : setset, (xA, f x B)U𝒫 A, {f x|xU} 𝒫 B
Theorem. (image_monotone)
∀f : setset, ∀U V, U V{f x|xU} {f x|xV}
Theorem. (setminus_antimonotone)
∀A U V, U VA V A U
Theorem. (SchroederBernstein)
∀A B, ∀f g : setset, inj A B finj B A g B
Theorem. (atleastp_antisym_equip)
∀A B, B A B
End of Section SchroederBernstein
Beginning of Section PigeonHole
Theorem. (PigeonHole_nat)
∀n, ∀f : setset, (i, f i n)¬ (i j, f i = f ji = j)
End of Section PigeonHole
Theorem. (Union_ordsucc_eq)
∀n, () = n
Theorem. (cases_1)
i1, ∀p : setprop, p 0p i
Theorem. (cases_2)
i2, ∀p : setprop, p 0p 1p i
Definition. We define ordinal to be λα : set βα, of type setprop.
Theorem. (ordinal_TransSet)
∀α : set,
Theorem. (ordinal_Hered)
∀α : set, βα,
Theorem. (TransSet_ordsucc)
∀X : set, TransSet ()
Theorem. (ordinal_ordsucc)
∀α : set, ordinal ()
Theorem. (nat_p_ordinal)
∀n : set,
Theorem. (TransSet_ordsucc_In_Subq)
∀X : set, xX, X
Theorem. (ordinal_ordsucc_In_Subq)
∀α, βα, α
Theorem. (ordinal_trichotomy_or)
∀α β : set, α β α = β β α
Theorem. (ordinal_trichotomy_or_impred)
∀α β : set, ∀p : prop, (α βp)(α = βp)(β αp)p
Theorem. (ordinal_In_Or_Subq)
∀α β, α β β α
Theorem. (ordinal_linear)
∀α β, α β β α
Theorem. (ordinal_ordsucc_In_eq)
∀α β, β α α α =
Theorem. (ordinal_lim_or_succ)
∀α, (βα, α) (βα, α = )
Theorem. (ordinal_ordsucc_In)
∀α, βα,
Theorem. (ordinal_famunion)
∀X, ∀F : setset, (xX, ordinal (F x))ordinal (xXF x)
Theorem. (ordinal_binintersect)
∀α β, ordinal (α β)
Theorem. (ordinal_binunion)
∀α β, ordinal (α β)
Theorem. (ordinal_ind)
∀p : setprop, (∀α, (βα, p β)p α)∀α, p α
Theorem. (least_ordinal_ex)
∀p : setprop, (α, p α)α, p α βα, ¬ p β
Theorem. (equip_Sing_1)
∀x, 1
Theorem. (TransSet_In_ordsucc_Subq)
∀x y, x x y
Theorem. (exandE_i)
∀P Q : setprop, (x, P x Q x)∀r : prop, (∀x, P xQ xr)r
Theorem. (exandE_ii)
∀P Q : (setset)prop, (x : setset, P x Q x)∀p : prop, (∀x : setset, P xQ xp)p
Theorem. (exandE_iii)
∀P Q : (setsetset)prop, (x : setsetset, P x Q x)∀p : prop, (∀x : setsetset, P xQ xp)p
Theorem. (exandE_iiii)
∀P Q : (setsetsetset)prop, (x : setsetsetset, P x Q x)∀p : prop, (∀x : setsetsetset, P xQ xp)p
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
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
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
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.
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.
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 () of type setset.
Theorem. (In_rec_i_G_c)
∀X : set, ∀f : setset, (xX, (f x)) (F X f)
Theorem. (In_rec_i_G_inv)
∀X : set, ∀Y : set, Yf : setset, (xX, (f x)) Y = F X f
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, Y ZY = Z
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 ⇒ of type set(setset).
Theorem. (In_rec_G_ii_c)
∀X : set, ∀f : set(setset), (xX, (f x)) (F X f)
Theorem. (In_rec_G_ii_inv)
∀X : set, ∀Y : (setset), Yf : set(setset), (xX, (f x)) Y = F X f
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), Y ZY = Z
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 ⇒ of type set(setsetset).
Theorem. (In_rec_G_iii_c)
∀X : set, ∀f : set(setsetset), (xX, (f x)) (F X f)
Theorem. (In_rec_G_iii_inv)
∀X : set, ∀Y : (setsetset), Yf : set(setsetset), (xX, (f x)) Y = F X f
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), Y ZY = Z
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 of type setset.
Theorem. (nat_primrec_r)
∀X : set, ∀g h : setset, (xX, g x = h x)F X g = F X h
Theorem. (nat_primrec_S)
∀n : set, = f n ()
End of Section NatRec
Definition. We define add_nat to be λn m : set (λ_ r ⇒ ) m of type setsetset.
∀n : set, n + 0 = n
∀n m : set, n + = ordsucc (n + m)
∀n : set, ∀m : set, nat_p (n + m)
∀n : set, ∀m : set, ∀k : set, (n + m) + k = n + (m + k)
∀m : set, 0 + m = m
∀n : set, ∀m : set, + m = ordsucc (n + m)
∀n : set, ∀m : set, n + m = m + n
∀m, km, ∀n, k + n m + n
∀n, ∀m, km, n + k n + m
∀k, ∀m, k m∀n, k + n m + n
∀n, ∀k, ∀m, k mn + k n + m
∀m, ∀n, m m + n
∀n, ∀m, n mk, m = k + n
∀k, ∀m, ∀n, k + n = m + nk = m
Beginning of Section NatMul
Definition. We define mul_nat to be λn m : set (λ_ r ⇒ n + r) m of type setsetset.
Theorem. (mul_nat_0R)
∀n : set, n * 0 = 0
Theorem. (mul_nat_SR)
∀n m, n * = n + n * m
Theorem. (mul_nat_p)
∀n : set, ∀m : set, nat_p (n * m)
Theorem. (mul_nat_0L)
∀m : set, 0 * m = 0
Theorem. (mul_nat_SL)
∀n : set, ∀m : set, * m = n * m + m
Theorem. (mul_nat_com)
∀n : set, ∀m : set, n * m = m * n
∀n : set, ∀m : set, ∀k : set, n * (m + k) = n * m + n * k
Theorem. (mul_nat_asso)
∀n : set, ∀m : set, ∀k : set, (n * m) * k = n * (m * k)
Theorem. (mul_nat_Subq_R)
∀m n, m n∀k, m * k n * k
Theorem. (mul_nat_Subq_L)
∀m n, m n∀k, k * m k * n
Theorem. (mul_nat_0_or_Subq)
∀m, ∀n, n = 0 m m * n
Theorem. (mul_nat_0_inv)
∀m, ∀n, m * n = 0m = 0 n = 0
Theorem. (mul_nat_0m_1n_In)
∀m, ∀n, 0 m1 nm m * n
Theorem. (nat_le1_cases)
∀m, m 1m = 0 m = 1
Definition. We define Pi_nat to be λf n ⇒ (λi r ⇒ r * f i) n of type (setset)setset.
Theorem. (Pi_nat_0)
∀f : setset, 0 = 1
Theorem. (Pi_nat_S)
∀f : setset, ∀n, () = n * f n
Theorem. (Pi_nat_p)
∀f : setset, ∀n, (in, nat_p (f i))nat_p ( n)
Theorem. (Pi_nat_0_inv)
∀f : setset, ∀n, (in, nat_p (f i)) n = 0(in, f i = 0)
Definition. We define exp_nat to be λn m : set (λ_ r ⇒ n * r) m of type setsetset.
Theorem. (exp_nat_S)
∀n m, n ^ () = n * n ^ m
Theorem. (exp_nat_p)
∀n, ∀m, nat_p (n ^ m)
End of Section NatMul
Beginning of Section form100_52
Theorem. (equip_finite_Power)
∀n, ∀X, nequip (𝒫 X) (2 ^ n)
End of Section form100_52
Theorem. (ZF_closed_E)
∀U, ∀p : prop, (p)p
Theorem. (ZF_Union_closed)
∀U, XU, X U
Theorem. (ZF_Power_closed)
∀U, XU, 𝒫 X U
Theorem. (ZF_Repl_closed)
∀U, XU, ∀F : setset, (xX, F x U){F x|xX} U
Theorem. (ZF_UPair_closed)
∀U, x yU, {x,y} U
Theorem. (ZF_Sing_closed)
∀U, xU, {x} U
Theorem. (ZF_binunion_closed)
∀U, X YU, (X Y) U
Theorem. (ZF_ordsucc_closed)
∀U, xU, U
Theorem. (nat_p_UnivOf_Empty)
∀n : set,
Definition. We define ω to be of type set.
Theorem. (omega_nat_p)
Theorem. (nat_p_omega)
∀n : set, n ω
Theorem. (omega_ordsucc)
Theorem. (form100_22_v2)
∀f : setset, ¬ inj () ω f
Theorem. (form100_22_v3)
∀g : setset, ¬ () g
Definition. We define finite to be λX ⇒ nω, n of type setprop.
Theorem. (nat_finite)
∀n,
Theorem. (finite_ind)
∀p : setprop, (∀X y, y Xp Xp (X {y}))∀X, p X
Theorem. (Sing_finite)
∀x,
∀X y, finite (X {y})
Theorem. (binunion_finite)
∀X, ∀Y, finite (X Y)
Theorem. (famunion_nat_finite)
∀X : setset, ∀n, (in, finite (X i))finite (inX i)
Theorem. (Subq_finite)
∀X, ∀Y, Y X
Definition. We define infinite to be λA ⇒ ¬ of type setprop.
Beginning of Section InfinitePrimes
Definition. We define divides_nat to be λm n ⇒ m ω n ω kω, m * k = n of type setsetprop.
Theorem. (divides_nat_tra)
∀k m n, m n n
Definition. We define prime_nat to be λn ⇒ n ω 1 n kω, nk = 1 k = n of type setprop.
Theorem. (Pi_nat_divides)
∀f : setset, ∀n, (in, nat_p (f i))(in, divides_nat (f i) ( n))
Definition. We define composite_nat to be λn ⇒ n ω k mω, 1 k 1 m k * m = n of type setprop.
Definition. We define primes to be of type set.
End of Section InfinitePrimes
Beginning of Section InfiniteRamsey
Theorem. (infiniteRamsey_lem)
∀X, ∀f g f' : setset, (ZX, f Z Z infinite (f Z))(ZX, g Z Z g Z f Z)f' 0 = f X(∀m, f' () = f (f' m))(∀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')
Theorem. (infiniteRamsey)
∀c, ∀n, ∀X, ∀C : setset, (YX, nC Y c)HX, ic, YH, nC Y = i
End of Section InfiniteRamsey
Definition. We define Inj1 to be In_rec_i (λX f ⇒ {f x|xX}) of type setset.
Theorem. (Inj1_eq)
∀X : set, Inj1 X = {Inj1 x|xX}
Theorem. (Inj1I1)
∀X : set, 0 Inj1 X
Theorem. (Inj1I2)
∀X x : set, x XInj1 x Inj1 X
Theorem. (Inj1E)
∀X y : set, y Inj1 Xy = 0 xX, y = Inj1 x
Theorem. (Inj1NE1)
∀x : set, Inj1 x 0
Theorem. (Inj1NE2)
∀x : set, Inj1 x
Definition. We define Inj0 to be λX ⇒ {Inj1 x|xX} of type setset.
Theorem. (Inj0I)
∀X x : set, x XInj1 x Inj0 X
Theorem. (Inj0E)
∀X y : set, y Inj0 Xx : set, x X y = Inj1 x
Definition. We define Unj to be In_rec_i (λX f ⇒ {f x|xX }) of type setset.
Theorem. (Unj_eq)
∀X : set, Unj X = {Unj x|xX }
Theorem. (Unj_Inj1_eq)
∀X : set, Unj (Inj1 X) = X
Theorem. (Inj1_inj)
∀X Y : set, Inj1 X = Inj1 YX = Y
Theorem. (Unj_Inj0_eq)
∀X : set, Unj (Inj0 X) = X
Theorem. (Inj0_inj)
∀X Y : set, Inj0 X = Inj0 YX = Y
Theorem. (Inj0_Inj1_neq)
∀X Y : set, Inj0 X Inj1 Y
Definition. We define setsum to be λX Y ⇒ {Inj0 x|xX} {Inj1 y|yY} of type setsetset.
Theorem. (Inj0_setsum)
∀X Y x : set, x XInj0 x X + Y
Theorem. (Inj1_setsum)
∀X Y y : set, y YInj1 y X + Y
Theorem. (setsum_Inj_inv)
∀X Y z : set, z X + Y(xX, z = Inj0 x) (yY, z = Inj1 y)
Theorem. (Inj0_setsum_0L)
∀X : set, 0 + X = Inj0 X
Theorem. (Inj1_setsum_1L)
∀X : set, 1 + X = Inj1 X
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.
Theorem. (pairI0)
∀X Y x, x Xpair 0 x pair X Y
Theorem. (pairI1)
∀X Y y, y Ypair 1 y pair X Y
Theorem. (pairE)
∀X Y z, z pair X Y(xX, z = pair 0 x) (yY, z = pair 1 y)
Theorem. (pairE0)
∀X Y x, pair 0 x pair X Yx X
Theorem. (pairE1)
∀X Y y, pair 1 y pair X Yy Y
Theorem. (proj0I)
∀w u : set, pair 0 u wu
Theorem. (proj0E)
∀w u : set, u pair 0 u w
Theorem. (proj1I)
∀w u : set, pair 1 u wu
Theorem. (proj1E)
∀w u : set, u pair 1 u w
Theorem. (proj0_pair_eq)
∀X Y : set, proj0 (pair X Y) = X
Theorem. (proj1_pair_eq)
∀X Y : set, proj1 (pair X Y) = Y
Definition. We define Sigma to be λX Y ⇒ xX{pair x y|yY x} of type set(setset)set.
Theorem. (Sigma_eta_proj0_proj1)
∀X : set, ∀Y : setset, z(xX, Y x), pair () () = z X Y ()
Theorem. (proj0_Sigma)
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x) X
Theorem. (proj1_Sigma)
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x) Y ()
Theorem. (pair_Sigma)
∀X : set, ∀Y : setset, xX, yY x, pair x y xX, Y x
Theorem. (pair_Sigma_E1)
∀X : set, ∀Y : setset, ∀x y : set, pair x y (xX, Y x)y Y x
Theorem. (Sigma_E)
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)xX, yY x, z = pair x y
Definition. We define setprod to be λX Y : setxX, Y of type setsetset.
Let lam : set(setset)setSigma
Definition. We define ap to be λf x ⇒ {|zf, y : set, z = pair x y} of type setsetset.
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
Theorem. (lamE)
∀X : set, ∀F : setset, ∀z : set, z (λxX F x)xX, yF x, z = pair x y
Theorem. (apI)
∀f x y, pair x y fy f x
Theorem. (apE)
∀f x y, y f xpair x y f
Theorem. (beta)
∀X : set, ∀F : setset, ∀x : set, x X(λxX F x) x = F x
Theorem. (pair_ap_0)
∀x y : set, (pair x y) 0 = x
Theorem. (pair_ap_1)
∀x y : set, (pair x y) 1 = y
Theorem. (ap0_Sigma)
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)(z 0) X
Theorem. (ap1_Sigma)
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)(z 1) (Y (z 0))
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)
Theorem. (tuple_pair)
∀x y : set, pair x y = (x,y)
Definition. We define Pi to be λX Y ⇒ {f𝒫 (xX, (Y x))|xX, f x Y x} of type set(setset)set.
Theorem. (PiI)
∀X : set, ∀Y : setset, ∀f : set, (uf, u 0 X)(xX, f x Y x)f xX, Y x
Theorem. (lam_Pi)
∀X : set, ∀Y : setset, ∀F : setset, (xX, F x Y x)(λxX F x) (xX, Y x)
Theorem. (ap_Pi)
∀X : set, ∀Y : setset, ∀f : set, ∀x : set, f (xX, Y x)x Xf x Y x
Definition. We define setexp to be λX Y : setyY, X of type setsetset.
Theorem. (pair_tuple_fun)
pair = (λx y ⇒ (x,y))
Beginning of Section Tuples
Variable x0 x1 : set
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}
Theorem. (lamI2)
∀X, ∀F : setset, xX, yF x, (x,y) λxX F x
Theorem. (tuple_2_Sigma)
∀X : set, ∀Y : setset, xX, yY x, (x,y) xX, Y x
Theorem. (tuple_2_setprod)
∀X : set, ∀Y : set, xX, yY, (x,y) X Y
End of Section pair_setsum
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 () 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 () ()
Definition. We define PNoEq_ to be λα p q ⇒ βα, p β q β of type set(setprop)(setprop)prop.
Theorem. (PNoEq_ref_)
∀α, ∀p : setprop, p p
Theorem. (PNoEq_sym_)
∀α, ∀p q : setprop, p q q p
Theorem. (PNoEq_tra_)
∀α, ∀p q r : setprop, p q q r p r
Theorem. (PNoEq_antimon_)
∀p q : setprop, ∀α, βα, p q p q
Definition. We define PNoLt_ to be λα p q ⇒ βα, p q ¬ p β q β of type set(setprop)(setprop)prop.
Theorem. (PNoLt_E_)
∀α, ∀p q : setprop, p q∀R : prop, (∀β, β α p q¬ p βq βR)R
Theorem. (PNoLt_irref_)
∀α, ∀p : setprop, ¬ p p
Theorem. (PNoLt_mon_)
∀p q : setprop, ∀α, βα, p q p q
Theorem. (PNoLt_trichotomy_or_)
∀p q : setprop, ∀α, p q p q q p
Definition. We define PNoLt to be λα p β q ⇒ PNoLt_ (α β) p q α β p q q α β α p q ¬ p β of type set(setprop)set(setprop)prop.
Theorem. (PNoLtI1)
∀α β, ∀p q : setprop, PNoLt_ (α β) p q p β q
Theorem. (PNoLtI2)
∀α β, ∀p q : setprop, α β p qq α p β q
Theorem. (PNoLtI3)
∀α β, ∀p q : setprop, β α p q¬ p β p β q
Theorem. (PNoLtE)
∀α β, ∀p q : setprop, p β q∀R : prop, (PNoLt_ (α β) p qR)(α β p qq αR)(β α p q¬ p βR)R
Theorem. (PNoLt_irref)
∀α, ∀p : setprop, ¬ p α p
Theorem. (PNoLt_trichotomy_or)
∀α β, ∀p q : setprop, p β q α = β p q q α p
Theorem. (PNoLtEq_tra)
∀α β, ∀p q r : setprop, p β q q r p β r
Theorem. (PNoEqLt_tra)
∀α β, ∀p q r : setprop, p q q β r p β r
Theorem. (PNoLt_tra)
∀α β γ, ∀p q r : setprop, p β q q γ r p γ r
Definition. We define PNoLe to be λα p β q ⇒ p β q α = β p q of type set(setprop)set(setprop)prop.
Theorem. (PNoLeI1)
∀α β, ∀p q : setprop, p β q p β q
Theorem. (PNoLeI2)
∀α, ∀p q : setprop, p q p α q
Theorem. (PNoLe_ref)
∀α, ∀p : setprop, p α p
Theorem. (PNoLe_antisym)
∀α β, ∀p q : setprop, p β q q α pα = β p q
Theorem. (PNoLtLe_tra)
∀α β γ, ∀p q r : setprop, p β q q γ r p γ r
Theorem. (PNoLeLt_tra)
∀α β γ, ∀p q r : setprop, p β q q γ r p γ r
Theorem. (PNoEqLe_tra)
∀α β, ∀p q r : setprop, p q q β r p β r
Theorem. (PNoLe_tra)
∀α β γ, ∀p q r : setprop, p β q q γ r p γ r
Definition. We define PNo_downc to be λL α p ⇒ β, q : setprop, L β q p β q of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_upc to be λR α p ⇒ β, q : setprop, R β q q α p of type (set(setprop)prop)set(setprop)prop.
Theorem. (PNoLe_downc)
∀L : set(setprop)prop, ∀α β, ∀p q : setprop, α p q α p β q
Theorem. (PNo_downc_ref)
∀L : set(setprop)prop, ∀α, ∀p : setprop, L α p α p
Theorem. (PNo_upc_ref)
∀R : set(setprop)prop, ∀α, ∀p : setprop, R α p α p
Theorem. (PNoLe_upc)
∀R : set(setprop)prop, ∀α β, ∀p q : setprop, α p p β q β q
Definition. We define PNoLt_pwise to be λL R ⇒ ∀γ, ∀p : setprop, L γ p∀δ, ∀q : setprop, R δ q p δ q of type (set(setprop)prop)(set(setprop)prop)prop.
Theorem. (PNoLt_pwise_downc_upc)
∀L R : set(setprop)prop, R ()
Definition. We define PNo_rel_strict_upperbd to be λL α p ⇒ βα, ∀q : setprop, β q q α p of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_rel_strict_lowerbd to be λR α p ⇒ βα, ∀q : setprop, β q p β q of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_rel_strict_imv to be λL R α p ⇒ of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
Theorem. (PNoEq_rel_strict_upperbd)
∀L : set(setprop)prop, ∀α, ∀p q : setprop, p q
Theorem. (PNo_rel_strict_upperbd_antimon)
∀L : set(setprop)prop, ∀α, ∀p : setprop, βα,
Theorem. (PNoEq_rel_strict_lowerbd)
∀R : set(setprop)prop, ∀α, ∀p q : setprop, p q
Theorem. (PNo_rel_strict_lowerbd_antimon)
∀R : set(setprop)prop, ∀α, ∀p : setprop, βα,
Theorem. (PNoEq_rel_strict_imv)
∀L R : set(setprop)prop, ∀α, ∀p q : setprop, p q α p α q
Theorem. (PNo_rel_strict_imv_antimon)
∀L R : set(setprop)prop, ∀α, ∀p : setprop, βα, α p β p
Definition. We define PNo_rel_strict_uniq_imv to be λL R α p ⇒ α p ∀q : setprop, α q 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 ⇒ () (λδ ⇒ p δ δ α) () (λδ ⇒ p δ δ = α) of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
Theorem. (PNo_extend0_eq)
∀α, ∀p : setprop, p (λδ ⇒ p δ δ α)
Theorem. (PNo_extend1_eq)
∀α, ∀p : setprop, p (λδ ⇒ p δ δ = α)
Theorem. (PNo_rel_imv_ex)
∀L R : set(setprop)prop, R∀α, (p : setprop, p) (tauα, p : setprop, tau p)
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, ∀α, L R∀p : setprop, α p () (λδ ⇒ p δ δ α)
Theorem. (PNo_lenbdd_strict_imv_extend1)
∀L R : set(setprop)prop, ∀α, L R∀p : setprop, α p () (λδ ⇒ p δ δ = α)
Theorem. (PNo_lenbdd_strict_imv_split)
∀L R : set(setprop)prop, ∀α, L R∀p : setprop, α p p
Theorem. (PNo_rel_imv_bdd_ex)
∀L R : set(setprop)prop, R∀α, L Rβ, p : setprop, p
Definition. We define PNo_strict_upperbd to be λL α p ⇒ ∀β, ∀q : setprop, L β q q α p of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_strict_lowerbd to be λR α p ⇒ ∀β, ∀q : setprop, R β q p β q of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_strict_imv to be λL R α p ⇒ p p of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
Theorem. (PNoEq_strict_upperbd)
∀L : set(setprop)prop, ∀α, ∀p q : setprop, p q p q
Theorem. (PNoEq_strict_lowerbd)
∀R : set(setprop)prop, ∀α, ∀p q : setprop, p q p q
Theorem. (PNoEq_strict_imv)
∀L R : set(setprop)prop, ∀α, ∀p q : setprop, p q α p α q
Theorem. (PNo_strict_upperbd_imp_rel_strict_upperbd)
∀L : set(setprop)prop, ∀α, β, ∀p : setprop, p
Theorem. (PNo_strict_lowerbd_imp_rel_strict_lowerbd)
∀R : set(setprop)prop, ∀α, β, ∀p : setprop, p
Theorem. (PNo_strict_imv_imp_rel_strict_imv)
∀L R : set(setprop)prop, ∀α, β, ∀p : setprop, α p β p
Theorem. (PNo_rel_split_imv_imp_strict_imv)
∀L R : set(setprop)prop, ∀α, ∀p : setprop, p α p
Theorem. (PNo_lenbdd_strict_imv_ex)
∀L R : set(setprop)prop, R∀α, L Rβ, p : setprop, β p
Definition. We define PNo_least_rep to be λL R β p ⇒ β p γβ, ∀q : setprop, ¬ γ q of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
Definition. We define PNo_least_rep2 to be λL R β p ⇒ β 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, R∀α, ∀p q : setprop, α p α qβα, p β q β
Theorem. (PNo_lenbdd_least_rep2_exuniq2)
∀L R : set(setprop)prop, R∀α, L Rβ, (p : setprop, β p) (∀p q : setprop, β p β qp = q)
Definition. We define PNo_bd to be λL R ⇒ of type (set(setprop)prop)(set(setprop)prop)set.
Definition. We define PNo_pred to be λL R ⇒ of type (set(setprop)prop)(set(setprop)prop)setprop.
Theorem. (PNo_bd_pred_lem)
∀L R : set(setprop)prop, R∀α, L R ( R) ( R)
Theorem. (PNo_bd_pred)
∀L R : set(setprop)prop, R∀α, L R ( R) ( R)
Theorem. (PNo_bd_In)
∀L R : set(setprop)prop, R∀α, L R R
Beginning of Section TaggedSets
Let tag : setsetλα ⇒
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
Theorem. (tagged_notin_ordinal)
∀α y, (y ') α
Theorem. (tagged_eqE_Subq)
∀α β, α ' = β 'α β
Theorem. (tagged_eqE_eq)
∀α β, α ' = β 'α = β
Theorem. (tagged_ReplE)
∀α β, β ' {γ '|γα}β α
Definition. We define SNoElts_ to be λα ⇒ α {β '|βα} of type setset.
Theorem. (SNoElts_mon)
∀α β, α β
Definition. We define SNo_ to be λα x ⇒ x βα, exactly1of2 (β ' x) (β x) of type setsetprop.
Definition. We define PSNo to be λα p ⇒ {βα|p β} {β '|βα, ¬ p β} of type set(setprop)set.
Theorem. (PNoEq_PSNo)
∀α, ∀p : setprop, (λβ ⇒ β PSNo α p) p
Theorem. (SNo_PSNo)
∀α, ∀p : setprop, SNo_ α (PSNo α p)
Theorem. (SNo_PSNo_eta_)
∀α x, SNo_ α xx = PSNo α (λβ ⇒ β x)
Definition. We define SNo to be λx ⇒ α, SNo_ α x of type setprop.
Theorem. (SNo_SNo)
∀α, ∀z, SNo_ α zSNo z
Definition. We define SNoLev to be λx ⇒ Eps_i (λα ⇒ SNo_ α x) of type setset.
Theorem. (SNoLev_uniq_Subq)
∀x α β, SNo_ α xSNo_ β xα β
Theorem. (SNoLev_uniq)
∀x α β, SNo_ α xSNo_ β xα = β
Theorem. (SNoLev_)
∀x, SNo xSNo_ () x
Theorem. (SNo_PSNo_eta)
∀x, SNo xx = PSNo () (λβ ⇒ β x)
Theorem. (SNoLev_PSNo)
∀α, ∀p : setprop, SNoLev (PSNo α p) = α
Theorem. (SNo_Subq)
∀x y, SNo xSNo y (α, α x α y)x y
Definition. We define SNoEq_ to be λα x y ⇒ (λβ ⇒ β x) (λβ ⇒ β y) of type setsetsetprop.
Theorem. (SNoEq_I)
∀α x y, (βα, β x β y) x y
Theorem. (SNo_eq)
∀x y, SNo xSNo y = SNoEq_ () x yx = y
End of Section TaggedSets
Definition. We define SNoLt to be λx y ⇒ PNoLt () (λβ ⇒ β x) () (λβ ⇒ β y) of type setsetprop.
Definition. We define SNoLe to be λx y ⇒ PNoLe () (λβ ⇒ β x) () (λβ ⇒ β y) of type setsetprop.
Theorem. (SNoLtLe)
∀x y, x < yx y
Theorem. (SNoLeE)
∀x y, SNo xSNo yx yx < y x = y
Theorem. (SNoEq_sym_)
∀α x y, x y y x
Theorem. (SNoEq_tra_)
∀α x y z, x y y z x z
Theorem. (SNoLtE)
∀x y, SNo xSNo yx < y∀p : prop, (∀z, SNo z SNoEq_ () z xSNoEq_ () z yx < zz < y x yp)( SNoEq_ () x y yp)( SNoEq_ () x y xp)p
Theorem. (SNoLtI2)
∀x y, SNoEq_ () x y yx < y
Theorem. (SNoLtI3)
∀x y, SNoEq_ () x y xx < y
Theorem. (SNoLt_irref)
∀x, ¬ x
Theorem. (SNoLt_trichotomy_or)
∀x y, SNo xSNo yx < y x = y y < x
Theorem. (SNoLt_trichotomy_or_impred)
∀x y, SNo xSNo y∀p : prop, (x < yp)(x = yp)(y < xp)p
Theorem. (SNoLt_tra)
∀x y z, SNo xSNo ySNo zx < yy < zx < z
Theorem. (SNoLe_ref)
∀x, x
Theorem. (SNoLe_antisym)
∀x y, SNo xSNo yx yy xx = y
Theorem. (SNoLtLe_tra)
∀x y z, SNo xSNo ySNo zx < yy zx < z
Theorem. (SNoLeLt_tra)
∀x y z, SNo xSNo ySNo zx yy < zx < z
Theorem. (SNoLe_tra)
∀x y z, SNo xSNo ySNo zx yy zx z
Theorem. (SNoLtLe_or)
∀x y, SNo xSNo yx < y y x
Theorem. (SNoLt_PSNo_PNoLt)
∀α β, ∀p q : setprop, PSNo α p < PSNo β q p β q
Theorem. (PNoLt_SNoLt_PSNo)
∀α β, ∀p q : setprop, p β qPSNo α p < PSNo β q
Definition. We define SNoCut to be λL R ⇒ PSNo (PNo_bd (λα p ⇒ PSNo α p L) (λα p ⇒ PSNo α p R)) (PNo_pred (λα p ⇒ PSNo α p L) (λα p ⇒ 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, RSNo ( R) SNoLev ( R) ordsucc ((xLordsucc ()) (yRordsucc ())) (xL, x < R) (yR, R < y) (∀z, SNo z(xL, x < z)(yR, z < y)SNoLev ( R) SNoEq_ (SNoLev ( R)) ( R) z)
Theorem. (SNoCutP_SNoCut_impred)
∀L R, R∀p : prop, (SNo ( R)SNoLev ( R) ordsucc ((xLordsucc ()) (yRordsucc ()))(xL, x < R)(yR, R < y)(∀z, SNo z(xL, x < z)(yR, z < y)SNoLev ( R) SNoEq_ (SNoLev ( R)) ( R) z)p)p
Theorem. (SNoCutP_L_0)
∀L, (xL, SNo x) 0
Definition. We define SNoS_ to be λα ⇒ {x𝒫 ()|βα, SNo_ β x} of type setset.
Theorem. (SNoS_E)
∀α, x, βα, SNo_ β x
Beginning of Section TaggedSets2
Let tag : setsetλα ⇒
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
Theorem. (SNoS_I)
∀α, ∀x, βα, SNo_ β xx
Theorem. (SNoS_I2)
∀x y, SNo xSNo y x SNoS_ ()
Theorem. (SNoS_Subq)
∀α β, α β
Theorem. (SNoLev_uniq2)
∀α, ∀x, SNo_ α x = α
Theorem. (SNoS_E2)
∀α, x, ∀p : prop, ( αordinal ()SNo xSNo_ () xp)p
Definition. We define SNoL to be λz ⇒ {xSNoS_ ()|x < z} of type setset.
Definition. We define SNoR to be λz ⇒ {ySNoS_ ()|z < y} of type setset.
Theorem. (SNoL_E)
∀x, SNo xwSNoL x, ∀p : prop, (SNo w w < xp)p
Theorem. (SNoR_E)
∀x, SNo xzSNoR x, ∀p : prop, (SNo z x < zp)p
Theorem. (SNoL_I)
∀z, SNo z∀x, SNo x x < zx SNoL z
Theorem. (SNoR_I)
∀z, SNo z∀y, SNo y z < yy SNoR z
Theorem. (SNo_eta)
∀z, SNo zz = SNoCut (SNoL z) (SNoR z)
Theorem. (SNoCutP_SNo_SNoCut)
∀L R, RSNo ( R)
Theorem. (SNoCutP_SNoCut_fst)
∀L R, R∀z, SNo z(xL, x < z)(yR, z < y)SNoLev ( R) SNoEq_ (SNoLev ( R)) ( R) z
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
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
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
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
Theorem. (ordinal_SNo_)
∀α, SNo_ α α
Theorem. (ordinal_SNo)
∀α, SNo α
Theorem. (ordinal_SNoLev_max)
∀α, ∀z, SNo z αz < α
Theorem. (ordinal_SNoL)
∀α, SNoL α =
Theorem. (ordinal_SNoLev_max_2)
∀α, ∀z, SNo z z α
Theorem. (ordinal_Subq_SNoLe)
∀α β, α βα β
Theorem. (ordinal_SNoLt_In)
∀α β, α < βα β
Theorem. (SNo_max_SNoLev)
∀x, SNo x(ySNoS_ (), y < x) = x
Theorem. (SNo_max_ordinal)
∀x, SNo x(ySNoS_ (), y < x)
Theorem. (pos_low_eq_one)
∀x, SNo x0 < x 1x = 1
Definition. We define SNo_extend0 to be λx ⇒ PSNo (ordsucc ()) (λδ ⇒ δ x δ ) of type setset.
Definition. We define SNo_extend1 to be λx ⇒ PSNo (ordsucc ()) (λδ ⇒ δ x δ = ) of type setset.
Theorem. (SNoLev_0_eq_0)
∀x, SNo x = 0x = 0
Definition. We define eps_ to be λn ⇒ {() '|mn} of type setset.
Theorem. (eps_ordinal_In_eq_0)
∀n α, α eps_ nα = 0
Theorem. (eps_SNo_eq)
∀n, xSNoS_ (), 0 < xSNoEq_ () (eps_ n) xmn, x = eps_ m
End of Section TaggedSets2
Theorem. (SNo_etaE)
∀z, SNo z∀p : prop, (∀L R, R(xL, )(yR, )z = Rp)p
Theorem. (SNo_ind)
∀P : setprop, (∀L R, R(xL, P x)(yR, P y)P ( R))∀z, SNo zP z
Beginning of Section SurrealRecI
Variable F : set(setset)set
Let default : setEps_i (λ_ ⇒ True)
Let G : set(setsetset)setsetλα g ⇒ If_ii () (λz : setif z SNoS_ () then F z (λw ⇒ g () w) else default) (λz : setdefault)
Definition. We define SNo_rec_i to be λz ⇒ () z of type setset.
Hypothesis Fr : ∀z, SNo z∀g h : setset, (wSNoS_ (), g w = h w)F z g = F z h
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 () (λz : setIf_ii (z SNoS_ ()) (F z (λw ⇒ g () w)) default) (λz : setdefault)
Definition. We define SNo_rec_ii to be λz ⇒ () z of type set(setset).
Hypothesis Fr : ∀z, SNo z∀g h : set(setset), (wSNoS_ (), g w = h w)F z g = F z h
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 of type setsetset.
Hypothesis Fr : ∀w, SNo w∀z, SNo z∀g h : setsetset, (xSNoS_ (), ∀y, SNo yg x y = h x y)(ySNoS_ (), 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_ (), f x = k x)∀z, SNo z∀g h : setset, (uSNoS_ (), g u = h u)G w f z g = G w k z h
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))
Theorem. (SNo_rec2_eq)
∀w, SNo w∀z, SNo z z = F w z SNo_rec2
End of Section SurrealRec2
Theorem. (SNo_ordinal_ind)
∀P : setprop, (∀α, x, P x)(∀x, SNo xP x)
Theorem. (SNo_ordinal_ind2)
∀P : setsetprop, (∀α, ∀β, x, y, P x y)(∀x y, SNo xSNo yP x y)
Theorem. (SNo_ordinal_ind3)
∀P : setsetsetprop, (∀α, ∀β, ∀γ, x, y, z, P x y z)(∀x y z, SNo xSNo ySNo zP x y z)
Theorem. (SNoLev_ind)
∀P : setprop, (∀x, SNo x(wSNoS_ (), P w)P x)(∀x, SNo xP x)
Theorem. (SNoLev_ind2)
∀P : setsetprop, (∀x y, SNo xSNo y(wSNoS_ (), P w y)(zSNoS_ (), P x z)(wSNoS_ (), zSNoS_ (), P w z)P x y)∀x y, SNo xSNo yP x y
Theorem. (SNoLev_ind3)
∀P : setsetsetprop, (∀x y z, SNo xSNo ySNo z(uSNoS_ (), P u y z)(vSNoS_ (), P x v z)(wSNoS_ (), P x y w)(uSNoS_ (), vSNoS_ (), P u v z)(uSNoS_ (), wSNoS_ (), P u y w)(vSNoS_ (), wSNoS_ (), P x v w)(uSNoS_ (), vSNoS_ (), wSNoS_ (), P u v w)P x y z)∀x y z, SNo xSNo ySNo zP x y z
Theorem. (restr_SNo_)
∀x, SNo xα, SNo_ α (x )
Theorem. (restr_SNo)
∀x, SNo xα, SNo (x )
Theorem. (restr_SNoLev)
∀x, SNo xα, SNoLev (x ) = α
Theorem. (restr_SNoEq)
∀x, SNo xα, (x ) x
Theorem. (SNo_extend0_restr_eq)
∀x, SNo xx = SNoElts_ ()
Theorem. (SNo_extend1_restr_eq)
∀x, SNo xx = SNoElts_ ()
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.
Theorem. (SNo_minus_SNo)
∀x, SNo xSNo (- x)
Theorem. (minus_SNo_Lt_contra)
∀x y, SNo xSNo yx < y- y < - x
Theorem. (minus_SNo_Le_contra)
∀x y, SNo xSNo yx y- y - x
Theorem. (minus_SNo_invol)
∀x, SNo x- - x = x
Theorem. (minus_SNo_SNo_)
∀α, ∀x, SNo_ α xSNo_ α (- x)
Theorem. (minus_SNo_SNoS_)
∀α, ∀x, x - x
Theorem. (minus_SNoCut_eq_lem)
∀v, SNo v∀L R, Rv = R- v = SNoCut {- z|zR} {- w|wL}
Theorem. (minus_SNo_Lt_contra1)
∀x y, SNo xSNo y- x < y- y < x
Theorem. (minus_SNo_Lt_contra2)
∀x y, SNo xSNo yx < - yy < - x
Theorem. (mordinal_SNoLev_min_2)
∀α, ∀z, SNo z - α z
End of Section SurrealMinus
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.
∀x, SNo x∀y, SNo yx + y = SNoCut ({w + y|wSNoL x} {x + w|wSNoL y}) ({z + y|zSNoR x} {x + z|zSNoR y})
∀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})
∀x y, SNo xSNo ySNo (x + y)
∀x y z, SNo xSNo ySNo zSNo (x + y + z)
∀x y z, SNo xSNo ySNo zSNo (x + y + - z)
∀x y z w, SNo xSNo ySNo zSNo wSNo (x + y + z + w)
∀x y z, SNo xSNo ySNo zx < zx + y < z + y
∀x y z, SNo xSNo ySNo zx zx + y z + y
∀x y z, SNo xSNo ySNo zy < zx + y < x + z
∀x y z, SNo xSNo ySNo zy zx + y x + z
∀x y z w, SNo xSNo ySNo zSNo wx < zy wx + y < z + w
∀x y z w, SNo xSNo ySNo zSNo wx zy < wx + y < z + w
∀x y z w, SNo xSNo ySNo zSNo wx < zy < wx + y < z + w
∀x y z w, SNo xSNo ySNo zSNo wx zy wx + y z + w
∀x y, SNo xSNo yx + y = y + x
∀x, SNo x0 + x = x
∀x, SNo xx + 0 = x
∀α, ∀β, α + β = SNoCut ({x + β|x} {α + x|x}) Empty
∀α, ∀β, ordinal (α + β)
∀α, ∀β, + β = ordsucc (α + β)