Definition df-nns

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

	Ref	Expression
Assertion	df-nns	⊢ ℕs = ( ℕ0s ∖ { 0s } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnns	⊢ ℕs
1		cn0s	⊢ ℕ0s
2		c0s	⊢ 0s
3	2	csn	⊢ { 0s }
4	1 3	cdif	⊢ ( ℕ0s ∖ { 0s } )
5	0 4	wceq	⊢ ℕs = ( ℕ0s ∖ { 0s } )