P. 279 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27801-27900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	noetalem2 27801*	Lemma for noeta 27802. The full statement of the theorem with hypotheses in place. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    &   ⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    ⇒   ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → ∃𝑐 ∈ No (∀𝑎 ∈ 𝐴 𝑎 <s 𝑐 ∧ ∀𝑏 ∈ 𝐵 𝑐 <s 𝑏 ∧ ( bday ‘𝑐) ⊆ 𝑂))
Theorem	noeta 27802*	The full-eta axiom for the surreal numbers. This is the single most important property of the surreals. It says that, given two sets of surreals such that one comes completely before the other, there is a surreal lying strictly between the two. Furthermore, if the birthdays of members of 𝐴 and 𝐵 are strictly bounded above by 𝑂, then 𝑂 non-strictly bounds the separator. Axiom FE of [Alling] p. 185. (Contributed by Scott Fenton, 9-Aug-2024.)
⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → ∃𝑧 ∈ No (∀𝑥 ∈ 𝐴 𝑥 <s 𝑧 ∧ ∀𝑦 ∈ 𝐵 𝑧 <s 𝑦 ∧ ( bday ‘𝑧) ⊆ 𝑂))
15.2  Initial consequences of Alling's axioms
15.2.1  Ordering Theorems
Syntax	csle 27803	Declare the syntax for surreal less-than or equal.
class ≤s
Definition	df-sle 27804	Define the surreal less-than or equal predicate. Compare df-le 11298. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ ≤s = (( No × No ) ∖ ◡ <s )
Theorem	sltirr 27805	Surreal less-than is irreflexive. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (𝐴 ∈ No → ¬ 𝐴 <s 𝐴)
Theorem	slttr 27806	Surreal less-than is transitive. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 <s 𝐵 ∧ 𝐵 <s 𝐶) → 𝐴 <s 𝐶))
Theorem	sltasym 27807	Surreal less-than is asymmetric. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ¬ 𝐵 <s 𝐴))
Theorem	sltlin 27808	Surreal less-than obeys trichotomy. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 <s 𝐴))
Theorem	slttrieq2 27809	Trichotomy law for surreal less-than. (Contributed by Scott Fenton, 22-Apr-2012.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 = 𝐵 ↔ (¬ 𝐴 <s 𝐵 ∧ ¬ 𝐵 <s 𝐴)))
Theorem	slttrine 27810	Trichotomy law for surreals. (Contributed by Scott Fenton, 23-Nov-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ≠ 𝐵 ↔ (𝐴 <s 𝐵 ∨ 𝐵 <s 𝐴)))
Theorem	slenlt 27811	Surreal less-than or equal in terms of less-than. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴))
Theorem	sltnle 27812	Surreal less-than in terms of less-than or equal. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ¬ 𝐵 ≤s 𝐴))
Theorem	sleloe 27813	Surreal less-than or equal in terms of less-than. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ≤s 𝐵 ↔ (𝐴 <s 𝐵 ∨ 𝐴 = 𝐵)))
Theorem	sletri3 27814	Trichotomy law for surreal less-than or equal. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 = 𝐵 ↔ (𝐴 ≤s 𝐵 ∧ 𝐵 ≤s 𝐴)))
Theorem	sltletr 27815	Surreal transitive law. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 <s 𝐵 ∧ 𝐵 ≤s 𝐶) → 𝐴 <s 𝐶))
Theorem	slelttr 27816	Surreal transitive law. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 ≤s 𝐵 ∧ 𝐵 <s 𝐶) → 𝐴 <s 𝐶))
Theorem	sletr 27817	Surreal transitive law. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 ≤s 𝐵 ∧ 𝐵 ≤s 𝐶) → 𝐴 ≤s 𝐶))
Theorem	slttrd 27818	Surreal less-than is transitive. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    &   ⊢ (𝜑 → 𝐵 <s 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 <s 𝐶)
Theorem	sltletrd 27819	Surreal less-than is transitive. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    &   ⊢ (𝜑 → 𝐵 ≤s 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 <s 𝐶)
Theorem	slelttrd 27820	Surreal less-than is transitive. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐴 ≤s 𝐵)    &   ⊢ (𝜑 → 𝐵 <s 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 <s 𝐶)
Theorem	sletrd 27821	Surreal less-than or equal is transitive. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐴 ≤s 𝐵)    &   ⊢ (𝜑 → 𝐵 ≤s 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≤s 𝐶)
Theorem	slerflex 27822	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 27823	Surreal trichotomy law. (Contributed by Scott Fenton, 14-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ≤s 𝐵 ∨ 𝐵 ≤s 𝐴))
Theorem	maxs1 27824	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 27825	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 27826	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 27827	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 27828	Surreal less-than implies less-than or equal. (Contributed by Scott Fenton, 16-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≤s 𝐵)
Theorem	sltne 27829	Surreal less-than implies not equal. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐴 <s 𝐵) → 𝐵 ≠ 𝐴)
Theorem	sltlend 27830	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 27831	The birthday function is a function. (Contributed by Scott Fenton, 14-Jun-2011.)
⊢ Fun bday
Theorem	bdayfn 27832	The birthday function is a function over No . (Contributed by Scott Fenton, 30-Jun-2011.)
⊢ bday Fn No
Theorem	bdaydm 27833	The birthday function's domain is No . (Contributed by Scott Fenton, 14-Jun-2011.)
⊢ dom bday = No
Theorem	bdayrn 27834	The birthday function's range is On. (Contributed by Scott Fenton, 14-Jun-2011.)
⊢ ran bday = On
Theorem	bdayelon 27835	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	nocvxminlem 27836*	Lemma for nocvxmin 27837. 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 27837*	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 27838	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 27839	Declare the syntax for surreal set less-than.
class <<s
Definition	df-sslt 27840*	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 27841	Declare the syntax for the surreal cut operator.
class |s
Definition	df-scut 27842*	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 27843*	A version of noeta 27802 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 27844*	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 27845	The first argument of surreal set less-than exists. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V)
Theorem	ssltex2 27846	The second argument of surreal set less-than exists. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V)
Theorem	ssltss1 27847	The first argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No )
Theorem	ssltss2 27848	The second argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No )
Theorem	ssltsep 27849*	The separation property of surreal set less-than. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)
Theorem	ssltd 27850*	Deduce surreal set less-than. (Contributed by Scott Fenton, 24-Sep-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ No )    &   ⊢ (𝜑 → 𝐵 ⊆ No )    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 <s 𝑦)    ⇒   ⊢ (𝜑 → 𝐴 <<s 𝐵)
Theorem	ssltsn 27851	Surreal set less-than of two singletons. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    ⇒   ⊢ (𝜑 → {𝐴} <<s {𝐵})
Theorem	ssltsepc 27852	Two elements of separated sets obey less-than. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝑋 <s 𝑌)
Theorem	ssltsepcd 27853	Two elements of separated sets obey less-than. Deduction form of ssltsepc 27852. (Contributed by Scott Fenton, 25-Sep-2024.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 <s 𝑌)
Theorem	sssslt1 27854	Relation between surreal set less-than and subset. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴) → 𝐶 <<s 𝐵)
Theorem	sssslt2 27855	Relation between surreal set less-than and subset. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐴 <<s 𝐶)
Theorem	nulsslt 27856	The empty set is less-than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 ∈ 𝒫 No → ∅ <<s 𝐴)
Theorem	nulssgt 27857	The empty set is greater than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 ∈ 𝒫 No → 𝐴 <<s ∅)
Theorem	conway 27858*	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 27859*	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 27860	Cut properties of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
Theorem	scutcl 27861	Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.)
⊢ (𝐴 <<s 𝐵 → (𝐴 |s 𝐵) ∈ No )
Theorem	scutcld 27862	Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) ∈ No )
Theorem	scutbday 27863*	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 27864*	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 27865*	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 27866	Transitive law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ∧ 𝐵 ≠ ∅) → 𝐴 <<s 𝐶)
Theorem	ssltun1 27867	Union law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → (𝐴 ∪ 𝐵) <<s 𝐶)
Theorem	ssltun2 27868	Union law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s (𝐵 ∪ 𝐶))
Theorem	scutun12 27869	Union law for surreal cuts. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → ((𝐴 ∪ 𝐶) |s (𝐵 ∪ 𝐷)) = (𝐴 |s 𝐵))
Theorem	dmscut 27870	The domain of the surreal cut operation is all separated surreal sets. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ dom |s = <<s
Theorem	scutf 27871	Functionality statement for the surreal cut operator. (Contributed by Scott Fenton, 15-Dec-2021.)
⊢ |s : <<s ⟶ No
Theorem	etasslt 27872*	A restatement of noeta 27802 using set less-than. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂) → ∃𝑥 ∈ No (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday ‘𝑥) ⊆ 𝑂))
Theorem	etasslt2 27873*	A version of etasslt 27872 with fewer hypotheses but a weaker upper bound. (Contributed by Scott Fenton, 10-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ∃𝑥 ∈ No (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday ‘𝑥) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))))
Theorem	scutbdaybnd 27874	An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂) → ( bday ‘(𝐴 |s 𝐵)) ⊆ 𝑂)
Theorem	scutbdaybnd2 27875	An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵)))
Theorem	scutbdaybnd2lim 27876	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 27877	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 27878*	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	sltrec 27879*	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	ssltdisj 27880	If 𝐴 preceeds 𝐵, then 𝐴 and 𝐵 are disjoint. (Contributed by Scott Fenton, 18-Sep-2024.)
⊢ (𝐴 <<s 𝐵 → (𝐴 ∩ 𝐵) = ∅)
15.3.2  Zero and One
Syntax	c0s 27881	Declare the class syntax for surreal zero.
class 0s
Syntax	c1s 27882	Declare the class syntax for surreal one.
class 1s
Definition	df-0s 27883	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 27884	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 27885	Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 0s ∈ No
Theorem	1sno 27886	Surreal one is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 1s ∈ No
Theorem	bday0s 27887	Calculate the birthday of surreal zero. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ ( bday ‘ 0s ) = ∅
Theorem	0slt1s 27888	Surreal zero is less than surreal one. Theorem from [Conway] p. 7. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 0s <s 1s
Theorem	bday0b 27889	The only surreal with birthday ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝑋 ∈ No → (( bday ‘𝑋) = ∅ ↔ 𝑋 = 0s ))
Theorem	bday1s 27890	The birthday of surreal one is ordinal one. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ( bday ‘ 1s ) = 1o
Theorem	cuteq0 27891	Condition for a surreal cut to equal zero. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝜑 → 𝐴 <<s { 0s })    &   ⊢ (𝜑 → { 0s } <<s 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = 0s )
Theorem	cuteq1 27892	Condition for a surreal cut to equal one. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (𝜑 → 0s ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 <<s { 1s })    &   ⊢ (𝜑 → { 1s } <<s 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = 1s )
Theorem	sgt0ne0 27893	A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ ( 0s <s 𝐴 → 𝐴 ≠ 0s )
Theorem	sgt0ne0d 27894	A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (𝜑 → 0s <s 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0s )
15.3.3  Cuts and Options
Syntax	cmade 27895	Declare the symbol for the made by function.
class M
Syntax	cold 27896	Declare the symbol for the older than function.
class O
Syntax	cnew 27897	Declare the symbol for the new on function.
class N
Syntax	cleft 27898	Declare the symbol for the left option function.
class L
Syntax	cright 27899	Declare the symbol for the right option function.
class R
Definition	df-made 27900	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 𝑓))))