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	ssltdisj 27801	If 𝐴 preceeds 𝐵, then 𝐴 and 𝐵 are disjoint. (Contributed by Scott Fenton, 18-Sep-2024.)
⊢ (𝐴 <<s 𝐵 → (𝐴 ∩ 𝐵) = ∅)
Theorem	eqscut3 27802*	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 27803	Declare the class syntax for surreal zero.
class 0s
Syntax	c1s 27804	Declare the class syntax for surreal one.
class 1s
Definition	df-0s 27805	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 27806	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 27807	Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 0s ∈ No
Theorem	1sno 27808	Surreal one is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 1s ∈ No
Theorem	bday0s 27809	Calculate the birthday of surreal zero. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ ( bday ‘ 0s ) = ∅
Theorem	0slt1s 27810	Surreal zero is less than surreal one. Theorem from [Conway] p. 7. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ 0s <s 1s
Theorem	bday0b 27811	The only surreal with birthday ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝑋 ∈ No → (( bday ‘𝑋) = ∅ ↔ 𝑋 = 0s ))
Theorem	bday1s 27812	The birthday of surreal one is ordinal one. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ( bday ‘ 1s ) = 1o
Theorem	cuteq0 27813	Condition for a surreal cut to equal zero. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝜑 → 𝐴 <<s { 0s })    &   ⊢ (𝜑 → { 0s } <<s 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = 0s )
Theorem	cutneg 27814	The simplest number greater than a negative number is zero. (Contributed by Scott Fenton, 4-Sep-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 0s )    ⇒   ⊢ (𝜑 → ({𝐴} |s ∅) = 0s )
Theorem	cuteq1 27815	Condition for a surreal cut to equal one. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (𝜑 → 0s ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 <<s { 1s })    &   ⊢ (𝜑 → { 1s } <<s 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = 1s )
Theorem	sgt0ne0 27816	A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ ( 0s <s 𝐴 → 𝐴 ≠ 0s )
Theorem	sgt0ne0d 27817	A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (𝜑 → 0s <s 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0s )
Theorem	1sne0s 27818	Surreal zero does not equal surreal one. (Contributed by Scott Fenton, 5-Sep-2025.)
⊢ 1s ≠ 0s
Theorem	rightpos 27819*	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 27820	Declare the symbol for the made by function.
class M
Syntax	cold 27821	Declare the symbol for the older than function.
class O
Syntax	cnew 27822	Declare the symbol for the new on function.
class N
Syntax	cleft 27823	Declare the symbol for the left option function.
class L
Syntax	cright 27824	Declare the symbol for the right option function.
class R
Definition	df-made 27825	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 27826	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 27827	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 27828*	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 27829*	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 27830	The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))))
Theorem	madeval2 27831*	Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ (𝐴 ∈ On → ( M ‘𝐴) = {𝑥 ∈ No ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)})
Theorem	oldval 27832	The value of the old options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ (𝐴 ∈ On → ( O ‘𝐴) = ∪ ( M “ 𝐴))
Theorem	newval 27833	The value of the new options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( N ‘𝐴) = (( M ‘𝐴) ∖ ( O ‘𝐴))
Theorem	madef 27834	The made function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ M :On⟶𝒫 No
Theorem	oldf 27835	The older function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ O :On⟶𝒫 No
Theorem	newf 27836	The new function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ N :On⟶𝒫 No
Theorem	old0 27837	No surreal is older than ∅. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ ( O ‘∅) = ∅
Theorem	madessno 27838	Made sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( M ‘𝐴) ⊆ No
Theorem	oldssno 27839	Old sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( O ‘𝐴) ⊆ No
Theorem	newssno 27840	New sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( N ‘𝐴) ⊆ No
Theorem	leftval 27841*	The value of the left options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( L ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝑥 <s 𝐴}
Theorem	rightval 27842*	The value of the right options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( R ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝐴 <s 𝑥}
Theorem	elleft 27843	Membership in the left set of a surreal. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( L ‘𝐵) ↔ (𝐴 ∈ ( O ‘( bday ‘𝐵)) ∧ 𝐴 <s 𝐵))
Theorem	elright 27844	Membership in the right set of a surreal. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( R ‘𝐵) ↔ (𝐴 ∈ ( O ‘( bday ‘𝐵)) ∧ 𝐵 <s 𝐴))
Theorem	leftlt 27845	A member of a surreal's left set is less than it. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( L ‘𝐵) → 𝐴 <s 𝐵)
Theorem	rightgt 27846	A member of a surreal's right set is greater than it. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( R ‘𝐵) → 𝐵 <s 𝐴)
Theorem	leftf 27847	The functionality of the left options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ L : No ⟶𝒫 No
Theorem	rightf 27848	The functionality of the right options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ R : No ⟶𝒫 No
Theorem	elmade 27849*	Membership in the made function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ (𝐴 ∈ On → (𝑋 ∈ ( M ‘𝐴) ↔ ∃𝑙 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑋)))
Theorem	elmade2 27850*	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 27851*	Membership in an old set. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (𝐴 ∈ On → (𝑋 ∈ ( O ‘𝐴) ↔ ∃𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘𝑏)))
Theorem	ssltleft 27852	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 27853	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 27854	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 27855	The only surreal made on day ∅ is 0s. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ ( M ‘∅) = { 0s }
Theorem	new0 27856	The only surreal new on day ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ( N ‘∅) = { 0s }
Theorem	old1 27857	The only surreal older than 1o is 0s. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ( O ‘1o) = { 0s }
Theorem	madess 27858	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 27859	The older-than set is a subset of the made set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( O ‘𝐴) ⊆ ( M ‘𝐴)
Theorem	oldss 27860	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 27861	The left options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
Theorem	rightssold 27862	The right options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
Theorem	leftssno 27863	The left set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( L ‘𝐴) ⊆ No
Theorem	rightssno 27864	The right set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( R ‘𝐴) ⊆ No
Theorem	madecut 27865	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 27866	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 27867	The made set is the old set of its successor. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( O ‘suc 𝐴))
Theorem	oldsuc 27868	The value of the old set at a successor. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝐴 ∈ On → ( O ‘suc 𝐴) = (( O ‘𝐴) ∪ ( N ‘𝐴)))
Theorem	oldlim 27869	The value of the old set at a limit ordinal. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ((Lim 𝐴 ∧ 𝐴 ∈ 𝑉) → ( O ‘𝐴) = ∪ ( O “ 𝐴))
Theorem	madebdayim 27870	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 27871	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 27872	No surreal is a member of its birthday's old set. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ ¬ 𝑋 ∈ ( O ‘( bday ‘𝑋))
Theorem	leftirr 27873	No surreal is a member of its left set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ¬ 𝑋 ∈ ( L ‘𝑋)
Theorem	rightirr 27874	No surreal is a member of its right set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ¬ 𝑋 ∈ ( R ‘𝑋)
Theorem	left0s 27875	The left set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ( L ‘ 0s ) = ∅
Theorem	right0s 27876	The right set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ( R ‘ 0s ) = ∅
Theorem	left1s 27877	The left set of 1s is the singleton of 0s. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ( L ‘ 1s ) = { 0s }
Theorem	right1s 27878	The right set of 1s is empty . (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ( R ‘ 1s ) = ∅
Theorem	lrold 27879	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 27880*	Lemma for madebday 27882. If the inductive hypothesis of madebday 27882 is satisfied, the converse of oldbdayim 27871 holds. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ ∀𝑏 ∈ 𝐴 ∀𝑦 ∈ No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No ) → (( bday ‘𝑋) ∈ 𝐴 → 𝑋 ∈ ( O ‘𝐴)))
Theorem	madebdaylemlrcut 27881*	Lemma for madebday 27882. If the inductive hypothesis of madebday 27882 is satisfied up to the birthday of 𝑋, then the conclusion of lrcut 27886 holds. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ((∀𝑏 ∈ ( bday ‘𝑋)∀𝑦 ∈ No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No ) → (( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋)
Theorem	madebday 27882	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 27883	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 27884	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 27885	One direction of the biconditional in newbday 27884. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝑋 ∈ ( N ‘𝐴) → ( bday ‘𝑋) = 𝐴)
Theorem	lrcut 27886	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	scutfo 27887	The surreal cut function is onto. (Contributed by Scott Fenton, 23-Aug-2024.)
⊢ |s : <<s –onto→ No
Theorem	sltn0 27888	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 27889	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	sltlpss 27890	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 ‘𝑌)))
Theorem	slelss 27891	If two surreals 𝐴 and 𝐵 share a birthday, then 𝐴 ≤s 𝐵 if and only if the left set of 𝐴 is a non-strict subset of the left set of 𝐵. (Contributed by Scott Fenton, 21-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( bday ‘𝐴) = ( bday ‘𝐵)) → (𝐴 ≤s 𝐵 ↔ ( L ‘𝐴) ⊆ ( L ‘𝐵)))
Theorem	0elold 27892	Zero is in the old set of any non-zero number. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐴 ≠ 0s )    ⇒   ⊢ (𝜑 → 0s ∈ ( O ‘( bday ‘𝐴)))
Theorem	0elleft 27893	Zero is in the left set of any positive number. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐴)    ⇒   ⊢ (𝜑 → 0s ∈ ( L ‘𝐴))
Theorem	0elright 27894	Zero is in the right set of any negative number. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 0s )    ⇒   ⊢ (𝜑 → 0s ∈ ( R ‘𝐴))
Theorem	madefi 27895	The made set of an ordinal natural is finite. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ (𝐴 ∈ ω → ( M ‘𝐴) ∈ Fin)
Theorem	oldfi 27896	The old set of an ordinal natural is finite. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ (𝐴 ∈ ω → ( O ‘𝐴) ∈ Fin)
Theorem	bdayiun 27897*	The birthday of a surreal is the least upper bound of the successors of the birthdays of its options. This is the definition of the birthday of a combinatorial game in the Lean Combinatorial Game Theory library at https://github.com/vihdzp/combinatorial-games. (Contributed by Scott Fenton, 22-Nov-2025.)
⊢ (𝐴 ∈ No → ( bday ‘𝐴) = ∪ 𝑥 ∈ ( O ‘( bday ‘𝐴))suc ( bday ‘𝑥))
Theorem	bdayle 27898*	A condition for bounding a birthday above. (Contributed by Scott Fenton, 22-Nov-2025.)
⊢ ((𝑋 ∈ No ∧ Ord 𝑂) → (( bday ‘𝑋) ⊆ 𝑂 ↔ ∀𝑦 ∈ ( O ‘( bday ‘𝑋))( bday ‘𝑦) ∈ 𝑂))
Theorem	ssltbday 27899	Birthday comparison rule for surreals. (Contributed by Scott Fenton, 23-Feb-2026.)
⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅))    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐿 <<s {𝐵})    &   ⊢ (𝜑 → {𝐵} <<s 𝑅)    ⇒   ⊢ (𝜑 → ( bday ‘𝐴) ⊆ ( bday ‘𝐵))
15.3.4  Cofinality and coinitiality
Theorem	cofsslt 27900*	If every element of 𝐴 is bounded above by some element of 𝐵 and 𝐵 precedes 𝐶, then 𝐴 precedes 𝐶. Note - we will often use the term "cofinal" to denote that every element of 𝐴 is bounded above by some element of 𝐵. Similarly, we will use the term "coinitial" to denote that every element of 𝐴 is bounded below by some element of 𝐵. (Contributed by Scott Fenton, 24-Sep-2024.)
⊢ ((𝐴 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶) → 𝐴 <<s 𝐶)