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
15.3.3  Cuts and Options
Syntax	cmade 28201	Declare the symbol for the made by function.
class M
Syntax	cold 28202	Declare the symbol for the older than function.
class O
Syntax	cnew 28203	Declare the symbol for the new on function.
class N
Syntax	cleft 28204	Declare the symbol for the left option function.
class L
Syntax	cright 28205	Declare the symbol for the right option function.
class R
Definition	df-made 28206	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 28207	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 28208	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 28209*	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 28210*	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 28211	The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))))
Theorem	madeval2 28212*	Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ (𝐴 ∈ On → ( M ‘𝐴) = {𝑥 ∈ No ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)})
Theorem	oldval 28213	The value of the old options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ (𝐴 ∈ On → ( O ‘𝐴) = ∪ ( M “ 𝐴))
Theorem	newval 28214	The value of the new options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( N ‘𝐴) = (( M ‘𝐴) ∖ ( O ‘𝐴))
Theorem	madef 28215	The made function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ M :On⟶𝒫 No
Theorem	oldf 28216	The older function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ O :On⟶𝒫 No
Theorem	newf 28217	The new function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ N :On⟶𝒫 No
Theorem	old0 28218	No surreal is older than ∅. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ ( O ‘∅) = ∅
Theorem	madessno 28219	Made sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( M ‘𝐴) ⊆ No
Theorem	oldssno 28220	Old sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( O ‘𝐴) ⊆ No
Theorem	newssno 28221	New sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( N ‘𝐴) ⊆ No
Theorem	madeno 28222	An element of a made set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ ( M ‘𝐵) → 𝐴 ∈ No )
Theorem	oldno 28223	An element of an old set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ ( O ‘𝐵) → 𝐴 ∈ No )
Theorem	newno 28224	An element of a new set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ ( N ‘𝐵) → 𝐴 ∈ No )
Theorem	madenod 28225	An element of a made set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ ( M ‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	oldnod 28226	An element of an old set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ ( O ‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	newnod 28227	An element of a new set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ ( N ‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	leftval 28228*	The value of the left options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( L ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝑥 <s 𝐴}
Theorem	rightval 28229*	The value of the right options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( R ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝐴 <s 𝑥}
Theorem	elleft 28230	Membership in the left set of a surreal. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( L ‘𝐵) ↔ (𝐴 ∈ ( O ‘( bday ‘𝐵)) ∧ 𝐴 <s 𝐵))
Theorem	elright 28231	Membership in the right set of a surreal. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( R ‘𝐵) ↔ (𝐴 ∈ ( O ‘( bday ‘𝐵)) ∧ 𝐵 <s 𝐴))
Theorem	leftlt 28232	A member of a surreal's left set is less than it. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( L ‘𝐵) → 𝐴 <s 𝐵)
Theorem	rightgt 28233	A member of a surreal's right set is greater than it. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( R ‘𝐵) → 𝐵 <s 𝐴)
Theorem	leftf 28234	The functionality of the left options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ L : No ⟶𝒫 No
Theorem	rightf 28235	The functionality of the right options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ R : No ⟶𝒫 No
Theorem	elmade 28236*	Membership in the made function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ (𝐴 ∈ On → (𝑋 ∈ ( M ‘𝐴) ↔ ∃𝑙 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑋)))
Theorem	elmade2 28237*	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 28238*	Membership in an old set. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (𝐴 ∈ On → (𝑋 ∈ ( O ‘𝐴) ↔ ∃𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘𝑏)))
Theorem	sltsleft 28239	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 28240	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 28241	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 28242	The only surreal made on day ∅ is 0s. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ ( M ‘∅) = { 0s }
Theorem	new0 28243	The only surreal new on day ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ( N ‘∅) = { 0s }
Theorem	old1 28244	The only surreal older than 1o is 0s. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ( O ‘1o) = { 0s }
Theorem	madess 28245	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 28246	The older-than set is a subset of the made set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( O ‘𝐴) ⊆ ( M ‘𝐴)
Theorem	oldmade 28247	An element of an old set is an element of a made set. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ ( O ‘𝐵) → 𝐴 ∈ ( M ‘𝐵))
Theorem	oldmaded 28248	An element of an old set is an element of a made set. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ ( O ‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ ( M ‘𝐵))
Theorem	oldss 28249	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 28250	The left options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
Theorem	rightssold 28251	The right options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
Theorem	leftssno 28252	The left set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( L ‘𝐴) ⊆ No
Theorem	rightssno 28253	The right set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( R ‘𝐴) ⊆ No
Theorem	leftold 28254	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 28255	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 28256	An element of a left set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ ( L ‘𝐵) → 𝐴 ∈ No )
Theorem	rightno 28257	An element of a right set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ ( R ‘𝐵) → 𝐴 ∈ No )
Theorem	leftoldd 28258	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 28259	An element of a left set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ ( L ‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	rightoldd 28260	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 28261	An element of a right set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ ( R ‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	madecut 28262	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 28263	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 28264	The made set is the old set of its successor. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( O ‘suc 𝐴))
Theorem	oldsuc 28265	The value of the old set at a successor. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝐴 ∈ On → ( O ‘suc 𝐴) = (( O ‘𝐴) ∪ ( N ‘𝐴)))
Theorem	oldlim 28266	The value of the old set at a limit ordinal. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ((Lim 𝐴 ∧ 𝐴 ∈ 𝑉) → ( O ‘𝐴) = ∪ ( O “ 𝐴))
Theorem	madebdayim 28267	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 28268	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 28269	No surreal is a member of its birthday's old set. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ ¬ 𝑋 ∈ ( O ‘( bday ‘𝑋))
Theorem	leftirr 28270	No surreal is a member of its left set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ¬ 𝑋 ∈ ( L ‘𝑋)
Theorem	rightirr 28271	No surreal is a member of its right set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ¬ 𝑋 ∈ ( R ‘𝑋)
Theorem	left0s 28272	The left set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ( L ‘ 0s ) = ∅
Theorem	right0s 28273	The right set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ( R ‘ 0s ) = ∅
Theorem	left1s 28274	The left set of 1s is the singleton of 0s. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ( L ‘ 1s ) = { 0s }
Theorem	right1s 28275	The right set of 1s is empty . (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ( R ‘ 1s ) = ∅
Theorem	lrold 28276	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 28277*	Lemma for madebday 28279. If the inductive hypothesis of madebday 28279 is satisfied, the converse of oldbdayim 28268 holds. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ ∀𝑏 ∈ 𝐴 ∀𝑦 ∈ No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No ) → (( bday ‘𝑋) ∈ 𝐴 → 𝑋 ∈ ( O ‘𝐴)))
Theorem	madebdaylemlrcut 28278*	Lemma for madebday 28279. If the inductive hypothesis of madebday 28279 is satisfied up to the birthday of 𝑋, then the conclusion of lrcut 28283 holds. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ((∀𝑏 ∈ ( bday ‘𝑋)∀𝑦 ∈ No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No ) → (( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋)
Theorem	madebday 28279	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 28280	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 28281	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 28282	One direction of the biconditional in newbday 28281. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝑋 ∈ ( N ‘𝐴) → ( bday ‘𝑋) = 𝐴)
Theorem	lrcut 28283	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 28284	The surreal cut function is onto. (Contributed by Scott Fenton, 23-Aug-2024.)
⊢ |s : <<s –onto→ No
Theorem	ltsn0 28285	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 28286	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 28287	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	leslss 28288	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 28289	Zero is in the old set of any nonzero number. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐴 ≠ 0s )    ⇒   ⊢ (𝜑 → 0s ∈ ( O ‘( bday ‘𝐴)))
Theorem	0elleft 28290	Zero is in the left set of any positive number. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐴)    ⇒   ⊢ (𝜑 → 0s ∈ ( L ‘𝐴))
Theorem	0elright 28291	Zero is in the right set of any negative number. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 0s )    ⇒   ⊢ (𝜑 → 0s ∈ ( R ‘𝐴))
Theorem	madefi 28292	The made set of an ordinal natural is finite. (Contributed by Scott Fenton, 20-Aug-2025.) (Proof shortened by Vincent Gonzalez, 19-Aug-2026.)
⊢ (𝐴 ∈ ω → ( M ‘𝐴) ∈ Fin)
Theorem	oldfi 28293	The old set of an ordinal natural is finite. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ (𝐴 ∈ ω → ( O ‘𝐴) ∈ Fin)
Theorem	bdayiun 28294*	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 28295*	A condition for bounding a birthday above. (Contributed by Scott Fenton, 22-Nov-2025.)
⊢ ((𝑋 ∈ No ∧ Ord 𝑂) → (( bday ‘𝑋) ⊆ 𝑂 ↔ ∀𝑦 ∈ ( O ‘( bday ‘𝑋))( bday ‘𝑦) ∈ 𝑂))
Theorem	sltsbday 28296	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	cofslts 28297*	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 𝐶)
Theorem	coinitslts 28298*	If 𝐵 is coinitial with 𝐶 and 𝐴 precedes 𝐶, then 𝐴 precedes 𝐵. (Contributed by Scott Fenton, 24-Sep-2024.)
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s 𝐵)
Theorem	cofcut1 28299*	If 𝐶 is cofinal with 𝐴 and 𝐷 is coinitial with 𝐵 and the cut of 𝐴 and 𝐵 lies between 𝐶 and 𝐷, then the cut of 𝐶 and 𝐷 is equal to the cut of 𝐴 and 𝐵. Theorem 2.6 of [Gonshor] p. 10. (Contributed by Scott Fenton, 25-Sep-2024.)
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐴 |s 𝐵) = (𝐶 |s 𝐷))
Theorem	cofcut1d 28300*	If 𝐶 is cofinal with 𝐴 and 𝐷 is coinitial with 𝐵 and the cut of 𝐴 and 𝐵 lies between 𝐶 and 𝐷, then the cut of 𝐶 and 𝐷 is equal to the cut of 𝐴 and 𝐵. Theorem 2.6 of [Gonshor] p. 10. (Contributed by Scott Fenton, 23-Jan-2025.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧)    &   ⊢ (𝜑 → 𝐶 <<s {(𝐴 |s 𝐵)})    &   ⊢ (𝜑 → {(𝐴 |s 𝐵)} <<s 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = (𝐶 |s 𝐷))