Definition df-n0s

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

	Ref	Expression
Assertion	df-n0s	$$⊢{\mathbb{N}}_{\mathrm{0s}}=\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x{+}_s{1}_s\right),0_s\right)\left[\mathrm{\omega }\right]$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnn0s	$$class{\mathbb{N}}_{\mathrm{0s}}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvarx$$
4		cadds	$$class{+}_s$$
5		c1s	$$class{1}_s$$
6	3 5 4	co	$$class\left(x{+}_s{1}_s\right)$$
7	1 2 6	cmpt	$$class\left(x\in \mathrm{V}⟼x{+}_s{1}_s\right)$$
8		c0s	$$class{0}_s$$
9	7 8	crdg	$$class\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x{+}_s{1}_s\right),0_s\right)$$
10		com	$$class\mathrm{\omega }$$
11	9 10	cima	$$class\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x{+}_s{1}_s\right),0_s\right)\left[\mathrm{\omega }\right]$$
12	0 11	wceq	$$wff{\mathbb{N}}_{\mathrm{0s}}=\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x{+}_s{1}_s\right),0_s\right)\left[\mathrm{\omega }\right]$$