Metamath Proof Explorer

Theorem reno

Description: A surreal real is a surreal number. (Contributed by Scott Fenton, 19-Feb-2026)

Ref Expression
Assertion reno 
|- ( A e. RR_s -> A e. No )

Proof

Step Hyp Ref Expression
1 elreno 
 |-  ( A e. RR_s <-> ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )
2 1 simplbi 
 |-  ( A e. RR_s -> A e. No )