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
Definition	df-left 27801*	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 27802*	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 27803	The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))))
Theorem	madeval2 27804*	Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ (𝐴 ∈ On → ( M ‘𝐴) = {𝑥 ∈ No ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)})
Theorem	oldval 27805	The value of the old options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ (𝐴 ∈ On → ( O ‘𝐴) = ∪ ( M “ 𝐴))
Theorem	newval 27806	The value of the new options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( N ‘𝐴) = (( M ‘𝐴) ∖ ( O ‘𝐴))
Theorem	madef 27807	The made function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ M :On⟶𝒫 No
Theorem	oldf 27808	The older function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ O :On⟶𝒫 No
Theorem	newf 27809	The new function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ N :On⟶𝒫 No
Theorem	old0 27810	No surreal is older than ∅. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ ( O ‘∅) = ∅
Theorem	madessno 27811	Made sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( M ‘𝐴) ⊆ No
Theorem	oldssno 27812	Old sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( O ‘𝐴) ⊆ No
Theorem	newssno 27813	New sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( N ‘𝐴) ⊆ No
Theorem	leftval 27814*	The value of the left options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( L ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝑥 <s 𝐴}
Theorem	rightval 27815*	The value of the right options function. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( R ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝐴 <s 𝑥}
Theorem	elleft 27816	Membership in the left set of a surreal. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( L ‘𝐵) ↔ (𝐴 ∈ ( O ‘( bday ‘𝐵)) ∧ 𝐴 <s 𝐵))
Theorem	elright 27817	Membership in the right set of a surreal. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( R ‘𝐵) ↔ (𝐴 ∈ ( O ‘( bday ‘𝐵)) ∧ 𝐵 <s 𝐴))
Theorem	leftlt 27818	A member of a surreal's left set is less than it. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( L ‘𝐵) → 𝐴 <s 𝐵)
Theorem	rightgt 27819	A member of a surreal's right set is greater than it. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ( R ‘𝐵) → 𝐵 <s 𝐴)
Theorem	leftf 27820	The functionality of the left options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ L : No ⟶𝒫 No
Theorem	rightf 27821	The functionality of the right options function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ R : No ⟶𝒫 No
Theorem	elmade 27822*	Membership in the made function. (Contributed by Scott Fenton, 6-Aug-2024.)
⊢ (𝐴 ∈ On → (𝑋 ∈ ( M ‘𝐴) ↔ ∃𝑙 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑋)))
Theorem	elmade2 27823*	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 27824*	Membership in an old set. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (𝐴 ∈ On → (𝑋 ∈ ( O ‘𝐴) ↔ ∃𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘𝑏)))
Theorem	ssltleft 27825	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 27826	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 27827	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 27828	The only surreal made on day ∅ is 0s. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ ( M ‘∅) = { 0s }
Theorem	new0 27829	The only surreal new on day ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ( N ‘∅) = { 0s }
Theorem	old1 27830	The only surreal older than 1o is 0s. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ( O ‘1o) = { 0s }
Theorem	madess 27831	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 27832	The older-than set is a subset of the made set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( O ‘𝐴) ⊆ ( M ‘𝐴)
Theorem	oldss 27833	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 27834	The left options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
Theorem	rightssold 27835	The right options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
Theorem	leftssno 27836	The left set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( L ‘𝐴) ⊆ No
Theorem	rightssno 27837	The right set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( R ‘𝐴) ⊆ No
Theorem	madecut 27838	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 27839	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 27840	The made set is the old set of its successor. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( O ‘suc 𝐴))
Theorem	oldsuc 27841	The value of the old set at a successor. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝐴 ∈ On → ( O ‘suc 𝐴) = (( O ‘𝐴) ∪ ( N ‘𝐴)))
Theorem	oldlim 27842	The value of the old set at a limit ordinal. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ((Lim 𝐴 ∧ 𝐴 ∈ 𝑉) → ( O ‘𝐴) = ∪ ( O “ 𝐴))
Theorem	madebdayim 27843	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 27844	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 27845	No surreal is a member of its birthday's old set. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ ¬ 𝑋 ∈ ( O ‘( bday ‘𝑋))
Theorem	leftirr 27846	No surreal is a member of its left set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ¬ 𝑋 ∈ ( L ‘𝑋)
Theorem	rightirr 27847	No surreal is a member of its right set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ¬ 𝑋 ∈ ( R ‘𝑋)
Theorem	left0s 27848	The left set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ( L ‘ 0s ) = ∅
Theorem	right0s 27849	The right set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ( R ‘ 0s ) = ∅
Theorem	left1s 27850	The left set of 1s is the singleton of 0s. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ( L ‘ 1s ) = { 0s }
Theorem	right1s 27851	The right set of 1s is empty . (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ( R ‘ 1s ) = ∅
Theorem	lrold 27852	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 27853*	Lemma for madebday 27855. If the inductive hypothesis of madebday 27855 is satisfied, the converse of oldbdayim 27844 holds. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ ∀𝑏 ∈ 𝐴 ∀𝑦 ∈ No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No ) → (( bday ‘𝑋) ∈ 𝐴 → 𝑋 ∈ ( O ‘𝐴)))
Theorem	madebdaylemlrcut 27854*	Lemma for madebday 27855. If the inductive hypothesis of madebday 27855 is satisfied up to the birthday of 𝑋, then the conclusion of lrcut 27859 holds. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ((∀𝑏 ∈ ( bday ‘𝑋)∀𝑦 ∈ No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No ) → (( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋)
Theorem	madebday 27855	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 27856	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 27857	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 27858	One direction of the biconditional in newbday 27857. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝑋 ∈ ( N ‘𝐴) → ( bday ‘𝑋) = 𝐴)
Theorem	lrcut 27859	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 27860	The surreal cut function is onto. (Contributed by Scott Fenton, 23-Aug-2024.)
⊢ |s : <<s –onto→ No
Theorem	sltn0 27861	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 27862	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 27863	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 27864	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 27865	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 27866	Zero is in the left set of any positive number. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐴)    ⇒   ⊢ (𝜑 → 0s ∈ ( L ‘𝐴))
Theorem	0elright 27867	Zero is in the right set of any negative number. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 0s )    ⇒   ⊢ (𝜑 → 0s ∈ ( R ‘𝐴))
Theorem	madefi 27868	The made set of an ordinal natural is finite. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ (𝐴 ∈ ω → ( M ‘𝐴) ∈ Fin)
Theorem	oldfi 27869	The old set of an ordinal natural is finite. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ (𝐴 ∈ ω → ( O ‘𝐴) ∈ Fin)
Theorem	bdayiun 27870*	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 27871*	A condition for bounding a birthday above. (Contributed by Scott Fenton, 22-Nov-2025.)
⊢ ((𝑋 ∈ No ∧ Ord 𝑂) → (( bday ‘𝑋) ⊆ 𝑂 ↔ ∀𝑦 ∈ ( O ‘( bday ‘𝑋))( bday ‘𝑦) ∈ 𝑂))
15.3.4  Cofinality and coinitiality
Theorem	cofsslt 27872*	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	coinitsslt 27873*	If 𝐵 is coinitial with 𝐶 and 𝐴 precedes 𝐶, then 𝐴 precedes 𝐵. (Contributed by Scott Fenton, 24-Sep-2024.)
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s 𝐵)
Theorem	cofcut1 27874*	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 27875*	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 𝐷))
Theorem	cofcut2 27876*	If 𝐴 and 𝐶 are mutually cofinal and 𝐵 and 𝐷 are mutually coinitial, then the cut of 𝐴 and 𝐵 is equal to the cut of 𝐶 and 𝐷. Theorem 2.7 of [Gonshor] p. 10. (Contributed by Scott Fenton, 25-Sep-2024.)
⊢ (((𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (∀𝑡 ∈ 𝐶 ∃𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀𝑟 ∈ 𝐷 ∃𝑠 ∈ 𝐵 𝑠 ≤s 𝑟)) → (𝐴 |s 𝐵) = (𝐶 |s 𝐷))
Theorem	cofcut2d 27877*	If 𝐴 and 𝐶 are mutually cofinal and 𝐵 and 𝐷 are mutually coinitial, then the cut of 𝐴 and 𝐵 is equal to the cut of 𝐶 and 𝐷. Theorem 2.7 of [Gonshor] p. 10. (Contributed by Scott Fenton, 23-Jan-2025.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝒫 No )    &   ⊢ (𝜑 → 𝐷 ∈ 𝒫 No )    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧)    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝐶 ∃𝑢 ∈ 𝐴 𝑡 ≤s 𝑢)    &   ⊢ (𝜑 → ∀𝑟 ∈ 𝐷 ∃𝑠 ∈ 𝐵 𝑠 ≤s 𝑟)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = (𝐶 |s 𝐷))
Theorem	cofcutr 27878*	If 𝑋 is the cut of 𝐴 and 𝐵, then 𝐴 is cofinal with ( L ‘𝑋) and 𝐵 is coinitial with ( R ‘𝑋). Theorem 2.9 of [Gonshor] p. 12. (Contributed by Scott Fenton, 25-Sep-2024.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (∀𝑥 ∈ ( L ‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ ( R ‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧))
Theorem	cofcutr1d 27879*	If 𝑋 is the cut of 𝐴 and 𝐵, then 𝐴 is cofinal with ( L ‘𝑋). First half of theorem 2.9 of [Gonshor] p. 12. (Contributed by Scott Fenton, 23-Jan-2025.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ ( L ‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦)
Theorem	cofcutr2d 27880*	If 𝑋 is the cut of 𝐴 and 𝐵, then 𝐵 is coinitial with ( R ‘𝑋). Second half of theorem 2.9 of [Gonshor] p. 12. (Contributed by Scott Fenton, 25-Sep-2024.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵))    ⇒   ⊢ (𝜑 → ∀𝑧 ∈ ( R ‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧)
Theorem	cofcutrtime 27881*	If 𝑋 is the cut of 𝐴 and 𝐵 and all of 𝐴 and 𝐵 are older than 𝑋, then ( L ‘𝑋) is cofinal with 𝐴 and ( R ‘𝑋) is coinitial with 𝐵. Note: we will call a cut where all of the elements of the cut are older than the cut itself a "timely" cut. Part of Theorem 4.02(12) of [Alling] p. 125. (Contributed by Scott Fenton, 27-Sep-2024.)
⊢ (((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ( L ‘𝑋)𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ ( R ‘𝑋)𝑤 ≤s 𝑧))
Theorem	cofcutrtime1d 27882*	If 𝑋 is a timely cut of 𝐴 and 𝐵, then ( L ‘𝑋) is cofinal with 𝐴. (Contributed by Scott Fenton, 23-Jan-2025.)
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)))    &   ⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ( L ‘𝑋)𝑥 ≤s 𝑦)
Theorem	cofcutrtime2d 27883*	If 𝑋 is a timely cut of 𝐴 and 𝐵, then ( R ‘𝑋) is coinitial with 𝐵. (Contributed by Scott Fenton, 23-Jan-2025.)
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)))    &   ⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵))    ⇒   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ ( R ‘𝑋)𝑤 ≤s 𝑧)
Theorem	cofss 27884*	Cofinality for a subset. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ⊆ No )    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦)
Theorem	coiniss 27885*	Coinitiality for a subset. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ⊆ No )    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐴 𝑦 ≤s 𝑥)
Theorem	cutlt 27886*	Eliminating all elements below a given element of a cut does not affect the cut. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐿 <<s 𝑅)    &   ⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐿)    ⇒   ⊢ (𝜑 → 𝐴 = (({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) |s 𝑅))
Theorem	cutpos 27887*	Reduce the elements of a cut for a positive number. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = (({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) |s ( R ‘𝐴)))
Theorem	cutmax 27888*	If 𝐴 has a maximum, then the maximum may be used alone in the cut. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑦 ∈ 𝐴 𝑦 ≤s 𝑋)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = ({𝑋} |s 𝐵))
Theorem	cutmin 27889*	If 𝐵 has a minimum, then the minimum may be used alone in the cut. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 𝑋 ≤s 𝑦)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = (𝐴 |s {𝑋}))
15.4  Induction and recursion
15.4.1  Induction and recursion on one variable
Syntax	cnorec 27890	Declare the syntax for surreal recursion of one variable.
class norec (𝐹)
Definition	df-norec 27891*	Define the recursion generator for surreal functions of one variable. This generator creates a recursive function of surreals from their value on their left and right sets. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ norec (𝐹) = frecs({⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝐹)
Theorem	lrrecval 27892*	The next step in the development of the surreals is to establish induction and recursion across left and right sets. To that end, we are going to develop a relationship 𝑅 that is founded, partial, and set-like across the surreals. This first theorem just establishes the value of 𝑅. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}    ⇒   ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴𝑅𝐵 ↔ 𝐴 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))))
Theorem	lrrecval2 27893*	Next, we establish an alternate expression for 𝑅. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}    ⇒   ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴𝑅𝐵 ↔ ( bday ‘𝐴) ∈ ( bday ‘𝐵)))
Theorem	lrrecpo 27894*	Now, we establish that 𝑅 is a partial ordering on No . (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}    ⇒   ⊢ 𝑅 Po No
Theorem	lrrecse 27895*	Next, we show that 𝑅 is set-like over No . (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}    ⇒   ⊢ 𝑅 Se No
Theorem	lrrecfr 27896*	Now we show that 𝑅 is founded over No . (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}    ⇒   ⊢ 𝑅 Fr No
Theorem	lrrecpred 27897*	Finally, we calculate the value of the predecessor class over 𝑅. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}    ⇒   ⊢ (𝐴 ∈ No → Pred(𝑅, No , 𝐴) = (( L ‘𝐴) ∪ ( R ‘𝐴)))
Theorem	noinds 27898*	Induction principle for a single surreal. If a property passes from a surreal's left and right sets to the surreal itself, then it holds for all surreals. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 ∈ No → (∀𝑦 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))𝜓 → 𝜑))    ⇒   ⊢ (𝐴 ∈ No → 𝜒)
Theorem	norecfn 27899	Surreal recursion over one variable is a function over the surreals. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝐹 = norec (𝐺)    ⇒   ⊢ 𝐹 Fn No
Theorem	norecov 27900	Calculate the value of the surreal recursion operation. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝐹 = norec (𝐺)    ⇒   ⊢ (𝐴 ∈ No → (𝐹‘𝐴) = (𝐴𝐺(𝐹 ↾ (( L ‘𝐴) ∪ ( R ‘𝐴)))))