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
Syntax	cscut 27701	Declare the syntax for the surreal cut operator.
class |s
Definition	df-scut 27702*	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 27703*	A version of noeta 27662 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 27704*	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 27705	The first argument of surreal set less-than exists. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V)
Theorem	ssltex2 27706	The second argument of surreal set less-than exists. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V)
Theorem	ssltss1 27707	The first argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No )
Theorem	ssltss2 27708	The second argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No )
Theorem	ssltsep 27709*	The separation property of surreal set less-than. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)
Theorem	ssltd 27710*	Deduce surreal set less-than. (Contributed by Scott Fenton, 24-Sep-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ No )    &   ⊢ (𝜑 → 𝐵 ⊆ No )    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 <s 𝑦)    ⇒   ⊢ (𝜑 → 𝐴 <<s 𝐵)
Theorem	ssltsn 27711	Surreal set less-than of two singletons. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    ⇒   ⊢ (𝜑 → {𝐴} <<s {𝐵})
Theorem	ssltsepc 27712	Two elements of separated sets obey less-than. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝑋 <s 𝑌)
Theorem	ssltsepcd 27713	Two elements of separated sets obey less-than. Deduction form of ssltsepc 27712. (Contributed by Scott Fenton, 25-Sep-2024.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 <s 𝑌)
Theorem	sssslt1 27714	Relation between surreal set less-than and subset. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴) → 𝐶 <<s 𝐵)
Theorem	sssslt2 27715	Relation between surreal set less-than and subset. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐴 <<s 𝐶)
Theorem	nulsslt 27716	The empty set is less-than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 ∈ 𝒫 No → ∅ <<s 𝐴)
Theorem	nulssgt 27717	The empty set is greater than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 ∈ 𝒫 No → 𝐴 <<s ∅)
Theorem	conway 27718*	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 27719*	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 27720	Cut properties of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
Theorem	scutcl 27721	Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.)
⊢ (𝐴 <<s 𝐵 → (𝐴 |s 𝐵) ∈ No )
Theorem	scutcld 27722	Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) ∈ No )
Theorem	scutbday 27723*	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 27724*	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 27725*	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 27726	Transitive law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ∧ 𝐵 ≠ ∅) → 𝐴 <<s 𝐶)
Theorem	ssltun1 27727	Union law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → (𝐴 ∪ 𝐵) <<s 𝐶)
Theorem	ssltun2 27728	Union law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s (𝐵 ∪ 𝐶))
Theorem	scutun12 27729	Union law for surreal cuts. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → ((𝐴 ∪ 𝐶) |s (𝐵 ∪ 𝐷)) = (𝐴 |s 𝐵))
Theorem	dmscut 27730	The domain of the surreal cut operation is all separated surreal sets. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ dom |s = <<s
Theorem	scutf 27731	Functionality statement for the surreal cut operator. (Contributed by Scott Fenton, 15-Dec-2021.)
⊢ |s : <<s ⟶ No
Theorem	etasslt 27732*	A restatement of noeta 27662 using set less-than. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂) → ∃𝑥 ∈ No (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday ‘𝑥) ⊆ 𝑂))
Theorem	etasslt2 27733*	A version of etasslt 27732 with fewer hypotheses but a weaker upper bound. (Contributed by Scott Fenton, 10-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ∃𝑥 ∈ No (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday ‘𝑥) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))))
Theorem	scutbdaybnd 27734	An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂) → ( bday ‘(𝐴 |s 𝐵)) ⊆ 𝑂)
Theorem	scutbdaybnd2 27735	An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵)))
Theorem	scutbdaybnd2lim 27736	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 27737	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 27738*	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 27739*	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 27740	If 𝐴 preceeds 𝐵, then 𝐴 and 𝐵 are disjoint. (Contributed by Scott Fenton, 18-Sep-2024.)
⊢ (𝐴 <<s 𝐵 → (𝐴 ∩ 𝐵) = ∅)
15.3.2  Zero and One
Syntax	c0s 27741	Declare the class syntax for surreal zero.
class 0s
Syntax	c1s 27742	Declare the class syntax for surreal one.
class 1s
Definition	df-0s 27743	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 27744	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 27745	Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 0s ∈ No
Theorem	1sno 27746	Surreal one is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 1s ∈ No
Theorem	bday0s 27747	Calculate the birthday of surreal zero. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ ( bday ‘ 0s ) = ∅
Theorem	0slt1s 27748	Surreal zero is less than surreal one. Theorem from [Conway] p. 7. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 0s <s 1s
Theorem	bday0b 27749	The only surreal with birthday ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝑋 ∈ No → (( bday ‘𝑋) = ∅ ↔ 𝑋 = 0s ))
Theorem	bday1s 27750	The birthday of surreal one is ordinal one. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ( bday ‘ 1s ) = 1o
Theorem	cuteq0 27751	Condition for a surreal cut to equal zero. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝜑 → 𝐴 <<s { 0s })    &   ⊢ (𝜑 → { 0s } <<s 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = 0s )
Theorem	cutneg 27752	The simplest number greater than a negative number is zero. (Contributed by Scott Fenton, 4-Sep-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 0s )    ⇒   ⊢ (𝜑 → ({𝐴} |s ∅) = 0s )
Theorem	cuteq1 27753	Condition for a surreal cut to equal one. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (𝜑 → 0s ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 <<s { 1s })    &   ⊢ (𝜑 → { 1s } <<s 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = 1s )
Theorem	sgt0ne0 27754	A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ ( 0s <s 𝐴 → 𝐴 ≠ 0s )
Theorem	sgt0ne0d 27755	A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (𝜑 → 0s <s 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0s )
Theorem	1sne0s 27756	Surreal zero does not equal surreal one. (Contributed by Scott Fenton, 5-Sep-2025.)
⊢ 1s ≠ 0s
15.3.3  Cuts and Options
Syntax	cmade 27757	Declare the symbol for the made by function.
class M
Syntax	cold 27758	Declare the symbol for the older than function.
class O
Syntax	cnew 27759	Declare the symbol for the new on function.
class N
Syntax	cleft 27760	Declare the symbol for the left option function.
class L
Syntax	cright 27761	Declare the symbol for the right option function.
class R
Definition	df-made 27762	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 27763	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 27764	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 27765*	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 27766*	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 27767	The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))))
Theorem	madeval2 27768*	Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ (𝐴 ∈ On → ( M ‘𝐴) = {𝑥 ∈ No ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)})
Theorem	oldval 27769	The value of the old options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ (𝐴 ∈ On → ( O ‘𝐴) = ∪ ( M “ 𝐴))
Theorem	newval 27770	The value of the new options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( N ‘𝐴) = (( M ‘𝐴) ∖ ( O ‘𝐴))
Theorem	madef 27771	The made function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ M :On⟶𝒫 No
Theorem	oldf 27772	The older function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ O :On⟶𝒫 No
Theorem	newf 27773	The new function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ N :On⟶𝒫 No
Theorem	old0 27774	No surreal is older than ∅. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ ( O ‘∅) = ∅
Theorem	madessno 27775	Made sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( M ‘𝐴) ⊆ No
Theorem	oldssno 27776	Old sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( O ‘𝐴) ⊆ No
Theorem	newssno 27777	New sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( N ‘𝐴) ⊆ No
Theorem	leftval 27778*	The value of the left options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( L ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝑥 <s 𝐴}
Theorem	rightval 27779*	The value of the right options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( R ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝐴 <s 𝑥}
Theorem	elleft 27780	Membership in the left set of a surreal. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( L ‘𝐵) ↔ (𝐴 ∈ ( O ‘( bday ‘𝐵)) ∧ 𝐴 <s 𝐵))
Theorem	elright 27781	Membership in the right set of a surreal. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( R ‘𝐵) ↔ (𝐴 ∈ ( O ‘( bday ‘𝐵)) ∧ 𝐵 <s 𝐴))
Theorem	leftlt 27782	A member of a surreal's left set is less than it. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( L ‘𝐵) → 𝐴 <s 𝐵)
Theorem	rightgt 27783	A member of a surreal's right set is greater than it. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( R ‘𝐵) → 𝐵 <s 𝐴)
Theorem	leftf 27784	The functionality of the left options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ L : No ⟶𝒫 No
Theorem	rightf 27785	The functionality of the right options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ R : No ⟶𝒫 No
Theorem	elmade 27786*	Membership in the made function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ (𝐴 ∈ On → (𝑋 ∈ ( M ‘𝐴) ↔ ∃𝑙 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑋)))
Theorem	elmade2 27787*	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 27788*	Membership in an old set. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (𝐴 ∈ On → (𝑋 ∈ ( O ‘𝐴) ↔ ∃𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘𝑏)))
Theorem	ssltleft 27789	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	ssltright 27790	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	lltropt 27791	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 27792	The only surreal made on day ∅ is 0s. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ ( M ‘∅) = { 0s }
Theorem	new0 27793	The only surreal new on day ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ( N ‘∅) = { 0s }
Theorem	old1 27794	The only surreal older than 1o is 0s. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ( O ‘1o) = { 0s }
Theorem	madess 27795	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 27796	The older-than set is a subset of the made set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( O ‘𝐴) ⊆ ( M ‘𝐴)
Theorem	leftssold 27797	The left options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
Theorem	rightssold 27798	The right options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
Theorem	leftssno 27799	The left set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( L ‘𝐴) ⊆ No
Theorem	rightssno 27800	The right set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( R ‘𝐴) ⊆ No