P. 287 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28601-28700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	precsexlem9 28601*	Lemma for surreal reciprocal. Show that the product of 𝐴 and a left element is less than one and the product of 𝐴 and a right element is greater than one. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 0s <s 𝐴)    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))    ⇒   ⊢ ((𝜑 ∧ 𝐼 ∈ ω) → (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐)))
Theorem	precsexlem10 28602*	Lemma for surreal reciprocal. Show that the union of the left sets is less than the union of the right sets. Note that this is the first theorem in the surreal numbers to require the axiom of infinity. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 0s <s 𝐴)    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))    ⇒   ⊢ (𝜑 → ∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω))
Theorem	precsexlem11 28603*	Lemma for surreal reciprocal. Show that the cut of the left and right sets is a multiplicative inverse for 𝐴. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 0s <s 𝐴)    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))    &   ⊢ 𝑌 = (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝑌) = 1s )
Theorem	precsex 28604*	Every positive surreal has a reciprocal. Theorem 10(iv) of [Conway] p. 21. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 0s <s 𝐴) → ∃𝑦 ∈ No (𝐴 ·s 𝑦) = 1s )
Theorem	recsex 28605*	A nonzero surreal has a reciprocal. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐴 ≠ 0s ) → ∃𝑥 ∈ No (𝐴 ·s 𝑥) = 1s )
Theorem	recsexd 28606*	A nonzero surreal has a reciprocal. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐴 ≠ 0s )    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐴 ·s 𝑥) = 1s )
Theorem	divmuls 28607	Relationship between surreal division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ (𝐶 ∈ No ∧ 𝐶 ≠ 0s )) → ((𝐴 /su 𝐶) = 𝐵 ↔ (𝐶 ·s 𝐵) = 𝐴))
Theorem	divmulsd 28608	Relationship between surreal division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐶) = 𝐵 ↔ (𝐶 ·s 𝐵) = 𝐴))
Theorem	divscl 28609	Surreal division closure law. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐵 ≠ 0s ) → (𝐴 /su 𝐵) ∈ No)
Theorem	divscld 28610	Surreal division closure law. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    ⇒   ⊢ (𝜑 → (𝐴 /su 𝐵) ∈ No)
Theorem	divscan2d 28611	A cancellation law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    ⇒   ⊢ (𝜑 → (𝐵 ·s (𝐴 /su 𝐵)) = 𝐴)
Theorem	divscan1d 28612	A cancellation law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐵) ·s 𝐵) = 𝐴)
Theorem	ltdivmulsd 28613	Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 0s <s 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐶 ·s 𝐵)))
Theorem	ltdivmuls2d 28614	Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 0s <s 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐵 ·s 𝐶)))
Theorem	ltmuldivsd 28615	Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 0s <s 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐵 /su 𝐶)))
Theorem	ltmuldivs2d 28616	Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 0s <s 𝐶)    ⇒   ⊢ (𝜑 → ((𝐶 ·s 𝐴) <s 𝐵 ↔ 𝐴 <s (𝐵 /su 𝐶)))
Theorem	divsassd 28617	An associative law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) /su 𝐶) = (𝐴 ·s (𝐵 /su 𝐶)))
Theorem	divmuldivsd 28618	Multiplication of two surreal ratios. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐷 ∈ No)    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    &   ⊢ (𝜑 → 𝐷 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐵) ·s (𝐶 /su 𝐷)) = ((𝐴 ·s 𝐶) /su (𝐵 ·s 𝐷)))
Theorem	divdivs1d 28619	Surreal division into a fraction. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐵) /su 𝐶) = (𝐴 /su (𝐵 ·s 𝐶)))
Theorem	divsrecd 28620	Relationship between surreal division and reciprocal. (Contributed by Scott Fenton, 13-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    ⇒   ⊢ (𝜑 → (𝐴 /su 𝐵) = (𝐴 ·s ( 1s /su 𝐵)))
Theorem	divsdird 28621	Distribution of surreal division over addition. (Contributed by Scott Fenton, 13-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) /su 𝐶) = ((𝐴 /su 𝐶) +s (𝐵 /su 𝐶)))
Theorem	divscan3d 28622	A cancellation law for surreal division. (Contributed by Scott Fenton, 13-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐵 ·s 𝐴) /su 𝐵) = 𝐴)
15.5.5  Absolute value
Syntax	cabss 28623	Declare the syntax for surreal absolute value.
class abss
Definition	df-abss 28624	Define the surreal absolute value function. See abssval 28625 for its value and absscl 28626 for its closure. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ abss = (𝑥 ∈ No ↦ if( 0s ≤s 𝑥, 𝑥, ( -s‘𝑥)))
Theorem	abssval 28625	The value of surreal absolute value. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → (abss‘𝐴) = if( 0s ≤s 𝐴, 𝐴, ( -s‘𝐴)))
Theorem	absscl 28626	Closure law for surreal absolute value. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → (abss‘𝐴) ∈ No)
Theorem	abssid 28627	The absolute value of a non-negative surreal is itself. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 0s ≤s 𝐴) → (abss‘𝐴) = 𝐴)
Theorem	abs0s 28628	The absolute value of surreal zero. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (abss‘ 0s ) = 0s
Theorem	abssnid 28629	For a negative surreal, its absolute value is its negation. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → (abss‘𝐴) = ( -s‘𝐴))
Theorem	absmuls 28630	Surreal absolute value distributes over multiplication. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (abss‘(𝐴 ·s 𝐵)) = ((abss‘𝐴) ·s (abss‘𝐵)))
Theorem	abssge0 28631	The absolute value of a surreal number is non-negative. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → 0s ≤s (abss‘𝐴))
Theorem	abssor 28632	The absolute value of a surreal is either that surreal or its negative. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → ((abss‘𝐴) = 𝐴 ∨ (abss‘𝐴) = ( -s‘𝐴)))
Theorem	absnegs 28633	Surreal absolute value of the negative. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → (abss‘( -s‘𝐴)) = (abss‘𝐴))
Theorem	leabss 28634	A surreal is less than or equal to its absolute value. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → 𝐴 ≤s (abss‘𝐴))
Theorem	abslts 28635	Surreal absolute value and less-than relation. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → ((abss‘𝐴) <s 𝐵 ↔ (( -s‘𝐵) <s 𝐴 ∧ 𝐴 <s 𝐵)))
Theorem	abssubs 28636	Swapping order of surreal subtraction doesn't change the absolute value. (Contributed by Scott Fenton, 29-Jan-2026.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (abss‘(𝐴 −s 𝐵)) = (abss‘(𝐵 −s 𝐴)))
15.6  Subsystems of surreals
15.6.1  Ordinal numbers
Syntax	cons 28637	Declare the syntax for surreal ordinals.
class Ons
Definition	df-ons 28638	Define the surreal ordinals. These are the maximum members of each generation of surreals. Variant of definition from [Conway] p. 27. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ Ons = {𝑥 ∈ No ∣ (R‘𝑥) = ∅}
Theorem	elons 28639	Membership in the class of surreal ordinals. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ (𝐴 ∈ Ons ↔ (𝐴 ∈ No ∧ (R‘𝐴) = ∅))
Theorem	onssno 28640	The surreal ordinals are a subclass of the surreals. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ Ons ⊆ No
Theorem	onno 28641	A surreal ordinal is a surreal. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ (𝐴 ∈ Ons → 𝐴 ∈ No)
Theorem	0ons 28642	Surreal zero is a surreal ordinal. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ 0s ∈ Ons
Theorem	1ons 28643	Surreal one is a surreal ordinal. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ 1s ∈ Ons
Theorem	elons2 28644*	A surreal is ordinal iff it is the cut of some set of surreals and the empty set. Definition from [Conway] p. 27. (Contributed by Scott Fenton, 19-Mar-2025.)
⊢ (𝐴 ∈ Ons ↔ ∃𝑎 ∈ 𝒫 No𝐴 = (𝑎 |s ∅))
Theorem	elons2d 28645	The cut of any set of surreals and the empty set is a surreal ordinal. (Contributed by Scott Fenton, 19-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ No)    &   ⊢ (𝜑 → 𝑋 = (𝐴 |s ∅))    ⇒   ⊢ (𝜑 → 𝑋 ∈ Ons)
Theorem	onleft 28646	The left set of a surreal ordinal is the same as its old set. (Contributed by Scott Fenton, 6-Nov-2025.)
⊢ (𝐴 ∈ Ons → (O‘(bday‘𝐴)) = (L‘𝐴))
Theorem	ltonold 28647*	The class of ordinals less than any surreal is a subset of that surreal's old set. (Contributed by Scott Fenton, 22-Mar-2025.)
⊢ (𝐴 ∈ No → {𝑥 ∈ Ons ∣ 𝑥 <s 𝐴} ⊆ (O‘(bday‘𝐴)))
Theorem	ltonsex 28648*	The class of ordinals less than any particular surreal is a set. Theorem 14 of [Conway] p. 27. (Contributed by Scott Fenton, 22-Mar-2025.)
⊢ (𝐴 ∈ No → {𝑥 ∈ Ons ∣ 𝑥 <s 𝐴} ∈ V)
Theorem	oncutleft 28649	A surreal ordinal is equal to the cut of its left set and the empty set. (Contributed by Scott Fenton, 29-Mar-2025.)
⊢ (𝐴 ∈ Ons → 𝐴 = ((L‘𝐴) |s ∅))
Theorem	oncutlt 28650*	A surreal ordinal is the simplest number greater than all previous surreal ordinals. Theorem 15 of [Conway] p. 28. (Contributed by Scott Fenton, 4-Nov-2025.)
⊢ (𝐴 ∈ Ons → 𝐴 = ({𝑥 ∈ Ons ∣ 𝑥 <s 𝐴} |s ∅))
Theorem	bday11on 28651	The birthday function is one-to-one over the surreal ordinals. (Contributed by Scott Fenton, 6-Nov-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ∧ (bday‘𝐴) = (bday‘𝐵)) → 𝐴 = 𝐵)
Theorem	onnolt 28652	If a surreal ordinal is less than a given surreal, then it is simpler. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵) → (bday‘𝐴) ∈ (bday‘𝐵))
Theorem	onlts 28653	Less-than is the same as birthday comparison over surreal ordinals. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → (𝐴 <s 𝐵 ↔ (bday‘𝐴) ∈ (bday‘𝐵)))
Theorem	onles 28654	Less-than or equal is the same as non-strict birthday comparison over surreal ordinals. (Contributed by Scott Fenton, 25-Feb-2026.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → (𝐴 ≤s 𝐵 ↔ (bday‘𝐴) ⊆ (bday‘𝐵)))
Theorem	onltsd 28655	Less-than is the same as birthday comparison over surreal ordinals. Deduction version. (Contributed by Scott Fenton, 25-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ Ons)    &   ⊢ (𝜑 → 𝐵 ∈ Ons)    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (bday‘𝐴) ∈ (bday‘𝐵)))
Theorem	onlesd 28656	Less-than or equal is the same as non-strict birthday comparison over surreal ordinals. Deduction version. (Contributed by Scott Fenton, 25-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ Ons)    &   ⊢ (𝜑 → 𝐵 ∈ Ons)    ⇒   ⊢ (𝜑 → (𝐴 ≤s 𝐵 ↔ (bday‘𝐴) ⊆ (bday‘𝐵)))
Theorem	oniso 28657	The birthday function restricted to the surreal ordinals forms an order-preserving isomorphism with the regular ordinals. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ (bday ↾ Ons) Isom <s , E (Ons, On)
Theorem	onswe 28658	Surreal less-than well-orders the surreal ordinals. Part of Theorem 15 of [Conway] p. 28. (Contributed by Scott Fenton, 6-Nov-2025.)
⊢ <s We Ons
Theorem	onsse 28659	Surreal less-than is set-like over the surreal ordinals. (Contributed by Scott Fenton, 6-Nov-2025.)
⊢ <s Se Ons
Theorem	onsis 28660*	Transfinite induction schema for surreal ordinals. (Contributed by Scott Fenton, 6-Nov-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 ∈ Ons → (∀𝑦 ∈ Ons (𝑦 <s 𝑥 → 𝜓) → 𝜑))    ⇒   ⊢ (𝐴 ∈ Ons → 𝜒)
Theorem	ons2ind 28661*	Double induction schema for surreal ordinals. (Contributed by Scott Fenton, 22-Feb-2026.)
⊢ (𝑥 = 𝑥𝑂 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑦𝑂 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑥𝑂 → (𝜃 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑦 = 𝐵 → (𝜏 ↔ 𝜂))    &   ⊢ ((𝑥 ∈ Ons ∧ 𝑦 ∈ Ons) → ((∀𝑥𝑂 ∈ Ons ∀𝑦𝑂 ∈ Ons ((𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦) → 𝜒) ∧ ∀𝑥𝑂 ∈ Ons (𝑥𝑂 <s 𝑥 → 𝜓) ∧ ∀𝑦𝑂 ∈ Ons (𝑦𝑂 <s 𝑦 → 𝜃)) → 𝜑))    ⇒   ⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → 𝜂)
Theorem	bdayons 28662*	The birthday of a surreal ordinal is the set of all previous ordinal birthdays. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ Ons → (bday‘𝐴) = (bday “ {𝑥 ∈ Ons ∣ 𝑥 <s 𝐴}))
Theorem	onaddscl 28663	The surreal ordinals are closed under addition. (Contributed by Scott Fenton, 22-Aug-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → (𝐴 +s 𝐵) ∈ Ons)
Theorem	onmulscl 28664	The surreal ordinals are closed under multiplication. (Contributed by Scott Fenton, 22-Aug-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → (𝐴 ·s 𝐵) ∈ Ons)
Theorem	addonbday 28665	The birthday of the sum of two ordinals is the natural sum of their birthdays. (Contributed by Scott Fenton, 22-Feb-2026.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → (bday‘(𝐴 +s 𝐵)) = ((bday‘𝐴) +no (bday‘𝐵)))
Theorem	peano2ons 28666	The successor of a surreal ordinal is a surreal ordinal. (Contributed by Scott Fenton, 22-Aug-2025.)
⊢ (𝐴 ∈ Ons → (𝐴 +s 1s ) ∈ Ons)
Theorem	onsbnd 28667	The surreals of a given birthday are bounded above by that ordinal. (Contributed by Scott Fenton, 22-Feb-2026.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ (M‘(bday‘𝐴))) → 𝐵 ≤s 𝐴)
Theorem	onsbnd2 28668	The surreals of a given birthday are bounded below by the negative of that ordinal. (Contributed by Scott Fenton, 22-Feb-2026.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ (M‘(bday‘𝐴))) → ( -s‘𝐴) ≤s 𝐵)
15.6.2  Surreal recursive sequences
Syntax	cseqs 28669	Extend class notation with the surreal recursive sequence builder.
class seqs𝑀( + , 𝐹)
Definition	df-seqs 28670*	Define a general-purpose sequence builder for surreal numbers. Compare df-seq 14145. Note that in the theorems we develop here, we do not require 𝑀 to be an integer. This is because there are infinite surreal numbers and we may want to start our sequence there. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ seqs𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑦 + (𝐹‘(𝑥 +s 1s )))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)
Theorem	seqsex 28671	Existence of the surreal sequence builder operation. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ seqs𝑀( + , 𝐹) ∈ V
Theorem	seqseq123d 28672	Equality deduction for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑀 = 𝑁)    &   ⊢ (𝜑 → + = 𝑄)    &   ⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → seqs𝑀( + , 𝐹) = seqs𝑁(𝑄, 𝐺))
Theorem	nfseqs 28673	Hypothesis builder for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ Ⅎ𝑥𝑀    &   ⊢ Ⅎ𝑥 +    &   ⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥seqs𝑀( + , 𝐹)
Theorem	seqsval 28674*	The value of the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑥(𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 +s 1s ))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩) ↾ ω))    ⇒   ⊢ (𝜑 → seqs𝑀( + , 𝐹) = ran 𝑅)
Theorem	noseqex 28675	The next several theorems develop the concept of a countable sequence of surreals. This set is denoted by 𝑍 here and is the analogue of the upper integer sets for surreal numbers. However, we do not require the starting point to be an integer so we can accommodate infinite numbers. This first theorem establishes that 𝑍 is a set. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    ⇒   ⊢ (𝜑 → 𝑍 ∈ V)
Theorem	noseq0 28676	The surreal 𝐴 is a member of the sequence starting at 𝐴. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑍)
Theorem	noseqp1 28677*	One plus an element of 𝑍 is an element of 𝑍. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (𝐵 +s 1s ) ∈ 𝑍)
Theorem	noseqind 28678*	Peano's inductive postulate for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 +s 1s ) ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑍 ⊆ 𝐵)
Theorem	noseqinds 28679*	Induction schema for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑦 = (𝑧 +s 1s ) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑍) → (𝜃 → 𝜏))    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 𝜂)
Theorem	noseqssno 28680	A surreal sequence is a subset of the surreals. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → 𝑍 ⊆ No)
Theorem	noseqno 28681	An element of a surreal sequence is a surreal. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐵 ∈ No)
Theorem	om2noseq0 28682	The mapping 𝐺 is a one-to-one mapping from ω onto a countable sequence of surreals that will be used to show the properties of seqs. This theorem shows the value of 𝐺 at ordinal zero. Compare the series of theorems starting at om2uz0i 14090. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    ⇒   ⊢ (𝜑 → (𝐺‘∅) = 𝐶)
Theorem	om2noseqsuc 28683*	The value of 𝐺 at a successor. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝐴 ∈ ω)    ⇒   ⊢ (𝜑 → (𝐺‘suc 𝐴) = ((𝐺‘𝐴) +s 1s ))
Theorem	om2noseqfo 28684	Function statement for 𝐺. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺:ω–onto→𝑍)
Theorem	om2noseqlt 28685*	Surreal less-than relation for 𝐺. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ∈ 𝐵 → (𝐺‘𝐴) <s (𝐺‘𝐵)))
Theorem	om2noseqlt2 28686*	The mapping 𝐺 preserves order. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ∈ 𝐵 ↔ (𝐺‘𝐴) <s (𝐺‘𝐵)))
Theorem	om2noseqf1o 28687*	𝐺 is a bijection. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺:ω–1-1-onto→𝑍)
Theorem	om2noseqiso 28688*	𝐺 is an isomorphism from the finite ordinals to a surreal sequence. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺 Isom E , <s (ω, 𝑍))
Theorem	om2noseqoi 28689*	An alternative definition of 𝐺 in terms of df-oi 9504. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺 = OrdIso( <s , 𝑍))
Theorem	om2noseqrdg 28690*	A helper lemma for the value of a recursive definition generator on a surreal sequence with characteristic function 𝐹(𝑥, 𝑦) and initial value 𝐴. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω))    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ ω) → (𝑅‘𝐵) = ⟨(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))⟩)
Theorem	noseqrdglem 28691*	A helper lemma for the value of a recursive defintion generator on surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω))    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → ⟨𝐵, (2nd ‘(𝑅‘(◡𝐺‘𝐵)))⟩ ∈ ran 𝑅)
Theorem	noseqrdgfn 28692*	The recursive definition generator on surreal sequences is a function. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω))    &   ⊢ (𝜑 → 𝑆 = ran 𝑅)    ⇒   ⊢ (𝜑 → 𝑆 Fn 𝑍)
Theorem	noseqrdg0 28693*	Initial value of a recursive definition generator on surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω))    &   ⊢ (𝜑 → 𝑆 = ran 𝑅)    ⇒   ⊢ (𝜑 → (𝑆‘𝐶) = 𝐴)
Theorem	noseqrdgsuc 28694*	Successor value of a recursive definition generator on surreal sequences. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω))    &   ⊢ (𝜑 → 𝑆 = ran 𝑅)    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → (𝑆‘(𝐵 +s 1s )) = (𝐵𝐹(𝑆‘𝐵)))
Theorem	seqsfn 28695	The surreal sequence builder is a function. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ No)    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝑀) “ ω))    ⇒   ⊢ (𝜑 → seqs𝑀( + , 𝐹) Fn 𝑍)
Theorem	seqs1 28696	The value of the surreal sequence builder function at its initial value. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ No)    ⇒   ⊢ (𝜑 → (seqs𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀))
Theorem	seqsp1 28697	The value of the surreal sequence builder at a successor. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ No)    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝑀) “ ω))    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (seqs𝑀( + , 𝐹)‘(𝑁 +s 1s )) = ((seqs𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 +s 1s ))))
15.6.3  Natural numbers
Syntax	cn0s 28698	Declare the syntax for surreal non-negative integers.
class ℕ0s
Syntax	cnns 28699	Declare the syntax for surreal positive integers.
class ℕs
Definition	df-n0s 28700	Define the set of non-negative surreal integers. This set behaves similarly to ω and ℕ0, but it is a set of surreal numbers. Like those two sets, it satisfies the Peano axioms and is closed under (surreal) addition and multiplication. Compare df-nn 12336. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) “ ω)