P. 284 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28301-28400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	noseqinds 28301*	Induction schema for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑦 = (𝑧 +s 1s ) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑍) → (𝜃 → 𝜏))    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 𝜂)
Theorem	noseqssno 28302	A surreal sequence is a subset of the surreals. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → 𝑍 ⊆ No )
Theorem	noseqno 28303	An element of a surreal sequence is a surreal. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐵 ∈ No )
Theorem	om2noseq0 28304	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 13882. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    ⇒   ⊢ (𝜑 → (𝐺‘∅) = 𝐶)
Theorem	om2noseqsuc 28305*	The value of 𝐺 at a successor. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝐴 ∈ ω)    ⇒   ⊢ (𝜑 → (𝐺‘suc 𝐴) = ((𝐺‘𝐴) +s 1s ))
Theorem	om2noseqfo 28306	Function statement for 𝐺. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺:ω–onto→𝑍)
Theorem	om2noseqlt 28307*	Surreal less-than relation for 𝐺. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ∈ 𝐵 → (𝐺‘𝐴) <s (𝐺‘𝐵)))
Theorem	om2noseqlt2 28308*	The mapping 𝐺 preserves order. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ∈ 𝐵 ↔ (𝐺‘𝐴) <s (𝐺‘𝐵)))
Theorem	om2noseqf1o 28309*	𝐺 is a bijection. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺:ω–1-1-onto→𝑍)
Theorem	om2noseqiso 28310*	𝐺 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 28311*	An alternative definition of 𝐺 in terms of df-oi 9427. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺 = OrdIso( <s , 𝑍))
Theorem	om2noseqrdg 28312*	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 28313*	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 28314*	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 28315*	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 28316*	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 28317	The surreal sequence builder is a function. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ No )    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝑀) “ ω))    ⇒   ⊢ (𝜑 → seqs𝑀( + , 𝐹) Fn 𝑍)
Theorem	seqs1 28318	The value of the surreal sequence builder function at its initial value. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ No )    ⇒   ⊢ (𝜑 → (seqs𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀))
Theorem	seqsp1 28319	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 28320	Declare the syntax for surreal non-negative integers.
class ℕ0s
Syntax	cnns 28321	Declare the syntax for surreal positive integers.
class ℕs
Definition	df-n0s 28322	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 12158. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) “ ω)
Definition	df-nns 28323	Define the set of positive surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs = (ℕ0s ∖ { 0s })
Theorem	n0sexg 28324	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 28325	The set of all non-negative surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s ∈ V
Theorem	nnsex 28326	The set of all positive surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs ∈ V
Theorem	peano5n0s 28327*	Peano's inductive postulate for non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → ℕ0s ⊆ 𝐴)
Theorem	n0ssno 28328	The non-negative surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s ⊆ No
Theorem	nnssn0s 28329	The positive surreal integers are a subset of the non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs ⊆ ℕ0s
Theorem	nnssno 28330	The positive surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs ⊆ No
Theorem	n0no 28331	A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 ∈ No )
Theorem	nnno 28332	A positive surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs → 𝐴 ∈ No )
Theorem	n0nod 28333	A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	nnnod 28334	A positive surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕs)    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	nnn0s 28335	A positive surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝐴 ∈ ℕs → 𝐴 ∈ ℕ0s)
Theorem	nnn0sd 28336	A positive surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕs)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℕ0s)
Theorem	0n0s 28337	Peano postulate: 0s is a non-negative surreal integer. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ 0s ∈ ℕ0s
Theorem	peano2n0s 28338	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 28339	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 28340*	Alternate definition of the set of non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s = ∩ {𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)}
Theorem	n0sind 28341*	Principle of Mathematical Induction (inference schema). Compare nnind 12175 and finds 7848. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ (𝑥 = 0s → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 +s 1s ) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ℕ0s → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ ℕ0s → 𝜏)
Theorem	n0cut 28342	A cut form for non-negative surreal integers. (Contributed by Scott Fenton, 2-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 = ({(𝐴 -s 1s )} |s ∅))
Theorem	n0cut2 28343	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 28344	A surreal natural is a surreal ordinal. (Contributed by Scott Fenton, 2-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 ∈ Ons)
Theorem	nnne0s 28345	A surreal positive integer is nonzero. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs → 𝐴 ≠ 0s )
Theorem	n0sge0 28346	A non-negative integer is greater than or equal to zero. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 0s ≤s 𝐴)
Theorem	nnsgt0 28347	A positive integer is greater than zero. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs → 0s <s 𝐴)
Theorem	elnns 28348	Membership in the positive surreal integers. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs ↔ (𝐴 ∈ ℕ0s ∧ 𝐴 ≠ 0s ))
Theorem	elnns2 28349	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 28350*	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 28351	A positive surreal integer is greater than or equal to one. (Contributed by Scott Fenton, 26-Jul-2025.)
⊢ (𝑁 ∈ ℕs → 1s ≤s 𝑁)
Theorem	n0addscl 28352	The non-negative surreal integers are closed under addition. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕ0s) → (𝐴 +s 𝐵) ∈ ℕ0s)
Theorem	n0mulscl 28353	The non-negative surreal integers are closed under multiplication. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕ0s) → (𝐴 ·s 𝐵) ∈ ℕ0s)
Theorem	nnaddscl 28354	The positive surreal integers are closed under addition. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs) → (𝐴 +s 𝐵) ∈ ℕs)
Theorem	nnmulscl 28355	The positive surreal integers are closed under multiplication. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs) → (𝐴 ·s 𝐵) ∈ ℕs)
Theorem	1n0s 28356	Surreal one is a non-negative surreal integer. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ 1s ∈ ℕ0s
Theorem	1nns 28357	Surreal one is a positive surreal integer. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ 1s ∈ ℕs
Theorem	peano2nns 28358	Peano postulate for positive surreal integers. One plus a positive surreal integer is a positive surreal integer. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs → (𝐴 +s 1s ) ∈ ℕs)
Theorem	nnsrecgt0d 28359	The reciprocal of a positive surreal integer is positive. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕs)    ⇒   ⊢ (𝜑 → 0s <s ( 1s /su 𝐴))
Theorem	n0bday 28360	A non-negative surreal integer has a finite birthday. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → ( bday ‘𝐴) ∈ ω)
Theorem	n0ssoldg 28361	The non-negative surreal integers are a subset of the old set of ω. To avoid the axiom of infinity, we include it as an antecedent. (Contributed by Scott Fenton, 20-Feb-2026.)
⊢ (ω ∈ V → ℕ0s ⊆ ( O ‘ω))
Theorem	n0ssold 28362	The non-negative surreal integers are a subset of the old set of ω. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ ℕ0s ⊆ ( O ‘ω)
Theorem	n0fincut 28363	The simplest number greater than a finite set of non-negative surreal integers is a non-negative surreal integer. (Contributed by Scott Fenton, 5-Nov-2025.)
⊢ ((𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin) → (𝐴 |s ∅) ∈ ℕ0s)
Theorem	onsfi 28364	A surreal ordinal with a finite birthday is a non-negative surreal integer. (Contributed by Scott Fenton, 4-Nov-2025.)
⊢ ((𝐴 ∈ Ons ∧ ( bday ‘𝐴) ∈ ω) → 𝐴 ∈ ℕ0s)
Theorem	eln0s2 28365	A non-negative surreal integer is a surreal ordinal with a finite birthday. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ ℕ0s ↔ (𝐴 ∈ Ons ∧ ( bday ‘𝐴) ∈ ω))
Theorem	onltn0s 28366	A surreal ordinal that is less than a non-negative integer is a non-negative integer. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ ℕ0s ∧ 𝐴 <s 𝐵) → 𝐴 ∈ ℕ0s)
Theorem	n0cutlt 28367*	A non-negative surreal integer is the simplest number greater than all previous non-negative surreal integers. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 = ({𝑥 ∈ ℕ0s ∣ 𝑥 <s 𝐴} |s ∅))
Theorem	seqn0sfn 28368	The surreal sequence builder is a function over ℕ0s when started from zero. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → seqs 0s ( + , 𝐹) Fn ℕ0s)
Theorem	eln0s 28369	A non-negative surreal integer is zero or a positive surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝐴 ∈ ℕ0s ↔ (𝐴 ∈ ℕs ∨ 𝐴 = 0s ))
Theorem	n0s0m1 28370	Every non-negative surreal integer is either zero or a successor. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝐴 ∈ ℕ0s → (𝐴 = 0s ∨ (𝐴 -s 1s ) ∈ ℕ0s))
Theorem	n0subs 28371	Subtraction of non-negative surreal integers. (Contributed by Scott Fenton, 26-May-2025.)
⊢ ((𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝑀 ≤s 𝑁 ↔ (𝑁 -s 𝑀) ∈ ℕ0s))
Theorem	n0subs2 28372	Subtraction of non-negative surreal integers. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝑀 <s 𝑁 ↔ (𝑁 -s 𝑀) ∈ ℕs))
Theorem	n0ltsp1le 28373	Non-negative surreal ordering relation. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝑀 <s 𝑁 ↔ (𝑀 +s 1s ) ≤s 𝑁))
Theorem	n0lesltp1 28374	Non-negative surreal ordering relation. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝑀 ≤s 𝑁 ↔ 𝑀 <s (𝑁 +s 1s )))
Theorem	n0lesm1lt 28375	Non-negative surreal ordering relation. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ ((𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝑀 ≤s 𝑁 ↔ (𝑀 -s 1s ) <s 𝑁))
Theorem	n0lts1e0 28376	A non-negative surreal integer is less than one iff it is zero. (Contributed by Scott Fenton, 23-Feb-2026.)
⊢ (𝐴 ∈ ℕ0s → (𝐴 <s 1s ↔ 𝐴 = 0s ))
Theorem	bdayn0p1 28377	The birthday of 𝐴 +s 1s is the successor of the birthday of 𝐴 when 𝐴 is a non-negative surreal integer. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ℕ0s → ( bday ‘(𝐴 +s 1s )) = suc ( bday ‘𝐴))
Theorem	bdayn0sf1o 28378	The birthday function restricted to the non-negative surreal integers is a bijection with the finite ordinals. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ( bday ↾ ℕ0s):ℕ0s–1-1-onto→ω
Theorem	n0p1nns 28379	One plus a non-negative surreal integer is a positive surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝐴 ∈ ℕ0s → (𝐴 +s 1s ) ∈ ℕs)
Theorem	dfnns2 28380	Alternate definition of the positive surreal integers. Compare df-nn 12158. (Contributed by Scott Fenton, 6-Aug-2025.)
⊢ ℕs = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 1s ) “ ω)
Theorem	nnsind 28381*	Principle of Mathematical Induction (inference schema). (Contributed by Scott Fenton, 6-Aug-2025.)
⊢ (𝑥 = 1s → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 +s 1s ) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ℕs → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ ℕs → 𝜏)
Theorem	nn1m1nns 28382	Every positive surreal integer is either one or a successor. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ (𝐴 ∈ ℕs → (𝐴 = 1s ∨ (𝐴 -s 1s ) ∈ ℕs))
Theorem	nnm1n0s 28383	A positive surreal integer minus one is a non-negative surreal integer. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ (𝑁 ∈ ℕs → (𝑁 -s 1s ) ∈ ℕ0s)
Theorem	eucliddivs 28384*	Euclid's division lemma for surreal numbers. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ ((𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕs) → ∃𝑝 ∈ ℕ0s ∃𝑞 ∈ ℕ0s (𝐴 = ((𝐵 ·s 𝑝) +s 𝑞) ∧ 𝑞 <s 𝐵))
Theorem	oldfib 28385	The old set of an ordinal is finite iff the ordinal is finite. (Contributed by Scott Fenton, 19-Feb-2026.)
⊢ (𝐴 ∈ On → (𝐴 ∈ ω ↔ ( O ‘𝐴) ∈ Fin))
15.6.4  Integers
Syntax	czs 28386	Declare the syntax for surreal integers.
class ℤs
Definition	df-zs 28387	Define the surreal integers. Compare dfz2 12519. (Contributed by Scott Fenton, 17-May-2025.)
⊢ ℤs = ( -s “ (ℕs × ℕs))
Theorem	zsex 28388	The surreal integers form a set. (Contributed by Scott Fenton, 17-May-2025.)
⊢ ℤs ∈ V
Theorem	zssno 28389	The surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-May-2025.)
⊢ ℤs ⊆ No
Theorem	zno 28390	A surreal integer is a surreal. (Contributed by Scott Fenton, 17-May-2025.)
⊢ (𝐴 ∈ ℤs → 𝐴 ∈ No )
Theorem	znod 28391	A surreal integer is a surreal. Deduction form. (Contributed by Scott Fenton, 17-May-2025.)
⊢ (𝜑 → 𝐴 ∈ ℤs)    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	elzs 28392*	Membership in the set of surreal integers. (Contributed by Scott Fenton, 17-May-2025.)
⊢ (𝐴 ∈ ℤs ↔ ∃𝑥 ∈ ℕs ∃𝑦 ∈ ℕs 𝐴 = (𝑥 -s 𝑦))
Theorem	nnzsubs 28393	The difference of two surreal positive integers is an integer. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ ((𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs) → (𝐴 -s 𝐵) ∈ ℤs)
Theorem	nnzs 28394	A positive surreal integer is a surreal integer. (Contributed by Scott Fenton, 17-May-2025.)
⊢ (𝐴 ∈ ℕs → 𝐴 ∈ ℤs)
Theorem	nnzsd 28395	A positive surreal integer is a surreal integer. Deduction form. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕs)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℤs)
Theorem	0zs 28396	Zero is a surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ 0s ∈ ℤs
Theorem	n0zs 28397	A non-negative surreal integer is a surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 ∈ ℤs)
Theorem	n0zsd 28398	A non-negative surreal integer is a surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℤs)
Theorem	1zs 28399	One is a surreal integer. (Contributed by Scott Fenton, 24-Jul-2025.)
⊢ 1s ∈ ℤs
Theorem	znegscl 28400	The surreal integers are closed under negation. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝐴 ∈ ℤs → ( -us ‘𝐴) ∈ ℤs)