Theorem nnssn0s

Description: The positive surreal integers are a subset of the non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025)

	Ref	Expression
Assertion	nnssn0s	⊢ ℕs ⊆ ℕ0s

Proof

Step	Hyp	Ref	Expression
1		df-nns	⊢ ℕs = ( ℕ0s ∖ { 0s } )
2		difss	⊢ ( ℕ0s ∖ { 0s } ) ⊆ ℕ0s
3	1 2	eqsstri	⊢ ℕs ⊆ ℕ0s