Metamath Proof Explorer

Theorem n0ssno

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

Ref Expression
Assertion n0ssno 
|- NN0_s C_ No

Proof

Step Hyp Ref Expression
1 df-n0s 
 |-  NN0_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) " _om )
2 1 a1i 
 |-  ( T. -> NN0_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) " _om ) )
3 0sno 
 |-  0s e. No
4 3 a1i 
 |-  ( T. -> 0s e. No )
5 2 4 noseqssno 
 |-  ( T. -> NN0_s C_ No )
6 5 mptru 
 |-  NN0_s C_ No