P. 281 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28001-28100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sltssepc 28001	Two elements of separated sets obey less-than. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝑋 <s 𝑌)
Theorem	sltssepcd 28002	Two elements of separated sets obey less-than. Deduction form of sltssepc 28001. (Contributed by Scott Fenton, 25-Sep-2024.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 <s 𝑌)
Theorem	ssslts1 28003	Relation between surreal set less-than and subset. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴) → 𝐶 <<s 𝐵)
Theorem	ssslts2 28004	Relation between surreal set less-than and subset. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐴 <<s 𝐶)
Theorem	nulslts 28005	The empty set is less-than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 ∈ 𝒫 No → ∅ <<s 𝐴)
Theorem	nulsgts 28006	The empty set is greater than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 ∈ 𝒫 No → 𝐴 <<s ∅)
Theorem	nulsltsd 28007	The empty set is less-than any set of surreals. Deduction version. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ No )    ⇒   ⊢ (𝜑 → ∅ <<s 𝐴)
Theorem	nulsgtsd 28008	The empty set is greater than any set of surreals. Deduction version. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ No )    ⇒   ⊢ (𝜑 → 𝐴 <<s ∅)
Theorem	conway 28009*	Conway's Simplicity Theorem. Given 𝐴 preceeding 𝐵, there is a unique surreal of minimal length separating them. This is a fundamental property of surreals and will be used (via surreal cuts) to prove many properties later on. Theorem from [Alling] p. 185. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ∃!𝑥 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))
Theorem	cutsval 28010*	The value of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → (𝐴 |s 𝐵) = (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})))
Theorem	cutcuts 28011	Cut properties of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
Theorem	cutscl 28012	Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.)
⊢ (𝐴 <<s 𝐵 → (𝐴 |s 𝐵) ∈ No )
Theorem	cutscld 28013	Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) ∈ No )
Theorem	cutbday 28014*	The birthday of the surreal cut is equal to the minimum birthday in the gap. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑥 ∈ No ∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)}))
Theorem	eqcuts 28015*	Condition for equality to a surreal cut. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ((𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) → ((𝐿 |s 𝑅) = 𝑋 ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ( bday ‘𝑋) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)}))))
Theorem	eqcuts2 28016*	Condition for equality to a surreal cut. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ((𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) → ((𝐿 |s 𝑅) = 𝑋 ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ∀𝑦 ∈ No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday ‘𝑋) ⊆ ( bday ‘𝑦)))))
Theorem	sltstr 28017	Transitive law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ∧ 𝐵 ≠ ∅) → 𝐴 <<s 𝐶)
Theorem	sltsun1 28018	Union law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → (𝐴 ∪ 𝐵) <<s 𝐶)
Theorem	sltsun2 28019	Union law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s (𝐵 ∪ 𝐶))
Theorem	cutsun12 28020	Union law for surreal cuts. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → ((𝐴 ∪ 𝐶) |s (𝐵 ∪ 𝐷)) = (𝐴 |s 𝐵))
Theorem	dmcuts 28021	The domain of the surreal cut operation is all separated surreal sets. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ dom |s = <<s
Theorem	cutsf 28022	Functionality statement for the surreal cut operator. (Contributed by Scott Fenton, 15-Dec-2021.)
⊢ |s : <<s ⟶ No
Theorem	etaslts 28023*	A restatement of noeta 27944 using set less-than. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂) → ∃𝑥 ∈ No (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday ‘𝑥) ⊆ 𝑂))
Theorem	etaslts2 28024*	A version of etaslts 28023 with fewer hypotheses but a weaker upper bound. (Contributed by Scott Fenton, 10-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ∃𝑥 ∈ No (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday ‘𝑥) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))))
Theorem	cutbdaybnd 28025	An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂) → ( bday ‘(𝐴 |s 𝐵)) ⊆ 𝑂)
Theorem	cutbdaybnd2 28026	An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵)))
Theorem	cutbdaybnd2lim 28027	An upper bound on the birthday of a surreal cut when it is a limit birthday. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday ‘(𝐴 |s 𝐵))) → ( bday ‘(𝐴 |s 𝐵)) ⊆ ∪ ( bday “ (𝐴 ∪ 𝐵)))
Theorem	cutbdaylt 28028	If a surreal lies in a gap and is not equal to the cut, its birthday is greater than the cut's. (Contributed by Scott Fenton, 11-Dec-2021.)
⊢ ((𝑋 ∈ No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → ( bday ‘(𝐴 |s 𝐵)) ∈ ( bday ‘𝑋))
Theorem	lesrec 28029*	A comparison law for surreals considered as cuts of sets of surreals. Definition from [Conway] p. 4. Theorem 4 of [Alling] p. 186. Theorem 2.5 of [Gonshor] p. 9. (Contributed by Scott Fenton, 11-Dec-2021.)
⊢ (((𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷) ∧ (𝑋 = (𝐴 |s 𝐵) ∧ 𝑌 = (𝐶 |s 𝐷))) → (𝑋 ≤s 𝑌 ↔ (∀𝑑 ∈ 𝐷 𝑋 <s 𝑑 ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑌)))
Theorem	lesrecd 28030*	A comparison law for surreals considered as cuts of sets of surreals. Definition from [Conway] p. 4. Theorem 4 of [Alling] p. 186. Theorem 2.5 of [Gonshor] p. 9. (Contributed by Scott Fenton, 5-Dec-2025.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝐶 <<s 𝐷)    &   ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵))    &   ⊢ (𝜑 → 𝑌 = (𝐶 |s 𝐷))    ⇒   ⊢ (𝜑 → (𝑋 ≤s 𝑌 ↔ (∀𝑑 ∈ 𝐷 𝑋 <s 𝑑 ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑌)))
Theorem	ltsrec 28031*	A comparison law for surreals considered as cuts of sets of surreals. (Contributed by Scott Fenton, 11-Dec-2021.)
⊢ (((𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷) ∧ (𝑋 = (𝐴 |s 𝐵) ∧ 𝑌 = (𝐶 |s 𝐷))) → (𝑋 <s 𝑌 ↔ (∃𝑐 ∈ 𝐶 𝑋 ≤s 𝑐 ∨ ∃𝑏 ∈ 𝐵 𝑏 ≤s 𝑌)))
Theorem	ltsrecd 28032*	A comparison law for surreals considered as cuts of sets of surreals. (Contributed by Scott Fenton, 5-Dec-2025.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝐶 <<s 𝐷)    &   ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵))    &   ⊢ (𝜑 → 𝑌 = (𝐶 |s 𝐷))    ⇒   ⊢ (𝜑 → (𝑋 <s 𝑌 ↔ (∃𝑐 ∈ 𝐶 𝑋 ≤s 𝑐 ∨ ∃𝑏 ∈ 𝐵 𝑏 ≤s 𝑌)))
Theorem	sltsdisj 28033	If 𝐴 preceeds 𝐵, then 𝐴 and 𝐵 are disjoint. (Contributed by Scott Fenton, 18-Sep-2024.)
⊢ (𝐴 <<s 𝐵 → (𝐴 ∩ 𝐵) = ∅)
Theorem	eqcuts3 28034*	A variant of the simplicity theorem - if 𝐵 lies between the cut sets of 𝐴 but none of its options do, then 𝐴 = 𝐵. Theorem 11 of [Conway] p. 23. (Contributed by Scott Fenton, 28-Nov-2025.)
⊢ (𝜑 → 𝐿 <<s 𝑅)    &   ⊢ (𝜑 → 𝑀 <<s 𝑆)    &   ⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅))    &   ⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆))    &   ⊢ (𝜑 → 𝐿 <<s {𝐵})    &   ⊢ (𝜑 → {𝐵} <<s 𝑅)    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ (𝑀 ∪ 𝑆) ¬ (𝐿 <<s {𝑥𝑂} ∧ {𝑥𝑂} <<s 𝑅))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
15.3.2  Zero and One
Syntax	c0s 28035	Declare the class syntax for surreal zero.
class 0s
Syntax	c1s 28036	Declare the class syntax for surreal one.
class 1s
Definition	df-0s 28037	Define surreal zero. This is the simplest cut of surreal number sets. Definition from [Conway] p. 17. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 0s = (∅ |s ∅)
Definition	df-1s 28038	Define surreal one. This is the simplest number greater than surreal zero. Definition from [Conway] p. 18. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 1s = ({ 0s } |s ∅)
Theorem	0no 28039	Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 0s ∈ No
Theorem	1no 28040	Surreal one is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 1s ∈ No
Theorem	bday0 28041	Calculate the birthday of surreal zero. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ ( bday ‘ 0s ) = ∅
Theorem	0lt1s 28042	Surreal zero is less than surreal one. Theorem from [Conway] p. 7. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 0s <s 1s
Theorem	bday0b 28043	The only surreal with birthday ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝑋 ∈ No → (( bday ‘𝑋) = ∅ ↔ 𝑋 = 0s ))
Theorem	bday1 28044	The birthday of surreal one is ordinal one. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ( bday ‘ 1s ) = 1o
Theorem	cuteq0 28045	Condition for a surreal cut to equal zero. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝜑 → 𝐴 <<s { 0s })    &   ⊢ (𝜑 → { 0s } <<s 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = 0s )
Theorem	cutneg 28046	The simplest number greater than a negative number is zero. (Contributed by Scott Fenton, 4-Sep-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 0s )    ⇒   ⊢ (𝜑 → ({𝐴} |s ∅) = 0s )
Theorem	cuteq1 28047	Condition for a surreal cut to equal one. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (𝜑 → 0s ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 <<s { 1s })    &   ⊢ (𝜑 → { 1s } <<s 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = 1s )
Theorem	gt0ne0s 28048	A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ ( 0s <s 𝐴 → 𝐴 ≠ 0s )
Theorem	gt0ne0sd 28049	A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (𝜑 → 0s <s 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0s )
Theorem	1ne0s 28050	Surreal zero does not equal surreal one. (Contributed by Scott Fenton, 5-Sep-2025.)
⊢ 1s ≠ 0s
Theorem	rightge0 28051*	A surreal is non-negative iff all its right options are positive. (Contributed by Scott Fenton, 1-Jan-2026.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵))    ⇒   ⊢ (𝜑 → ( 0s ≤s 𝑋 ↔ ∀𝑥𝑅 ∈ 𝐵 0s <s 𝑥𝑅))
15.3.3  Cuts and Options
Syntax	cmade 28052	Declare the symbol for the made by function.
class M
Syntax	cold 28053	Declare the symbol for the older than function.
class O
Syntax	cnew 28054	Declare the symbol for the new on function.
class N
Syntax	cleft 28055	Declare the symbol for the left option function.
class L
Syntax	cright 28056	Declare the symbol for the right option function.
class R
Definition	df-made 28057	Define the made by function. This function carries an ordinal to all surreals made by sections of surreals older than it. Definition from [Conway] p. 29. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ M = recs((𝑓 ∈ V ↦ ( |s “ (𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓))))
Definition	df-old 28058	Define the older than function. This function carries an ordinal to all surreals made by a previous ordinal. Definition from [Conway] p. 29. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ O = (𝑥 ∈ On ↦ ∪ ( M “ 𝑥))
Definition	df-new 28059	Define the newer than function. This function carries an ordinal to all surreals made on that day. Definition from [Conway] p. 29. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ N = (𝑥 ∈ On ↦ (( M ‘𝑥) ∖ ( O ‘𝑥)))
Definition	df-left 28060*	Define the left options of a surreal. This is the set of surreals that are simpler and less than the given surreal. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ L = (𝑥 ∈ No ↦ {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ 𝑦 <s 𝑥})
Definition	df-right 28061*	Define the right options of a surreal. This is the set of surreals that are simpler and greater than the given surreal. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ R = (𝑥 ∈ No ↦ {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ 𝑥 <s 𝑦})
Theorem	madeval 28062	The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))))
Theorem	madeval2 28063*	Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ (𝐴 ∈ On → ( M ‘𝐴) = {𝑥 ∈ No ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)})
Theorem	oldval 28064	The value of the old options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ (𝐴 ∈ On → ( O ‘𝐴) = ∪ ( M “ 𝐴))
Theorem	newval 28065	The value of the new options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( N ‘𝐴) = (( M ‘𝐴) ∖ ( O ‘𝐴))
Theorem	madef 28066	The made function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ M :On⟶𝒫 No
Theorem	oldf 28067	The older function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ O :On⟶𝒫 No
Theorem	newf 28068	The new function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ N :On⟶𝒫 No
Theorem	old0 28069	No surreal is older than ∅. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ ( O ‘∅) = ∅
Theorem	madessno 28070	Made sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( M ‘𝐴) ⊆ No
Theorem	oldssno 28071	Old sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( O ‘𝐴) ⊆ No
Theorem	newssno 28072	New sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( N ‘𝐴) ⊆ No
Theorem	madeno 28073	An element of a made set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ ( M ‘𝐵) → 𝐴 ∈ No )
Theorem	oldno 28074	An element of an old set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ ( O ‘𝐵) → 𝐴 ∈ No )
Theorem	newno 28075	An element of a new set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ ( N ‘𝐵) → 𝐴 ∈ No )
Theorem	madenod 28076	An element of a made set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ ( M ‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	oldnod 28077	An element of an old set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ ( O ‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	newnod 28078	An element of a new set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ ( N ‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	leftval 28079*	The value of the left options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( L ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝑥 <s 𝐴}
Theorem	rightval 28080*	The value of the right options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( R ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝐴 <s 𝑥}
Theorem	elleft 28081	Membership in the left set of a surreal. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( L ‘𝐵) ↔ (𝐴 ∈ ( O ‘( bday ‘𝐵)) ∧ 𝐴 <s 𝐵))
Theorem	elright 28082	Membership in the right set of a surreal. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( R ‘𝐵) ↔ (𝐴 ∈ ( O ‘( bday ‘𝐵)) ∧ 𝐵 <s 𝐴))
Theorem	leftlt 28083	A member of a surreal's left set is less than it. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( L ‘𝐵) → 𝐴 <s 𝐵)
Theorem	rightgt 28084	A member of a surreal's right set is greater than it. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( R ‘𝐵) → 𝐵 <s 𝐴)
Theorem	leftf 28085	The functionality of the left options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ L : No ⟶𝒫 No
Theorem	rightf 28086	The functionality of the right options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ R : No ⟶𝒫 No
Theorem	elmade 28087*	Membership in the made function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ (𝐴 ∈ On → (𝑋 ∈ ( M ‘𝐴) ↔ ∃𝑙 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑋)))
Theorem	elmade2 28088*	Membership in the made function in terms of the old function. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (𝐴 ∈ On → (𝑋 ∈ ( M ‘𝐴) ↔ ∃𝑙 ∈ 𝒫 ( O ‘𝐴)∃𝑟 ∈ 𝒫 ( O ‘𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑋)))
Theorem	elold 28089*	Membership in an old set. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (𝐴 ∈ On → (𝑋 ∈ ( O ‘𝐴) ↔ ∃𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘𝑏)))
Theorem	sltsleft 28090	A surreal is greater than its left options. Theorem 0(ii) of [Conway] p. 16. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (𝐴 ∈ No → ( L ‘𝐴) <<s {𝐴})
Theorem	sltsright 28091	A surreal is less than its right options. Theorem 0(i) of [Conway] p. 16. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (𝐴 ∈ No → {𝐴} <<s ( R ‘𝐴))
Theorem	lltr 28092	The left options of a surreal are strictly less than the right options of the same surreal. (Contributed by Scott Fenton, 6-Aug-2024.) (Revised by Scott Fenton, 21-Feb-2025.)
⊢ ( L ‘𝐴) <<s ( R ‘𝐴)
Theorem	made0 28093	The only surreal made on day ∅ is 0s. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ ( M ‘∅) = { 0s }
Theorem	new0 28094	The only surreal new on day ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ( N ‘∅) = { 0s }
Theorem	old1 28095	The only surreal older than 1o is 0s. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ( O ‘1o) = { 0s }
Theorem	madess 28096	If 𝐴 is less than or equal to ordinal 𝐵, then the made set of 𝐴 is included in the made set of 𝐵. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ((𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵) → ( M ‘𝐴) ⊆ ( M ‘𝐵))
Theorem	oldssmade 28097	The older-than set is a subset of the made set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( O ‘𝐴) ⊆ ( M ‘𝐴)
Theorem	oldmade 28098	An element of an old set is an element of a made set. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ ( O ‘𝐵) → 𝐴 ∈ ( M ‘𝐵))
Theorem	oldmaded 28099	An element of an old set is an element of a made set. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ ( O ‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ ( M ‘𝐵))
Theorem	oldss 28100	If 𝐴 is less than or equal to ordinal 𝐵, then the old set of 𝐴 is included in the made set of 𝐵. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ((𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵) → ( O ‘𝐴) ⊆ ( O ‘𝐵))