Theorem nnord 7593

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

Assertion

Ref	Expression
nnord	⊢ (𝐴 ∈ ω → Ord 𝐴)

Proof of Theorem nnord

Step	Hyp	Ref	Expression
1		nnon 7591	. 2 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)
2		eloni 6184	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐴 ∈ ω → Ord 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2111  Ord word 6173  Oncon0 6174  ωcom 7585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-rab 3079  df-v 3411  df-in 3867  df-ss 3877  df-uni 4802  df-tr 5143  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-ord 6177  df-on 6178  df-om 7586

This theorem is referenced by:  nnlim  7598  nnsuc  7602  omsucne  7603  nnaordi  8260  nnaord  8261  nnaword  8269  nnmord  8274  nnmwordi  8277  nnawordex  8279  omsmo  8297  enrefnn  8630  phplem1  8731  phplem2  8732  phplem3  8733  phplem4  8734  php  8736  php4  8739  nndomog  8743  dif1enlem  8744  pssnn  8751  unfi  8754  ominf  8781  isinf  8782  pssnnOLD  8787  dif1enOLD  8800  unblem1  8816  isfinite2  8822  unfilem1  8828  inf3lem5  9141  inf3lem6  9142  cantnfp1lem2  9188  cantnfp1lem3  9189  dif1card  9483  nnadju  9670  pwsdompw  9677  ackbij1lem5  9697  ackbij1lem14  9706  ackbij1lem16  9708  ackbij1b  9712  ackbij2  9716  sornom  9750  infpssrlem4  9779  infpssrlem5  9780  fin23lem26  9798  fin23lem23  9799  isf32lem2  9827  isf32lem3  9828  isf32lem4  9829  domtriomlem  9915  axdc3lem2  9924  axdc3lem4  9926  canthp1lem2  10126  elni2  10350  piord  10353  addnidpi  10374  indpi  10380  om2uzf1oi  13383  fzennn  13398  hashp1i  13827  bnj529  32252  bnj1098  32295  bnj570  32417  bnj594  32424  bnj580  32425  bnj967  32457  bnj1001  32471  bnj1053  32488  bnj1071  32489  hfun  34063  finminlem  34090  finxpsuclem  35128  finxpsuc  35129  wepwso  40395