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