Metamath Proof Explorer


Theorem nnord

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

Ref Expression
Assertion nnord AωOrdA

Proof

Step Hyp Ref Expression
1 nnon AωAOn
2 eloni AOnOrdA
3 1 2 syl AωOrdA