Theorem nnord 4583

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

Assertion

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

Proof of Theorem nnord

Step	Hyp	Ref	Expression
1		nnon 4581	. 2 |- ( A e. om -> A e. On )
2		eloni 4347	. 2 |- ( A e. On -> Ord A )
3	1, 2	syl 14	1 |- ( A e. om -> Ord A )

Syntax hints:   -> wi 4   e. wcel 2135   Ord word 4334   Oncon0 4335   omcom 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-sep 4094  ax-nul 4102  ax-pow 4147  ax-pr 4181  ax-un 4405  ax-iinf 4559

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447  df-rex 2448  df-v 2723  df-dif 3113  df-un 3115  df-in 3117  df-ss 3124  df-nul 3405  df-pw 3555  df-sn 3576  df-pr 3577  df-uni 3784  df-int 3819  df-tr 4075  df-iord 4338  df-on 4340  df-suc 4343  df-iom 4562

This theorem is referenced by:  nnsucsssuc  6451  nnsucuniel  6454  nntri1  6455  nnsseleq  6460  nntr2  6462  phplem1  6809  phplem2  6810  phplem3  6811  phplem4  6812  phplem4dom  6819  nndomo  6821  dif1en  6836  nnwetri  6872  unsnfi  6875  ctmlemr  7064  nnnninf  7081  nnnninfeq  7083  nnnninfeq2  7084  nninfisol  7088  piord  7243  addnidpig  7268  archnqq  7349  frecfzennn  10351  hashp1i  10712  ennnfonelemk  12270  ennnfonelemg  12273  ennnfonelemhf1o  12283  ennnfonelemhom  12285  ctinfom  12298  nnsf  13719  peano4nninf  13720  nninfsellemeq  13728