Metamath Proof Explorer

Theorem 2sno

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

Ref Expression
Assertion 2sno 
|- 2s e. No

Proof

Step Hyp Ref Expression
1 2nns 
 |-  2s e. NN_s
2 nnsno 
 |-  ( 2s e. NN_s -> 2s e. No )
3 1 2 ax-mp 
 |-  2s e. No