P. 286 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28501-28600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	divsdird 28501	Distribution of surreal division over addition. (Contributed by Scott Fenton, 13-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) /su 𝐶) = ((𝐴 /su 𝐶) +s (𝐵 /su 𝐶)))
Theorem	divscan3d 28502	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 28503	Declare the syntax for surreal absolute value.
class abss
Definition	df-abss 28504	Define the surreal absolute value function. See abssval 28505 for its value and absscl 28506 for its closure. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ abss = (𝑥 ∈ No ↦ if( 0s ≤s 𝑥, 𝑥, ( -us ‘𝑥)))
Theorem	abssval 28505	The value of surreal absolute value. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → (abss‘𝐴) = if( 0s ≤s 𝐴, 𝐴, ( -us ‘𝐴)))
Theorem	absscl 28506	Closure law for surreal absolute value. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → (abss‘𝐴) ∈ No )
Theorem	abssid 28507	The absolute value of a non-negative surreal is itself. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 0s ≤s 𝐴) → (abss‘𝐴) = 𝐴)
Theorem	abs0s 28508	The absolute value of surreal zero. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (abss‘ 0s ) = 0s
Theorem	abssnid 28509	For a negative surreal, its absolute value is its negation. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → (abss‘𝐴) = ( -us ‘𝐴))
Theorem	absmuls 28510	Surreal absolute value distributes over multiplication. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (abss‘(𝐴 ·s 𝐵)) = ((abss‘𝐴) ·s (abss‘𝐵)))
Theorem	abssge0 28511	The absolute value of a surreal number is non-negative. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → 0s ≤s (abss‘𝐴))
Theorem	abssor 28512	The absolute value of a surreal is either that surreal or its negative. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → ((abss‘𝐴) = 𝐴 ∨ (abss‘𝐴) = ( -us ‘𝐴)))
Theorem	absnegs 28513	Surreal absolute value of the negative. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → (abss‘( -us ‘𝐴)) = (abss‘𝐴))
Theorem	leabss 28514	A surreal is less than or equal to its absolute value. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → 𝐴 ≤s (abss‘𝐴))
Theorem	abslts 28515	Surreal absolute value and less-than relation. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((abss‘𝐴) <s 𝐵 ↔ (( -us ‘𝐵) <s 𝐴 ∧ 𝐴 <s 𝐵)))
Theorem	abssubs 28516	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 28517	Declare the syntax for surreal ordinals.
class Ons
Definition	df-ons 28518	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 28519	Membership in the class of surreal ordinals. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ (𝐴 ∈ Ons ↔ (𝐴 ∈ No ∧ ( R ‘𝐴) = ∅))
Theorem	onssno 28520	The surreal ordinals are a subclass of the surreals. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ Ons ⊆ No
Theorem	onno 28521	A surreal ordinal is a surreal. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ (𝐴 ∈ Ons → 𝐴 ∈ No )
Theorem	0ons 28522	Surreal zero is a surreal ordinal. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ 0s ∈ Ons
Theorem	1ons 28523	Surreal one is a surreal ordinal. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ 1s ∈ Ons
Theorem	elons2 28524*	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 28525	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 28526	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 28527*	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 28528*	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 28529	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 28530*	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 28531	The birthday function is one-to-one over the surreal ordinals. (Contributed by Scott Fenton, 6-Nov-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ∧ ( bday ‘𝐴) = ( bday ‘𝐵)) → 𝐴 = 𝐵)
Theorem	onnolt 28532	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 28533	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 28534	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 28535	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 28536	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 28537	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 28538	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 28539	Surreal less-than is set-like over the surreal ordinals. (Contributed by Scott Fenton, 6-Nov-2025.)
⊢ <s Se Ons
Theorem	onsis 28540*	Transfinite induction schema for surreal ordinals. (Contributed by Scott Fenton, 6-Nov-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 ∈ Ons → (∀𝑦 ∈ Ons (𝑦 <s 𝑥 → 𝜓) → 𝜑))    ⇒   ⊢ (𝐴 ∈ Ons → 𝜒)
Theorem	ons2ind 28541*	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 28542*	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 28543	The surreal ordinals are closed under addition. (Contributed by Scott Fenton, 22-Aug-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → (𝐴 +s 𝐵) ∈ Ons)
Theorem	onmulscl 28544	The surreal ordinals are closed under multiplication. (Contributed by Scott Fenton, 22-Aug-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → (𝐴 ·s 𝐵) ∈ Ons)
Theorem	addonbday 28545	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 28546	The successor of a surreal ordinal is a surreal ordinal. (Contributed by Scott Fenton, 22-Aug-2025.)
⊢ (𝐴 ∈ Ons → (𝐴 +s 1s ) ∈ Ons)
Theorem	onsbnd 28547	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 28548	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 28549	Extend class notation with the surreal recursive sequence builder.
class seqs𝑀( + , 𝐹)
Definition	df-seqs 28550*	Define a general-purpose sequence builder for surreal numbers. Compare df-seq 14068. 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 28551	Existence of the surreal sequence builder operation. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ seqs𝑀( + , 𝐹) ∈ V
Theorem	seqseq123d 28552	Equality deduction for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑀 = 𝑁)    &   ⊢ (𝜑 → + = 𝑄)    &   ⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → seqs𝑀( + , 𝐹) = seqs𝑁(𝑄, 𝐺))
Theorem	nfseqs 28553	Hypothesis builder for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ Ⅎ𝑥𝑀    &   ⊢ Ⅎ𝑥 +    &   ⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥seqs𝑀( + , 𝐹)
Theorem	seqsval 28554*	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 28555	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 28556	The surreal 𝐴 is a member of the sequence starting at 𝐴. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑍)
Theorem	noseqp1 28557*	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 28558*	Peano's inductive postulate for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 +s 1s ) ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑍 ⊆ 𝐵)
Theorem	noseqinds 28559*	Induction schema for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑦 = (𝑧 +s 1s ) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑍) → (𝜃 → 𝜏))    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 𝜂)
Theorem	noseqssno 28560	A surreal sequence is a subset of the surreals. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → 𝑍 ⊆ No )
Theorem	noseqno 28561	An element of a surreal sequence is a surreal. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐵 ∈ No )
Theorem	om2noseq0 28562	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 14013. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    ⇒   ⊢ (𝜑 → (𝐺‘∅) = 𝐶)
Theorem	om2noseqsuc 28563*	The value of 𝐺 at a successor. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝐴 ∈ ω)    ⇒   ⊢ (𝜑 → (𝐺‘suc 𝐴) = ((𝐺‘𝐴) +s 1s ))
Theorem	om2noseqfo 28564	Function statement for 𝐺. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺:ω–onto→𝑍)
Theorem	om2noseqlt 28565*	Surreal less-than relation for 𝐺. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ∈ 𝐵 → (𝐺‘𝐴) <s (𝐺‘𝐵)))
Theorem	om2noseqlt2 28566*	The mapping 𝐺 preserves order. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ∈ 𝐵 ↔ (𝐺‘𝐴) <s (𝐺‘𝐵)))
Theorem	om2noseqf1o 28567*	𝐺 is a bijection. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺:ω–1-1-onto→𝑍)
Theorem	om2noseqiso 28568*	𝐺 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 28569*	An alternative definition of 𝐺 in terms of df-oi 9485. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺 = OrdIso( <s , 𝑍))
Theorem	om2noseqrdg 28570*	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 28571*	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 28572*	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 28573*	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 28574*	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 28575	The surreal sequence builder is a function. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ No )    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝑀) “ ω))    ⇒   ⊢ (𝜑 → seqs𝑀( + , 𝐹) Fn 𝑍)
Theorem	seqs1 28576	The value of the surreal sequence builder function at its initial value. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ No )    ⇒   ⊢ (𝜑 → (seqs𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀))
Theorem	seqsp1 28577	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 28578	Declare the syntax for surreal non-negative integers.
class ℕ0s
Syntax	cnns 28579	Declare the syntax for surreal positive integers.
class ℕs
Definition	df-n0s 28580	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 12261. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) “ ω)
Definition	df-nns 28581	Define the set of positive surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs = (ℕ0s ∖ { 0s })
Theorem	n0sexg 28582	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 28583	The set of all non-negative surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s ∈ V
Theorem	nnsex 28584	The set of all positive surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs ∈ V
Theorem	peano5n0s 28585*	Peano's inductive postulate for non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → ℕ0s ⊆ 𝐴)
Theorem	n0ssno 28586	The non-negative surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s ⊆ No
Theorem	nnssn0s 28587	The positive surreal integers are a subset of the non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs ⊆ ℕ0s
Theorem	nnssno 28588	The positive surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs ⊆ No
Theorem	n0no 28589	A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 ∈ No )
Theorem	nnno 28590	A positive surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs → 𝐴 ∈ No )
Theorem	n0nod 28591	A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	nnnod 28592	A positive surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕs)    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	nnn0s 28593	A positive surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝐴 ∈ ℕs → 𝐴 ∈ ℕ0s)
Theorem	nnn0sd 28594	A positive surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕs)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℕ0s)
Theorem	0n0s 28595	Peano postulate: 0s is a non-negative surreal integer. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ 0s ∈ ℕ0s
Theorem	peano2n0s 28596	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 28597	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 28598*	Alternate definition of the set of non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s = ∩ {𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)}
Theorem	n0sind 28599*	Principle of Mathematical Induction (inference schema). Compare nnind 12278 and finds 7896. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ (𝑥 = 0s → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 +s 1s ) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ℕ0s → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ ℕ0s → 𝜏)
Theorem	n0cut 28600	A cut form for non-negative surreal integers. (Contributed by Scott Fenton, 2-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 = ({(𝐴 -s 1s )} |s ∅))