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
|- ( A e. No -> Ord dom A )

Proof

Step Hyp Ref Expression
1 nodmon
 |-  ( A e. No -> dom A e. On )
2 eloni
 |-  ( dom A e. On -> Ord dom A )
3 1 2 syl
 |-  ( A e. No -> Ord dom A )