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