P. 283 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28201-28300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	0no 28201	Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 0s ∈ No
Theorem	1no 28202	Surreal one is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 1s ∈ No
Theorem	bday0 28203	Calculate the birthday of surreal zero. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (bday‘ 0s ) = ∅
Theorem	0lt1s 28204	Surreal zero is less than surreal one. Theorem from [Conway] p. 7. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 0s <s 1s
Theorem	bday0b 28205	The only surreal with birthday ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝑋 ∈ No → ((bday‘𝑋) = ∅ ↔ 𝑋 = 0s ))
Theorem	bday1 28206	The birthday of surreal one is ordinal one. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (bday‘ 1s ) = 1o
Theorem	cuteq0 28207	Condition for a surreal cut to equal zero. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝜑 → 𝐴 <<s { 0s })    &   ⊢ (𝜑 → { 0s } <<s 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = 0s )
Theorem	cutneg 28208	The simplest number greater than a negative number is zero. (Contributed by Scott Fenton, 4-Sep-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐴 <s 0s )    ⇒   ⊢ (𝜑 → ({𝐴} |s ∅) = 0s )
Theorem	cuteq1 28209	Condition for a surreal cut to equal one. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (𝜑 → 0s ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 <<s { 1s })    &   ⊢ (𝜑 → { 1s } <<s 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = 1s )
Theorem	gt0ne0s 28210	A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ ( 0s <s 𝐴 → 𝐴 ≠ 0s )
Theorem	gt0ne0sd 28211	A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (𝜑 → 0s <s 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0s )
Theorem	1ne0s 28212	Surreal zero does not equal surreal one. (Contributed by Scott Fenton, 5-Sep-2025.)
⊢ 1s ≠ 0s
Theorem	rightge0 28213*	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 28214	Declare the symbol for the made by function.
class M
Syntax	cold 28215	Declare the symbol for the older than function.
class O
Syntax	cnew 28216	Declare the symbol for the new on function.
class N
Syntax	cleft 28217	Declare the symbol for the left option function.
class L
Syntax	cright 28218	Declare the symbol for the right option function.
class R
Definition	df-made 28219	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 28220	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 28221	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 28222*	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 28223*	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 28224	The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ (𝐴 ∈ On → (M‘𝐴) = ( |s “ (𝒫 ∪ (M “ 𝐴) × 𝒫 ∪ (M “ 𝐴))))
Theorem	madeval2 28225*	Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ (𝐴 ∈ On → (M‘𝐴) = {𝑥 ∈ No ∣ ∃𝑎 ∈ 𝒫 ∪ (M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ (M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)})
Theorem	oldval 28226	The value of the old options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ (𝐴 ∈ On → (O‘𝐴) = ∪ (M “ 𝐴))
Theorem	newval 28227	The value of the new options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ (N‘𝐴) = ((M‘𝐴) ∖ (O‘𝐴))
Theorem	madef 28228	The made function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ M:On⟶𝒫 No
Theorem	oldf 28229	The older function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ O:On⟶𝒫 No
Theorem	newf 28230	The new function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ N:On⟶𝒫 No
Theorem	old0 28231	No surreal is older than ∅. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (O‘∅) = ∅
Theorem	madessno 28232	Made sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ (M‘𝐴) ⊆ No
Theorem	oldssno 28233	Old sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ (O‘𝐴) ⊆ No
Theorem	newssno 28234	New sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ (N‘𝐴) ⊆ No
Theorem	madeno 28235	An element of a made set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ (M‘𝐵) → 𝐴 ∈ No)
Theorem	oldno 28236	An element of an old set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ (O‘𝐵) → 𝐴 ∈ No)
Theorem	newno 28237	An element of a new set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ (N‘𝐵) → 𝐴 ∈ No)
Theorem	madenod 28238	An element of a made set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ (M‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ No)
Theorem	oldnod 28239	An element of an old set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ (O‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ No)
Theorem	newnod 28240	An element of a new set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ (N‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ No)
Theorem	leftval 28241*	The value of the left options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ (L‘𝐴) = {𝑥 ∈ (O‘(bday‘𝐴)) ∣ 𝑥 <s 𝐴}
Theorem	rightval 28242*	The value of the right options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ (R‘𝐴) = {𝑥 ∈ (O‘(bday‘𝐴)) ∣ 𝐴 <s 𝑥}
Theorem	elleft 28243	Membership in the left set of a surreal. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ (L‘𝐵) ↔ (𝐴 ∈ (O‘(bday‘𝐵)) ∧ 𝐴 <s 𝐵))
Theorem	elright 28244	Membership in the right set of a surreal. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ (R‘𝐵) ↔ (𝐴 ∈ (O‘(bday‘𝐵)) ∧ 𝐵 <s 𝐴))
Theorem	leftlt 28245	A member of a surreal's left set is less than it. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ (L‘𝐵) → 𝐴 <s 𝐵)
Theorem	rightgt 28246	A member of a surreal's right set is greater than it. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ (R‘𝐵) → 𝐵 <s 𝐴)
Theorem	leftf 28247	The functionality of the left options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ L:No⟶𝒫 No
Theorem	rightf 28248	The functionality of the right options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ R:No⟶𝒫 No
Theorem	elmade 28249*	Membership in the made function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ (𝐴 ∈ On → (𝑋 ∈ (M‘𝐴) ↔ ∃𝑙 ∈ 𝒫 ∪ (M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ (M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑋)))
Theorem	elmade2 28250*	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 28251*	Membership in an old set. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (𝐴 ∈ On → (𝑋 ∈ (O‘𝐴) ↔ ∃𝑏 ∈ 𝐴 𝑋 ∈ (M‘𝑏)))
Theorem	sltsleft 28252	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 28253	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 28254	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 28255	The only surreal made on day ∅ is 0s. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (M‘∅) = { 0s }
Theorem	new0 28256	The only surreal new on day ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (N‘∅) = { 0s }
Theorem	old1 28257	The only surreal older than 1o is 0s. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ (O‘1o) = { 0s }
Theorem	madess 28258	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 28259	The older-than set is a subset of the made set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ (O‘𝐴) ⊆ (M‘𝐴)
Theorem	oldmade 28260	An element of an old set is an element of a made set. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ (O‘𝐵) → 𝐴 ∈ (M‘𝐵))
Theorem	oldmaded 28261	An element of an old set is an element of a made set. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ (O‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (M‘𝐵))
Theorem	oldss 28262	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‘𝐵))
Theorem	leftssold 28263	The left options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ (L‘𝑋) ⊆ (O‘(bday‘𝑋))
Theorem	rightssold 28264	The right options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ (R‘𝑋) ⊆ (O‘(bday‘𝑋))
Theorem	leftssno 28265	The left set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ (L‘𝐴) ⊆ No
Theorem	rightssno 28266	The right set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ (R‘𝐴) ⊆ No
Theorem	leftold 28267	An element of a left set is an element of the old set. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ (L‘𝐵) → 𝐴 ∈ (O‘(bday‘𝐵)))
Theorem	rightold 28268	An element of a right set is an element of the old set. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ (R‘𝐵) → 𝐴 ∈ (O‘(bday‘𝐵)))
Theorem	leftno 28269	An element of a left set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ (L‘𝐵) → 𝐴 ∈ No)
Theorem	rightno 28270	An element of a right set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ (R‘𝐵) → 𝐴 ∈ No)
Theorem	leftoldd 28271	An element of a left set is an element of the old set. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ (L‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (O‘(bday‘𝐵)))
Theorem	leftnod 28272	An element of a left set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ (L‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ No)
Theorem	rightoldd 28273	An element of a right set is an element of the old set. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ (R‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (O‘(bday‘𝐵)))
Theorem	rightnod 28274	An element of a right set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ (R‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ No)
Theorem	madecut 28275	Given a section that is a subset of an old set, the cut is a member of the made set. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (((𝐴 ∈ On ∧ 𝐿 <<s 𝑅) ∧ (𝐿 ⊆ (O‘𝐴) ∧ 𝑅 ⊆ (O‘𝐴))) → (𝐿 |s 𝑅) ∈ (M‘𝐴))
Theorem	madeun 28276	The made set is the union of the old set and the new set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ (M‘𝐴) = ((O‘𝐴) ∪ (N‘𝐴))
Theorem	madeoldsuc 28277	The made set is the old set of its successor. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝐴 ∈ On → (M‘𝐴) = (O‘suc 𝐴))
Theorem	oldsuc 28278	The value of the old set at a successor. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝐴 ∈ On → (O‘suc 𝐴) = ((O‘𝐴) ∪ (N‘𝐴)))
Theorem	oldlim 28279	The value of the old set at a limit ordinal. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ((Lim 𝐴 ∧ 𝐴 ∈ 𝑉) → (O‘𝐴) = ∪ (O “ 𝐴))
Theorem	madebdayim 28280	If a surreal is a member of a made set, its birthday is less than or equal to the level. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ (𝑋 ∈ (M‘𝐴) → (bday‘𝑋) ⊆ 𝐴)
Theorem	oldbdayim 28281	If 𝑋 is in the old set for 𝐴, then the birthday of 𝑋 is less than 𝐴. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ (𝑋 ∈ (O‘𝐴) → (bday‘𝑋) ∈ 𝐴)
Theorem	oldirr 28282	No surreal is a member of its birthday's old set. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ ¬ 𝑋 ∈ (O‘(bday‘𝑋))
Theorem	leftirr 28283	No surreal is a member of its left set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ¬ 𝑋 ∈ (L‘𝑋)
Theorem	rightirr 28284	No surreal is a member of its right set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ¬ 𝑋 ∈ (R‘𝑋)
Theorem	left0s 28285	The left set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ (L‘ 0s ) = ∅
Theorem	right0s 28286	The right set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ (R‘ 0s ) = ∅
Theorem	left1s 28287	The left set of 1s is the singleton of 0s. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ (L‘ 1s ) = { 0s }
Theorem	right1s 28288	The right set of 1s is empty . (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ (R‘ 1s ) = ∅
Theorem	lrold 28289	The union of the left and right options of a surreal make its old set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ((L‘𝐴) ∪ (R‘𝐴)) = (O‘(bday‘𝐴))
Theorem	madebdaylemold 28290*	Lemma for madebday 28292. If the inductive hypothesis of madebday 28292 is satisfied, the converse of oldbdayim 28281 holds. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ ∀𝑏 ∈ 𝐴 ∀𝑦 ∈ No ((bday‘𝑦) ⊆ 𝑏 → 𝑦 ∈ (M‘𝑏)) ∧ 𝑋 ∈ No) → ((bday‘𝑋) ∈ 𝐴 → 𝑋 ∈ (O‘𝐴)))
Theorem	madebdaylemlrcut 28291*	Lemma for madebday 28292. If the inductive hypothesis of madebday 28292 is satisfied up to the birthday of 𝑋, then the conclusion of lrcut 28296 holds. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ((∀𝑏 ∈ (bday‘𝑋)∀𝑦 ∈ No ((bday‘𝑦) ⊆ 𝑏 → 𝑦 ∈ (M‘𝑏)) ∧ 𝑋 ∈ No) → ((L‘𝑋) |s (R‘𝑋)) = 𝑋)
Theorem	madebday 28292	A surreal is part of the set made by ordinal 𝐴 iff its birthday is less than or equal to 𝐴. Remark in [Conway] p. 29. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ No) → (𝑋 ∈ (M‘𝐴) ↔ (bday‘𝑋) ⊆ 𝐴))
Theorem	oldbday 28293	A surreal is part of the set older than ordinal 𝐴 iff its birthday is less than 𝐴. Remark in [Conway] p. 29. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ No) → (𝑋 ∈ (O‘𝐴) ↔ (bday‘𝑋) ∈ 𝐴))
Theorem	newbday 28294	A surreal is an element of a new set iff its birthday is equal to that ordinal. Remark in [Conway] p. 29. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ No) → (𝑋 ∈ (N‘𝐴) ↔ (bday‘𝑋) = 𝐴))
Theorem	newbdayim 28295	One direction of the biconditional in newbday 28294. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝑋 ∈ (N‘𝐴) → (bday‘𝑋) = 𝐴)
Theorem	lrcut 28296	A surreal is equal to the cut of its left and right sets. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ (𝑋 ∈ No → ((L‘𝑋) |s (R‘𝑋)) = 𝑋)
Theorem	cutsfo 28297	The surreal cut function is onto. (Contributed by Scott Fenton, 23-Aug-2024.)
⊢ |s : <<s –onto→No
Theorem	ltsn0 28298	If 𝑋 is less than 𝑌, then either (L‘𝑌) or (R‘𝑋) is non-empty. (Contributed by Scott Fenton, 10-Dec-2024.)
⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑋 <s 𝑌) → ((L‘𝑌) ≠ ∅ ∨ (R‘𝑋) ≠ ∅))
Theorem	lruneq 28299	If two surreals share a birthday, then the union of their left and right sets are equal. (Contributed by Scott Fenton, 17-Sep-2024.)
⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ (bday‘𝑋) = (bday‘𝑌)) → ((L‘𝑋) ∪ (R‘𝑋)) = ((L‘𝑌) ∪ (R‘𝑌)))
Theorem	ltslpss 28300	If two surreals share a birthday, then 𝑋 <s 𝑌 iff the left set of 𝑋 is a proper subset of the left set of 𝑌. (Contributed by Scott Fenton, 17-Sep-2024.)
⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ (bday‘𝑋) = (bday‘𝑌)) → (𝑋 <s 𝑌 ↔ (L‘𝑋) ⊊ (L‘𝑌)))