Metamath Proof Explorer

Theorem norn

Description: The range of a surreal is a subset of the surreal signs. (Contributed by Scott Fenton, 16-Jun-2011)

Ref Expression
Assertion norn 
|- ( A e. No -> ran A C_ { 1o , 2o } )

Proof

Step Hyp Ref Expression
1 elno 
 |-  ( A e. No <-> E. x e. On A : x --> { 1o , 2o } )
2 frn 
 |-  ( A : x --> { 1o , 2o } -> ran A C_ { 1o , 2o } )
3 2 rexlimivw 
 |-  ( E. x e. On A : x --> { 1o , 2o } -> ran A C_ { 1o , 2o } )
4 1 3 sylbi 
 |-  ( A e. No -> ran A C_ { 1o , 2o } )