Theorem nnord 7820

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 7818	. 2 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)
2		eloni 6329	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐴 ∈ ω → Ord 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2114  Ord word 6318  Oncon0 6319  ωcom 7812

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rab 3391  df-v 3432  df-ss 3907  df-uni 4852  df-tr 5194  df-po 5534  df-so 5535  df-fr 5579  df-we 5581  df-ord 6322  df-on 6323  df-om 7813

This theorem is referenced by:  nnlim  7826  nnsuc  7830  omsucne  7831  omun  7834  nnaordi  8549  nnaord  8550  nnaword  8558  nnmord  8563  nnmwordi  8566  nnawordex  8568  nnaordex2  8570  omsmo  8589  eldifsucnn  8595  enrefnn  8988  pssnn  9098  unfi  9100  phplem2  9134  php  9136  php4  9139  nndomog  9142  onomeneq  9143  ominf  9169  isinf  9170  dif1ennnALT  9182  findcard3  9188  unblem1  9197  isfinite2  9203  unfilem1  9210  inf3lem5  9548  inf3lem6  9549  cantnfp1lem2  9595  cantnfp1lem3  9596  ttrcltr  9632  ttrclss  9636  dmttrcl  9637  rnttrcl  9638  ttrclselem2  9642  dif1card  9927  nnadju  10115  pwsdompw  10120  ackbij1lem5  10140  ackbij1lem14  10149  ackbij1lem16  10151  ackbij1b  10155  ackbij2  10159  sornom  10194  infpssrlem4  10223  infpssrlem5  10224  fin23lem26  10242  fin23lem23  10243  isf32lem2  10271  isf32lem3  10272  isf32lem4  10273  domtriomlem  10359  axdc3lem2  10368  axdc3lem4  10370  canthp1lem2  10571  elni2  10795  piord  10798  addnidpi  10819  indpi  10825  om2uzf1oi  13910  fzennn  13925  hashp1i  14360  om2noseqf1o  28311  bnj529  34904  bnj1098  34946  bnj570  35067  bnj594  35074  bnj580  35075  bnj967  35107  bnj1001  35121  bnj1053  35138  bnj1071  35139  fineqvnttrclselem2  35286  fineqvnttrclselem3  35287  nnuni  35929  hfun  36380  finminlem  36520  mh-inf3f1  36743  finxpsuclem  37733  finxpsuc  37734  wepwso  43495  dflim5  43781