Theorem nodmord

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

	Ref	Expression
Assertion	nodmord	⊢ ( 𝐴 ∈ No → Ord dom 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nodmon	⊢ ( 𝐴 ∈ No → dom 𝐴 ∈ On )
2		eloni	⊢ ( dom 𝐴 ∈ On → Ord dom 𝐴 )
3	1 2	syl	⊢ ( 𝐴 ∈ No → Ord dom 𝐴 )