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 } )