Metamath Proof Explorer

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 
|- NN_s C_ NN0_s

Proof

Step Hyp Ref Expression
1 df-nns 
 |-  NN_s = ( NN0_s \ { 0s } )
2 difss 
 |-  ( NN0_s \ { 0s } ) C_ NN0_s
3 1 2 eqsstri 
 |-  NN_s C_ NN0_s