P. 278 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27701-27800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	slelttrd 27701	Surreal less-than is transitive. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐴 ≤s 𝐵)    &   ⊢ (𝜑 → 𝐵 <s 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 <s 𝐶)
Theorem	sletrd 27702	Surreal less-than or equal is transitive. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐴 ≤s 𝐵)    &   ⊢ (𝜑 → 𝐵 ≤s 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≤s 𝐶)
Theorem	slerflex 27703	Surreal less-than or equal is reflexive. Theorem 0(iii) of [Conway] p. 16. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (𝐴 ∈ No → 𝐴 ≤s 𝐴)
Theorem	sletric 27704	Surreal trichotomy law. (Contributed by Scott Fenton, 14-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ≤s 𝐵 ∨ 𝐵 ≤s 𝐴))
Theorem	maxs1 27705	A surreal is less than or equal to the maximum of it and another. (Contributed by Scott Fenton, 14-Feb-2025.)
⊢ (𝐴 ∈ No → 𝐴 ≤s if(𝐴 ≤s 𝐵, 𝐵, 𝐴))
Theorem	maxs2 27706	A surreal is less than or equal to the maximum of it and another. (Contributed by Scott Fenton, 14-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝐵 ≤s if(𝐴 ≤s 𝐵, 𝐵, 𝐴))
Theorem	mins1 27707	The minimum of two surreals is less than or equal to the first. (Contributed by Scott Fenton, 14-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → if(𝐴 ≤s 𝐵, 𝐴, 𝐵) ≤s 𝐴)
Theorem	mins2 27708	The minimum of two surreals is less than or equal to the second. (Contributed by Scott Fenton, 14-Feb-2025.)
⊢ (𝐵 ∈ No → if(𝐴 ≤s 𝐵, 𝐴, 𝐵) ≤s 𝐵)
Theorem	sltled 27709	Surreal less-than implies less-than or equal. (Contributed by Scott Fenton, 16-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≤s 𝐵)
Theorem	sltne 27710	Surreal less-than implies not equal. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐴 <s 𝐵) → 𝐵 ≠ 𝐴)
Theorem	sltlend 27711	Surreal less-than in terms of less-than or equal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐴 ≤s 𝐵 ∧ 𝐵 ≠ 𝐴)))
15.2.2  Birthday Theorems
Theorem	bdayfun 27712	The birthday function is a function. (Contributed by Scott Fenton, 14-Jun-2011.)
⊢ Fun bday
Theorem	bdayfn 27713	The birthday function is a function over No . (Contributed by Scott Fenton, 30-Jun-2011.)
⊢ bday Fn No
Theorem	bdaydm 27714	The birthday function's domain is No . (Contributed by Scott Fenton, 14-Jun-2011.)
⊢ dom bday = No
Theorem	bdayrn 27715	The birthday function's range is On. (Contributed by Scott Fenton, 14-Jun-2011.)
⊢ ran bday = On
Theorem	bdayelon 27716	The value of the birthday function is always an ordinal. (Contributed by Scott Fenton, 14-Jun-2011.) (Proof shortened by Scott Fenton, 8-Dec-2021.)
⊢ ( bday ‘𝐴) ∈ On
Theorem	nobdaymin 27717*	Any non-empty class of surreals has a birthday-minimal element. (Contributed by Scott Fenton, 11-Dec-2025.)
⊢ ((𝐴 ⊆ No ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ( bday ‘𝑥) = ∩ ( bday “ 𝐴))
Theorem	nocvxminlem 27718*	Lemma for nocvxmin 27719. Given two birthday-minimal elements of a convex class of surreals, they are not comparable. (Contributed by Scott Fenton, 30-Jun-2011.)
⊢ ((𝐴 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No ((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → (((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday ‘𝑋) = ∩ ( bday “ 𝐴) ∧ ( bday ‘𝑌) = ∩ ( bday “ 𝐴))) → ¬ 𝑋 <s 𝑌))
Theorem	nocvxmin 27719*	Given a nonempty convex class of surreals, there is a unique birthday-minimal element of that class. Lemma 0 of [Alling] p. 185. (Contributed by Scott Fenton, 30-Jun-2011.)
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No ((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → ∃!𝑤 ∈ 𝐴 ( bday ‘𝑤) = ∩ ( bday “ 𝐴))
Theorem	noprc 27720	The surreal numbers are a proper class. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ ¬ No ∈ V
15.3  Conway cut representation In [Conway] surreal numbers are represented as equivalence classes of cuts of previously defined surreal numbers. This is complicated to handle in ZFC without classes so we do not make it our definition. However, we can define a cut operator on surreals that behaves similarly. We introduce such an operator in this section and use it to define all surreals hearafter.
15.3.1  Conway cuts
Syntax	csslt 27721	Declare the syntax for surreal set less-than.
class <<s
Definition	df-sslt 27722*	Define the relation that holds iff one set of surreals completely precedes another. (Contributed by Scott Fenton, 7-Dec-2021.)
⊢ <<s = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥 <s 𝑦)}
Syntax	cscut 27723	Declare the syntax for the surreal cut operator.
class |s
Definition	df-scut 27724*	Define the cut operator on surreal numbers. This operator, which Conway takes as the primitive operator over surreals, picks the surreal lying between two sets of surreals of minimal birthday. Definition from [Gonshor] p. 7. (Contributed by Scott Fenton, 7-Dec-2021.)
⊢ |s = (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
Theorem	noeta2 27725*	A version of noeta 27683 with fewer hypotheses but a weaker upper bound (Contributed by Scott Fenton, 7-Dec-2021.)
⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) → ∃𝑧 ∈ No (∀𝑥 ∈ 𝐴 𝑥 <s 𝑧 ∧ ∀𝑦 ∈ 𝐵 𝑧 <s 𝑦 ∧ ( bday ‘𝑧) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))))
Theorem	brsslt 27726*	Binary relation form of the surreal set less-than relation. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)))
Theorem	ssltex1 27727	The first argument of surreal set less-than exists. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V)
Theorem	ssltex2 27728	The second argument of surreal set less-than exists. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V)
Theorem	ssltss1 27729	The first argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No )
Theorem	ssltss2 27730	The second argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No )
Theorem	ssltsep 27731*	The separation property of surreal set less-than. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)
Theorem	ssltd 27732*	Deduce surreal set less-than. (Contributed by Scott Fenton, 24-Sep-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ No )    &   ⊢ (𝜑 → 𝐵 ⊆ No )    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 <s 𝑦)    ⇒   ⊢ (𝜑 → 𝐴 <<s 𝐵)
Theorem	ssltsnb 27733	Surreal set less-than of two singletons. (Contributed by Scott Fenton, 18-Jan-2026.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ({𝐴} <<s {𝐵} ↔ 𝐴 <s 𝐵))
Theorem	ssltsn 27734	Surreal set less-than of two singletons. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    ⇒   ⊢ (𝜑 → {𝐴} <<s {𝐵})
Theorem	ssltsepc 27735	Two elements of separated sets obey less-than. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝑋 <s 𝑌)
Theorem	ssltsepcd 27736	Two elements of separated sets obey less-than. Deduction form of ssltsepc 27735. (Contributed by Scott Fenton, 25-Sep-2024.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 <s 𝑌)
Theorem	sssslt1 27737	Relation between surreal set less-than and subset. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴) → 𝐶 <<s 𝐵)
Theorem	sssslt2 27738	Relation between surreal set less-than and subset. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐴 <<s 𝐶)
Theorem	nulsslt 27739	The empty set is less-than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 ∈ 𝒫 No → ∅ <<s 𝐴)
Theorem	nulssgt 27740	The empty set is greater than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 ∈ 𝒫 No → 𝐴 <<s ∅)
Theorem	conway 27741*	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	scutval 27742*	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	scutcut 27743	Cut properties of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
Theorem	scutcl 27744	Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.)
⊢ (𝐴 <<s 𝐵 → (𝐴 |s 𝐵) ∈ No )
Theorem	scutcld 27745	Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) ∈ No )
Theorem	scutbday 27746*	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	eqscut 27747*	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	eqscut2 27748*	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	sslttr 27749	Transitive law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ∧ 𝐵 ≠ ∅) → 𝐴 <<s 𝐶)
Theorem	ssltun1 27750	Union law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → (𝐴 ∪ 𝐵) <<s 𝐶)
Theorem	ssltun2 27751	Union law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s (𝐵 ∪ 𝐶))
Theorem	scutun12 27752	Union law for surreal cuts. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → ((𝐴 ∪ 𝐶) |s (𝐵 ∪ 𝐷)) = (𝐴 |s 𝐵))
Theorem	dmscut 27753	The domain of the surreal cut operation is all separated surreal sets. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ dom |s = <<s
Theorem	scutf 27754	Functionality statement for the surreal cut operator. (Contributed by Scott Fenton, 15-Dec-2021.)
⊢ |s : <<s ⟶ No
Theorem	etasslt 27755*	A restatement of noeta 27683 using set less-than. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂) → ∃𝑥 ∈ No (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday ‘𝑥) ⊆ 𝑂))
Theorem	etasslt2 27756*	A version of etasslt 27755 with fewer hypotheses but a weaker upper bound. (Contributed by Scott Fenton, 10-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ∃𝑥 ∈ No (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday ‘𝑥) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))))
Theorem	scutbdaybnd 27757	An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂) → ( bday ‘(𝐴 |s 𝐵)) ⊆ 𝑂)
Theorem	scutbdaybnd2 27758	An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵)))
Theorem	scutbdaybnd2lim 27759	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	scutbdaylt 27760	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	slerec 27761*	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	slerecd 27762*	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	sltrec 27763*	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	sltrecd 27764*	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	ssltdisj 27765	If 𝐴 preceeds 𝐵, then 𝐴 and 𝐵 are disjoint. (Contributed by Scott Fenton, 18-Sep-2024.)
⊢ (𝐴 <<s 𝐵 → (𝐴 ∩ 𝐵) = ∅)
Theorem	eqscut3 27766*	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 27767	Declare the class syntax for surreal zero.
class 0s
Syntax	c1s 27768	Declare the class syntax for surreal one.
class 1s
Definition	df-0s 27769	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 27770	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	0sno 27771	Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 0s ∈ No
Theorem	1sno 27772	Surreal one is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 1s ∈ No
Theorem	bday0s 27773	Calculate the birthday of surreal zero. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ ( bday ‘ 0s ) = ∅
Theorem	0slt1s 27774	Surreal zero is less than surreal one. Theorem from [Conway] p. 7. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 0s <s 1s
Theorem	bday0b 27775	The only surreal with birthday ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝑋 ∈ No → (( bday ‘𝑋) = ∅ ↔ 𝑋 = 0s ))
Theorem	bday1s 27776	The birthday of surreal one is ordinal one. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ( bday ‘ 1s ) = 1o
Theorem	cuteq0 27777	Condition for a surreal cut to equal zero. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝜑 → 𝐴 <<s { 0s })    &   ⊢ (𝜑 → { 0s } <<s 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = 0s )
Theorem	cutneg 27778	The simplest number greater than a negative number is zero. (Contributed by Scott Fenton, 4-Sep-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 0s )    ⇒   ⊢ (𝜑 → ({𝐴} |s ∅) = 0s )
Theorem	cuteq1 27779	Condition for a surreal cut to equal one. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (𝜑 → 0s ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 <<s { 1s })    &   ⊢ (𝜑 → { 1s } <<s 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = 1s )
Theorem	sgt0ne0 27780	A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ ( 0s <s 𝐴 → 𝐴 ≠ 0s )
Theorem	sgt0ne0d 27781	A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (𝜑 → 0s <s 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0s )
Theorem	1sne0s 27782	Surreal zero does not equal surreal one. (Contributed by Scott Fenton, 5-Sep-2025.)
⊢ 1s ≠ 0s
Theorem	rightpos 27783*	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 27784	Declare the symbol for the made by function.
class M
Syntax	cold 27785	Declare the symbol for the older than function.
class O
Syntax	cnew 27786	Declare the symbol for the new on function.
class N
Syntax	cleft 27787	Declare the symbol for the left option function.
class L
Syntax	cright 27788	Declare the symbol for the right option function.
class R
Definition	df-made 27789	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 27790	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 27791	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 27792*	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 27793*	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 27794	The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))))
Theorem	madeval2 27795*	Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ (𝐴 ∈ On → ( M ‘𝐴) = {𝑥 ∈ No ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)})
Theorem	oldval 27796	The value of the old options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ (𝐴 ∈ On → ( O ‘𝐴) = ∪ ( M “ 𝐴))
Theorem	newval 27797	The value of the new options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( N ‘𝐴) = (( M ‘𝐴) ∖ ( O ‘𝐴))
Theorem	madef 27798	The made function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ M :On⟶𝒫 No
Theorem	oldf 27799	The older function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ O :On⟶𝒫 No
Theorem	newf 27800	The new function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ N :On⟶𝒫 No