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	⊢ ( 𝐴 ∈ No → ran 𝐴 ⊆ { 1o , 2o } )

Proof

Step	Hyp	Ref	Expression
1		elno	⊢ ( 𝐴 ∈ No ↔ ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } )
2		frn	⊢ ( 𝐴 : 𝑥 ⟶ { 1o , 2o } → ran 𝐴 ⊆ { 1o , 2o } )
3	2	rexlimivw	⊢ ( ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } → ran 𝐴 ⊆ { 1o , 2o } )
4	1 3	sylbi	⊢ ( 𝐴 ∈ No → ran 𝐴 ⊆ { 1o , 2o } )