Theorem nnord 4463

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 4461	. 2 |- ( A e. om -> A e. On )
2		eloni 4235	. 2 |- ( A e. On -> Ord A )
3	1, 2	syl 14	1 |- ( A e. om -> Ord A )

Syntax hints:   -> wi 4   e. wcel 1448   Ord word 4222   Oncon0 4223   omcom 4442

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-13 1459  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-nul 3994  ax-pow 4038  ax-pr 4069  ax-un 4293  ax-iinf 4440

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ral 2380  df-rex 2381  df-v 2643  df-dif 3023  df-un 3025  df-in 3027  df-ss 3034  df-nul 3311  df-pw 3459  df-sn 3480  df-pr 3481  df-uni 3684  df-int 3719  df-tr 3967  df-iord 4226  df-on 4228  df-suc 4231  df-iom 4443

This theorem is referenced by:  nnsucsssuc  6318  nnsucuniel  6321  nntri1  6322  nnsseleq  6327  nntr2  6329  phplem1  6675  phplem2  6676  phplem3  6677  phplem4  6678  phplem4dom  6685  nndomo  6687  dif1en  6702  nnwetri  6733  unsnfi  6736  ctmlemr  6908  nnnninf  6935  piord  7020  addnidpig  7045  archnqq  7126  frecfzennn  10040  hashp1i  10397  ennnfonelemk  11705  ennnfonelemg  11708  ennnfonelemhf1o  11718  ennnfonelemhom  11720  ctinfom  11733  nnsf  12783  peano4nninf  12784  nninfalllemn  12786  nninfsellemeq  12794