Definition df-nns 28339

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

Assertion

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

Detailed syntax breakdown of Definition df-nns

Step	Hyp	Ref	Expression
1		cnns 28337	. 2 class ℕs
2		cnn0s 28336	. . 3 class ℕ0s
3		c0s 27885	. . . 4 class 0s
4	3	csn 4648	. . 3 class { 0s }
5	2, 4	cdif 3973	. 2 class (ℕ0s ∖ { 0s })
6	1, 5	wceq 1537	1 wff ℕs = (ℕ0s ∖ { 0s })

This definition is referenced by:  nnsex  28341  nnssn0s  28344  nnne0s  28358  elnns  28361  1nns  28370