Metamath Proof Explorer

Theorem nnssno

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

Ref Expression
Assertion nnssno 
|- NN_s C_ No

Proof

Step Hyp Ref Expression
1 nnssn0s 
 |-  NN_s C_ NN0_s
2 n0ssno 
 |-  NN0_s C_ No
3 1 2 sstri 
 |-  NN_s C_ No