Metamath Proof Explorer


Theorem nodmord

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

Ref Expression
Assertion nodmord ANoOrddomA

Proof

Step Hyp Ref Expression
1 nodmon ANodomAOn
2 eloni domAOnOrddomA
3 1 2 syl ANoOrddomA