Theorem nodmon

Description: The domain of a surreal is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011)

	Ref	Expression
Assertion	nodmon	⊢ ( 𝐴 ∈ No → dom 𝐴 ∈ On )

Proof

Step	Hyp	Ref	Expression
1		elno	⊢ ( 𝐴 ∈ No ↔ ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } )
2		fdm	⊢ ( 𝐴 : 𝑥 ⟶ { 1o , 2o } → dom 𝐴 = 𝑥 )
3	2	eleq1d	⊢ ( 𝐴 : 𝑥 ⟶ { 1o , 2o } → ( dom 𝐴 ∈ On ↔ 𝑥 ∈ On ) )
4	3	biimprcd	⊢ ( 𝑥 ∈ On → ( 𝐴 : 𝑥 ⟶ { 1o , 2o } → dom 𝐴 ∈ On ) )
5	4	rexlimiv	⊢ ( ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } → dom 𝐴 ∈ On )
6	1 5	sylbi	⊢ ( 𝐴 ∈ No → dom 𝐴 ∈ On )