Metamath Proof Explorer

Theorem n0snod

Description: A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025)

Ref Expression
Hypothesis n0snod.1 
|- ( ph -> A e. NN0_s )
Assertion n0snod 
|- ( ph -> A e. No )

Proof

Step Hyp Ref Expression
1 n0snod.1 
 |-  ( ph -> A e. NN0_s )
2 n0sno 
 |-  ( A e. NN0_s -> A e. No )
3 1 2 syl 
 |-  ( ph -> A e. No )