P. 285 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28401-28500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	abssubs 28401	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 28402	Declare the syntax for surreal ordinals.
class Ons
Definition	df-ons 28403	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 28404	Membership in the class of surreal ordinals. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ (𝐴 ∈ Ons ↔ (𝐴 ∈ No ∧ ( R ‘𝐴) = ∅))
Theorem	onssno 28405	The surreal ordinals are a subclass of the surreals. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ Ons ⊆ No
Theorem	onno 28406	A surreal ordinal is a surreal. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ (𝐴 ∈ Ons → 𝐴 ∈ No )
Theorem	0ons 28407	Surreal zero is a surreal ordinal. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ 0s ∈ Ons
Theorem	1ons 28408	Surreal one is a surreal ordinal. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ 1s ∈ Ons
Theorem	elons2 28409*	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 28410	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 28411	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 28412*	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 28413*	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 28414	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 28415*	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 28416	The birthday function is one-to-one over the surreal ordinals. (Contributed by Scott Fenton, 6-Nov-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ∧ ( bday ‘𝐴) = ( bday ‘𝐵)) → 𝐴 = 𝐵)
Theorem	onnolt 28417	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 28418	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 28419	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 28420	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 28421	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 28422	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 28423	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 28424	Surreal less-than is set-like over the surreal ordinals. (Contributed by Scott Fenton, 6-Nov-2025.)
⊢ <s Se Ons
Theorem	onsis 28425*	Transfinite induction schema for surreal ordinals. (Contributed by Scott Fenton, 6-Nov-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 ∈ Ons → (∀𝑦 ∈ Ons (𝑦 <s 𝑥 → 𝜓) → 𝜑))    ⇒   ⊢ (𝐴 ∈ Ons → 𝜒)
Theorem	ons2ind 28426*	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 28427*	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 28428	The surreal ordinals are closed under addition. (Contributed by Scott Fenton, 22-Aug-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → (𝐴 +s 𝐵) ∈ Ons)
Theorem	onmulscl 28429	The surreal ordinals are closed under multiplication. (Contributed by Scott Fenton, 22-Aug-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → (𝐴 ·s 𝐵) ∈ Ons)
Theorem	addonbday 28430	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 28431	The successor of a surreal ordinal is a surreal ordinal. (Contributed by Scott Fenton, 22-Aug-2025.)
⊢ (𝐴 ∈ Ons → (𝐴 +s 1s ) ∈ Ons)
Theorem	onsbnd 28432	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 28433	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 ‘𝐴))) → ( -us ‘𝐴) ≤s 𝐵)
15.6.2  Surreal recursive sequences
Syntax	cseqs 28434	Extend class notation with the surreal recursive sequence builder.
class seqs𝑀( + , 𝐹)
Definition	df-seqs 28435*	Define a general-purpose sequence builder for surreal numbers. Compare df-seq 14029. 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 28436	Existence of the surreal sequence builder operation. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ seqs𝑀( + , 𝐹) ∈ V
Theorem	seqseq123d 28437	Equality deduction for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑀 = 𝑁)    &   ⊢ (𝜑 → + = 𝑄)    &   ⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → seqs𝑀( + , 𝐹) = seqs𝑁(𝑄, 𝐺))
Theorem	nfseqs 28438	Hypothesis builder for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ Ⅎ𝑥𝑀    &   ⊢ Ⅎ𝑥 +    &   ⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥seqs𝑀( + , 𝐹)
Theorem	seqsval 28439*	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 28440	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 28441	The surreal 𝐴 is a member of the sequence starting at 𝐴. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑍)
Theorem	noseqp1 28442*	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 28443*	Peano's inductive postulate for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 +s 1s ) ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑍 ⊆ 𝐵)
Theorem	noseqinds 28444*	Induction schema for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑦 = (𝑧 +s 1s ) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑍) → (𝜃 → 𝜏))    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 𝜂)
Theorem	noseqssno 28445	A surreal sequence is a subset of the surreals. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → 𝑍 ⊆ No )
Theorem	noseqno 28446	An element of a surreal sequence is a surreal. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐵 ∈ No )
Theorem	om2noseq0 28447	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 13974. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    ⇒   ⊢ (𝜑 → (𝐺‘∅) = 𝐶)
Theorem	om2noseqsuc 28448*	The value of 𝐺 at a successor. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝐴 ∈ ω)    ⇒   ⊢ (𝜑 → (𝐺‘suc 𝐴) = ((𝐺‘𝐴) +s 1s ))
Theorem	om2noseqfo 28449	Function statement for 𝐺. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺:ω–onto→𝑍)
Theorem	om2noseqlt 28450*	Surreal less-than relation for 𝐺. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ∈ 𝐵 → (𝐺‘𝐴) <s (𝐺‘𝐵)))
Theorem	om2noseqlt2 28451*	The mapping 𝐺 preserves order. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ∈ 𝐵 ↔ (𝐺‘𝐴) <s (𝐺‘𝐵)))
Theorem	om2noseqf1o 28452*	𝐺 is a bijection. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺:ω–1-1-onto→𝑍)
Theorem	om2noseqiso 28453*	𝐺 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 28454*	An alternative definition of 𝐺 in terms of df-oi 9460. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺 = OrdIso( <s , 𝑍))
Theorem	om2noseqrdg 28455*	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 28456*	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 28457*	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 28458*	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 28459*	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 28460	The surreal sequence builder is a function. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ No )    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝑀) “ ω))    ⇒   ⊢ (𝜑 → seqs𝑀( + , 𝐹) Fn 𝑍)
Theorem	seqs1 28461	The value of the surreal sequence builder function at its initial value. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ No )    ⇒   ⊢ (𝜑 → (seqs𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀))
Theorem	seqsp1 28462	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 28463	Declare the syntax for surreal non-negative integers.
class ℕ0s
Syntax	cnns 28464	Declare the syntax for surreal positive integers.
class ℕs
Definition	df-n0s 28465	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 12225. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) “ ω)
Definition	df-nns 28466	Define the set of positive surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs = (ℕ0s ∖ { 0s })
Theorem	n0sexg 28467	The set of all non-negative surreal integers exists. This theorem avoids the axiom of infinity by including it as an antecedent. (Contributed by Scott Fenton, 20-Feb-2025.)
⊢ (ω ∈ V → ℕ0s ∈ V)
Theorem	n0sex 28468	The set of all non-negative surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s ∈ V
Theorem	nnsex 28469	The set of all positive surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs ∈ V
Theorem	peano5n0s 28470*	Peano's inductive postulate for non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → ℕ0s ⊆ 𝐴)
Theorem	n0ssno 28471	The non-negative surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s ⊆ No
Theorem	nnssn0s 28472	The positive surreal integers are a subset of the non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs ⊆ ℕ0s
Theorem	nnssno 28473	The positive surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs ⊆ No
Theorem	n0no 28474	A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 ∈ No )
Theorem	nnno 28475	A positive surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs → 𝐴 ∈ No )
Theorem	n0nod 28476	A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	nnnod 28477	A positive surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕs)    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	nnn0s 28478	A positive surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝐴 ∈ ℕs → 𝐴 ∈ ℕ0s)
Theorem	nnn0sd 28479	A positive surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕs)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℕ0s)
Theorem	0n0s 28480	Peano postulate: 0s is a non-negative surreal integer. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ 0s ∈ ℕ0s
Theorem	peano2n0s 28481	Peano postulate: the successor of a non-negative surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ (𝐴 ∈ ℕ0s → (𝐴 +s 1s ) ∈ ℕ0s)
Theorem	peano2n0sd 28482	Peano postulate: the successor of a non-negative surreal integer is a non-negative surreal integer. Deduction form. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → (𝐴 +s 1s ) ∈ ℕ0s)
Theorem	dfn0s2 28483*	Alternate definition of the set of non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s = ∩ {𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)}
Theorem	n0sind 28484*	Principle of Mathematical Induction (inference schema). Compare nnind 12242 and finds 7881. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ (𝑥 = 0s → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 +s 1s ) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ℕ0s → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ ℕ0s → 𝜏)
Theorem	n0cut 28485	A cut form for non-negative surreal integers. (Contributed by Scott Fenton, 2-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 = ({(𝐴 -s 1s )} |s ∅))
Theorem	n0cut2 28486	A cut form for the successor of a non-negative surreal integer. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ℕ0s → (𝐴 +s 1s ) = ({𝐴} |s ∅))
Theorem	n0on 28487	A surreal natural is a surreal ordinal. (Contributed by Scott Fenton, 2-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 ∈ Ons)
Theorem	nnne0s 28488	A surreal positive integer is nonzero. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs → 𝐴 ≠ 0s )
Theorem	n0sge0 28489	A non-negative integer is greater than or equal to zero. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 0s ≤s 𝐴)
Theorem	nnsgt0 28490	A positive integer is greater than zero. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs → 0s <s 𝐴)
Theorem	elnns 28491	Membership in the positive surreal integers. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs ↔ (𝐴 ∈ ℕ0s ∧ 𝐴 ≠ 0s ))
Theorem	elnns2 28492	A positive surreal integer is a non-negative surreal integer greater than zero. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs ↔ (𝐴 ∈ ℕ0s ∧ 0s <s 𝐴))
Theorem	n0s0suc 28493*	A non-negative surreal integer is either zero or a successor. (Contributed by Scott Fenton, 26-Jul-2025.)
⊢ (𝐴 ∈ ℕ0s → (𝐴 = 0s ∨ ∃𝑥 ∈ ℕ0s 𝐴 = (𝑥 +s 1s )))
Theorem	nnsge1 28494	A positive surreal integer is greater than or equal to one. (Contributed by Scott Fenton, 26-Jul-2025.)
⊢ (𝑁 ∈ ℕs → 1s ≤s 𝑁)
Theorem	n0addscl 28495	The non-negative surreal integers are closed under addition. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕ0s) → (𝐴 +s 𝐵) ∈ ℕ0s)
Theorem	n0mulscl 28496	The non-negative surreal integers are closed under multiplication. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕ0s) → (𝐴 ·s 𝐵) ∈ ℕ0s)
Theorem	nnaddscl 28497	The positive surreal integers are closed under addition. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs) → (𝐴 +s 𝐵) ∈ ℕs)
Theorem	nnmulscl 28498	The positive surreal integers are closed under multiplication. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs) → (𝐴 ·s 𝐵) ∈ ℕs)
Theorem	1n0s 28499	Surreal one is a non-negative surreal integer. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ 1s ∈ ℕ0s
Theorem	1nns 28500	Surreal one is a positive surreal integer. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ 1s ∈ ℕs