Metamath Proof Explorer

Theorem 2nns

Description: Surreal two is a surreal natural. (Contributed by Scott Fenton, 23-Jul-2025)

Ref Expression
Assertion 2nns 
|- 2s e. NN_s

Proof

Step Hyp Ref Expression
1 1p1e2s 
 |-  ( 1s +s 1s ) = 2s
2 1nns 
 |-  1s e. NN_s
3 peano2nns 
 |-  ( 1s e. NN_s -> ( 1s +s 1s ) e. NN_s )
4 2 3 ax-mp 
 |-  ( 1s +s 1s ) e. NN_s
5 1 4 eqeltrri 
 |-  2s e. NN_s