Theorem nnord 7816

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

Syntax hints:   → wi 4   ∈ wcel 2114  Ord word 6315  Oncon0 6316  ωcom 7808

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ral 3051  df-rab 3399  df-v 3441  df-ss 3917  df-uni 4863  df-tr 5205  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-ord 6319  df-on 6320  df-om 7809

This theorem is referenced by:  nnlim  7822  nnsuc  7826  omsucne  7827  omun  7830  nnaordi  8546  nnaord  8547  nnaword  8555  nnmord  8560  nnmwordi  8563  nnawordex  8565  nnaordex2  8567  omsmo  8586  eldifsucnn  8592  enrefnn  8985  pssnn  9095  unfi  9097  phplem2  9131  php  9133  php4  9136  nndomog  9139  onomeneq  9140  ominf  9166  isinf  9167  dif1ennnALT  9179  findcard3  9185  unblem1  9194  isfinite2  9200  unfilem1  9207  inf3lem5  9543  inf3lem6  9544  cantnfp1lem2  9590  cantnfp1lem3  9591  ttrcltr  9627  ttrclss  9631  dmttrcl  9632  rnttrcl  9633  ttrclselem2  9637  dif1card  9922  nnadju  10110  pwsdompw  10115  ackbij1lem5  10135  ackbij1lem14  10144  ackbij1lem16  10146  ackbij1b  10150  ackbij2  10154  sornom  10189  infpssrlem4  10218  infpssrlem5  10219  fin23lem26  10237  fin23lem23  10238  isf32lem2  10266  isf32lem3  10267  isf32lem4  10268  domtriomlem  10354  axdc3lem2  10363  axdc3lem4  10365  canthp1lem2  10566  elni2  10790  piord  10793  addnidpi  10814  indpi  10820  om2uzf1oi  13878  fzennn  13893  hashp1i  14328  om2noseqf1o  28280  bnj529  34876  bnj1098  34918  bnj570  35040  bnj594  35047  bnj580  35048  bnj967  35080  bnj1001  35094  bnj1053  35111  bnj1071  35112  fineqvnttrclselem2  35257  fineqvnttrclselem3  35258  nnuni  35900  hfun  36351  finminlem  36491  finxpsuclem  37571  finxpsuc  37572  wepwso  43322  dflim5  43608