Definition df-n0s 28295

Description: Define the set of non-negative surreal integers. This set behaves similarly to ω and ℕ₀, 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 12150. (Contributed by Scott Fenton, 17-Mar-2025.)

Assertion

Ref	Expression
df-n0s	⊢ ℕ0s = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) “ ω)

Detailed syntax breakdown of Definition df-n0s

Step	Hyp	Ref	Expression
1		cnn0s 28293	. 2 class ℕ0s
2		vx	. . . . 5 setvar 𝑥
3		cvv 3441	. . . . 5 class V
4	2	cv 1541	. . . . . 6 class 𝑥
5		c1s 27804	. . . . . 6 class 1s
6		cadds 27941	. . . . . 6 class +s
7	4, 5, 6	co 7360	. . . . 5 class (𝑥 +s 1s )
8	2, 3, 7	cmpt 5180	. . . 4 class (𝑥 ∈ V ↦ (𝑥 +s 1s ))
9		c0s 27803	. . . 4 class 0s
10	8, 9	crdg 8342	. . 3 class rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s )
11		com 7810	. . 3 class ω
12	10, 11	cima 5628	. 2 class (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) “ ω)
13	1, 12	wceq 1542	1 wff ℕ0s = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) “ ω)

This definition is referenced by:  n0sexg  28297  peano5n0s  28300  n0ssno  28301  0n0s  28310  peano2n0s  28311  n0sind  28313  seqn0sfn  28339