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 )