Theorem nnsex

Description: The set of all positive surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025)

	Ref	Expression
Assertion	nnsex	⊢ ℕs ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-nns	⊢ ℕs = ( ℕ0s ∖ { 0s } )
2		n0sex	⊢ ℕ0s ∈ V
3	2	difexi	⊢ ( ℕ0s ∖ { 0s } ) ∈ V
4	1 3	eqeltri	⊢ ℕs ∈ V