P. 288 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28701-28800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	seqsex 28701	Existence of the surreal sequence builder operation. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ seqs𝑀( + , 𝐹) ∈ V
Theorem	seqseq123d 28702	Equality deduction for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑀 = 𝑁)    &   ⊢ (𝜑 → + = 𝑄)    &   ⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → seqs𝑀( + , 𝐹) = seqs𝑁(𝑄, 𝐺))
Theorem	nfseqs 28703	Hypothesis builder for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ Ⅎ𝑥𝑀    &   ⊢ Ⅎ𝑥 +    &   ⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥seqs𝑀( + , 𝐹)
Theorem	seqsval 28704*	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 28705	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 28706	The surreal 𝐴 is a member of the sequence starting at 𝐴. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑍)
Theorem	noseqp1 28707*	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 28708*	Peano's inductive postulate for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 +s 1s ) ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑍 ⊆ 𝐵)
Theorem	noseqinds 28709*	Induction schema for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑦 = (𝑧 +s 1s ) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑍) → (𝜃 → 𝜏))    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 𝜂)
Theorem	noseqssno 28710	A surreal sequence is a subset of the surreals. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → 𝑍 ⊆ No)
Theorem	noseqno 28711	An element of a surreal sequence is a surreal. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐵 ∈ No)
Theorem	om2noseq0 28712	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 14117. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    ⇒   ⊢ (𝜑 → (𝐺‘∅) = 𝐶)
Theorem	om2noseqsuc 28713*	The value of 𝐺 at a successor. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝐴 ∈ ω)    ⇒   ⊢ (𝜑 → (𝐺‘suc 𝐴) = ((𝐺‘𝐴) +s 1s ))
Theorem	om2noseqfo 28714	Function statement for 𝐺. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺:ω⟶onto𝑍)
Theorem	om2noseqlt 28715*	Surreal less-than relation for 𝐺. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ∈ 𝐵 → (𝐺‘𝐴) <s (𝐺‘𝐵)))
Theorem	om2noseqlt2 28716*	The mapping 𝐺 preserves order. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ∈ 𝐵 ↔ (𝐺‘𝐴) <s (𝐺‘𝐵)))
Theorem	om2noseqf1o 28717*	𝐺 is a bijection. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺:ω⟶1-1onto𝑍)
Theorem	om2noseqiso 28718*	𝐺 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 28719*	An alternative definition of 𝐺 in terms of df-oi 9531. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺 = OrdIso( <s , 𝑍))
Theorem	om2noseqrdg 28720*	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 28721*	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 28722*	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 28723*	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 28724*	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 28725	The surreal sequence builder is a function. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ No)    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝑀) “ ω))    ⇒   ⊢ (𝜑 → seqs𝑀( + , 𝐹) Fn 𝑍)
Theorem	seqs1 28726	The value of the surreal sequence builder function at its initial value. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ No)    ⇒   ⊢ (𝜑 → (seqs𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀))
Theorem	seqsp1 28727	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 28728	Declare the syntax for surreal non-negative integers.
class ℕ0s
Syntax	cnns 28729	Declare the syntax for surreal positive integers.
class ℕs
Definition	df-n0s 28730	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 12363. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) “ ω)
Definition	df-nns 28731	Define the set of positive surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs = (ℕ0s ∖ { 0s })
Theorem	n0sexg 28732	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 28733	The set of all non-negative surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s ∈ V
Theorem	nnsex 28734	The set of all positive surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs ∈ V
Theorem	peano5n0s 28735*	Peano's inductive postulate for non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → ℕ0s ⊆ 𝐴)
Theorem	n0ssno 28736	The non-negative surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s ⊆ No
Theorem	nnssn0s 28737	The positive surreal integers are a subset of the non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs ⊆ ℕ0s
Theorem	nnssno 28738	The positive surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs ⊆ No
Theorem	n0no 28739	A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 ∈ No)
Theorem	nnno 28740	A positive surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs → 𝐴 ∈ No)
Theorem	n0nod 28741	A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → 𝐴 ∈ No)
Theorem	nnnod 28742	A positive surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕs)    ⇒   ⊢ (𝜑 → 𝐴 ∈ No)
Theorem	nnn0s 28743	A positive surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝐴 ∈ ℕs → 𝐴 ∈ ℕ0s)
Theorem	nnn0sd 28744	A positive surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕs)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℕ0s)
Theorem	0n0s 28745	Peano postulate: 0s is a non-negative surreal integer. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ 0s ∈ ℕ0s
Theorem	peano2n0s 28746	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 28747	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 28748*	Alternate definition of the set of non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s = ∩ {𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)}
Theorem	n0sind 28749*	Principle of Mathematical Induction (inference schema). Compare nnind 12380 and finds 7932. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ (𝑥 = 0s → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 +s 1s ) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ℕ0s → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ ℕ0s → 𝜏)
Theorem	n0cut 28750	A cut form for non-negative surreal integers. (Contributed by Scott Fenton, 2-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 = ({(𝐴 −s 1s )} |s ∅))
Theorem	n0cut2 28751	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 28752	A surreal natural is a surreal ordinal. (Contributed by Scott Fenton, 2-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 ∈ Ons)
Theorem	nnne0s 28753	A surreal positive integer is nonzero. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs → 𝐴 ≠ 0s )
Theorem	n0sge0 28754	A non-negative integer is greater than or equal to zero. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 0s ≤s 𝐴)
Theorem	nnsgt0 28755	A positive integer is greater than zero. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs → 0s <s 𝐴)
Theorem	elnns 28756	Membership in the positive surreal integers. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs ↔ (𝐴 ∈ ℕ0s ∧ 𝐴 ≠ 0s ))
Theorem	elnns2 28757	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 28758*	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 28759	A positive surreal integer is greater than or equal to one. (Contributed by Scott Fenton, 26-Jul-2025.)
⊢ (𝑁 ∈ ℕs → 1s ≤s 𝑁)
Theorem	n0addscl 28760	The non-negative surreal integers are closed under addition. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕ0s) → (𝐴 +s 𝐵) ∈ ℕ0s)
Theorem	n0mulscl 28761	The non-negative surreal integers are closed under multiplication. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕ0s) → (𝐴 ·s 𝐵) ∈ ℕ0s)
Theorem	nnaddscl 28762	The positive surreal integers are closed under addition. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs) → (𝐴 +s 𝐵) ∈ ℕs)
Theorem	nnmulscl 28763	The positive surreal integers are closed under multiplication. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs) → (𝐴 ·s 𝐵) ∈ ℕs)
Theorem	1n0s 28764	Surreal one is a non-negative surreal integer. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ 1s ∈ ℕ0s
Theorem	1nns 28765	Surreal one is a positive surreal integer. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ 1s ∈ ℕs
Theorem	peano2nns 28766	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 28767	The reciprocal of a positive surreal integer is positive. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕs)    ⇒   ⊢ (𝜑 → 0s <s ( 1s /su 𝐴))
Theorem	n0bday 28768	A non-negative surreal integer has a finite birthday. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → (bday‘𝐴) ∈ ω)
Theorem	n0ssoldg 28769	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 28770	The non-negative surreal integers are a subset of the old set of ω. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ ℕ0s ⊆ (O‘ω)
Theorem	n0fincut 28771	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 28772	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 28773	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 28774	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 28775*	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 28776	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 28777	A non-negative surreal integer is zero or a positive surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝐴 ∈ ℕ0s ↔ (𝐴 ∈ ℕs ∨ 𝐴 = 0s ))
Theorem	n0s0m1 28778	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 28779	Subtraction of non-negative surreal integers. (Contributed by Scott Fenton, 26-May-2025.)
⊢ ((𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝑀 ≤s 𝑁 ↔ (𝑁 −s 𝑀) ∈ ℕ0s))
Theorem	n0subs2 28780	Subtraction of non-negative surreal integers. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝑀 <s 𝑁 ↔ (𝑁 −s 𝑀) ∈ ℕs))
Theorem	n0ltsp1le 28781	Non-negative surreal ordering relation. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝑀 <s 𝑁 ↔ (𝑀 +s 1s ) ≤s 𝑁))
Theorem	n0lesltp1 28782	Non-negative surreal ordering relation. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝑀 ≤s 𝑁 ↔ 𝑀 <s (𝑁 +s 1s )))
Theorem	n0lesm1lt 28783	Non-negative surreal ordering relation. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ ((𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝑀 ≤s 𝑁 ↔ (𝑀 −s 1s ) <s 𝑁))
Theorem	n0lts1e0 28784	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 28785	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 28786	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-1ontoω
Theorem	n0p1nns 28787	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 28788	Alternate definition of the positive surreal integers. Compare df-nn 12363. (Contributed by Scott Fenton, 6-Aug-2025.)
⊢ ℕs = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 1s ) “ ω)
Theorem	nnsind 28789*	Principle of Mathematical Induction (inference schema). (Contributed by Scott Fenton, 6-Aug-2025.)
⊢ (𝑥 = 1s → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 +s 1s ) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ℕs → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ ℕs → 𝜏)
Theorem	nn1m1nns 28790	Every positive surreal integer is either one or a successor. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ (𝐴 ∈ ℕs → (𝐴 = 1s ∨ (𝐴 −s 1s ) ∈ ℕs))
Theorem	nnm1n0s 28791	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 28792*	Euclid's division lemma for surreal numbers. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ ((𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕs) → ∃𝑝 ∈ ℕ0s ∃𝑞 ∈ ℕ0s (𝐴 = ((𝐵 ·s 𝑝) +s 𝑞) ∧ 𝑞 <s 𝐵))
Theorem	oldfib 28793	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 28794	Declare the syntax for surreal integers.
class ℤs
Definition	df-zs 28795	Define the surreal integers. Compare dfz2 12739. (Contributed by Scott Fenton, 17-May-2025.)
⊢ ℤs = ( −s “ (ℕs × ℕs))
Theorem	zsex 28796	The surreal integers form a set. (Contributed by Scott Fenton, 17-May-2025.)
⊢ ℤs ∈ V
Theorem	zssno 28797	The surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-May-2025.)
⊢ ℤs ⊆ No
Theorem	zno 28798	A surreal integer is a surreal. (Contributed by Scott Fenton, 17-May-2025.)
⊢ (𝐴 ∈ ℤs → 𝐴 ∈ No)
Theorem	znod 28799	A surreal integer is a surreal. Deduction form. (Contributed by Scott Fenton, 17-May-2025.)
⊢ (𝜑 → 𝐴 ∈ ℤs)    ⇒   ⊢ (𝜑 → 𝐴 ∈ No)
Theorem	elzs 28800*	Membership in the set of surreal integers. (Contributed by Scott Fenton, 17-May-2025.)
⊢ (𝐴 ∈ ℤs ↔ ∃𝑥 ∈ ℕs ∃𝑦 ∈ ℕs 𝐴 = (𝑥 −s 𝑦))