Definition df-nns

Description: Define the set of positive surreal integers. (Contributed by Scott Fenton, 17-Mar-2025)

	Ref	Expression
Assertion	df-nns	$$⊢{\mathbb{N}}_s={\mathbb{N}}_{\mathrm{0s}}\setminus \left\{0_s\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnns	$$class{\mathbb{N}}_s$$
1		cn0s	$$class{\mathbb{N}}_{\mathrm{0s}}$$
2		c0s	$$class{0}_s$$
3	2	csn	$$class\left\{0_s\right\}$$
4	1 3	cdif	$$class\left({\mathbb{N}}_{\mathrm{0s}}\setminus \left\{0_s\right\}\right)$$
5	0 4	wceq	$$wff{\mathbb{N}}_s={\mathbb{N}}_{\mathrm{0s}}\setminus \left\{0_s\right\}$$