Theorem nnssno

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

	Ref	Expression
Assertion	nnssno	⊢ ℕs ⊆ No

Proof

Step	Hyp	Ref	Expression
1		nnssn0s	⊢ ℕs ⊆ ℕ0s
2		n0ssno	⊢ ℕ0s ⊆ No
3	1 2	sstri	⊢ ℕs ⊆ No