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 )