This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnord

Description: A natural number is ordinal. (Contributed by NM, 17-Oct-1995)

Ref Expression
Assertion nnord 
|- ( A e. _om -> Ord A )

Proof

Step Hyp Ref Expression
1 nnon 
 |-  ( A e. _om -> A e. On )
2 eloni 
 |-  ( A e. On -> Ord A )
3 1 2 syl 
 |-  ( A e. _om -> Ord A )