Theorem nnord 7814

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

Syntax hints:   → wi 4   ∈ wcel 2109  Ord word 6310  Oncon0 6311  ωcom 7806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rab 3397  df-v 3440  df-ss 3922  df-uni 4862  df-tr 5203  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-ord 6314  df-on 6315  df-om 7807

This theorem is referenced by:  nnlim  7820  nnsuc  7824  omsucne  7825  omun  7828  nnaordi  8543  nnaord  8544  nnaword  8552  nnmord  8557  nnmwordi  8560  nnawordex  8562  nnaordex2  8564  omsmo  8583  eldifsucnn  8589  enrefnn  8979  dif1enlemOLD  9081  pssnn  9092  unfi  9095  phplem2  9129  php  9131  php4  9134  nndomog  9137  onomeneq  9138  ominf  9163  ominfOLD  9164  isinf  9165  isinfOLD  9166  dif1ennnALT  9180  findcard3  9187  unblem1  9197  isfinite2  9203  unfilem1  9212  inf3lem5  9547  inf3lem6  9548  cantnfp1lem2  9594  cantnfp1lem3  9595  ttrcltr  9631  ttrclss  9635  dmttrcl  9636  rnttrcl  9637  ttrclselem2  9641  dif1card  9923  nnadju  10111  pwsdompw  10116  ackbij1lem5  10136  ackbij1lem14  10145  ackbij1lem16  10147  ackbij1b  10151  ackbij2  10155  sornom  10190  infpssrlem4  10219  infpssrlem5  10220  fin23lem26  10238  fin23lem23  10239  isf32lem2  10267  isf32lem3  10268  isf32lem4  10269  domtriomlem  10355  axdc3lem2  10364  axdc3lem4  10366  canthp1lem2  10566  elni2  10790  piord  10793  addnidpi  10814  indpi  10820  om2uzf1oi  13879  fzennn  13894  hashp1i  14329  om2noseqf1o  28219  bnj529  34727  bnj1098  34769  bnj570  34891  bnj594  34898  bnj580  34899  bnj967  34931  bnj1001  34945  bnj1053  34962  bnj1071  34963  nnuni  35719  hfun  36171  finminlem  36311  finxpsuclem  37390  finxpsuc  37391  wepwso  43036  dflim5  43322