Theorem nnord 7856

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

Syntax hints:   → wi 4   ∈ wcel 2144  Ord word 6347  Oncon0 6348  ωcom 7848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-rab 3417  df-v 3458  df-ss 3923  df-uni 4868  df-tr 5210  df-po 5557  df-so 5558  df-fr 5602  df-we 5604  df-ord 6351  df-on 6352  df-om 7849

This theorem is referenced by:  nnlim  7862  nnsuc  7866  omsucne  7867  omun  7870  nnaordi  8590  nnaord  8591  nnaword  8599  nnmord  8604  nnmwordi  8607  nnawordex  8609  nnaordex2  8611  omsmo  8630  eldifsucnn  8636  enrefnn  9029  pssnn  9139  unfi  9141  phplem2  9175  php  9177  php4  9180  nndomog  9183  onomeneq  9184  ominf  9210  isinf  9211  dif1ennnALT  9223  findcard3  9229  unblem1  9238  isfinite2  9244  unfilem1  9251  inf3lem5  9589  inf3lem6  9590  cantnfp1lem2  9636  cantnfp1lem3  9637  ttrcltr  9673  ttrclss  9677  dmttrcl  9678  rnttrcl  9679  ttrclselem2  9683  dif1card  9968  nnadju  10156  pwsdompw  10161  ackbij1lem5  10181  ackbij1lem14  10190  ackbij1lem16  10192  ackbij1b  10196  ackbij2  10200  sornom  10236  infpssrlem4  10265  infpssrlem5  10266  fin23lem26  10284  fin23lem23  10285  isf32lem2  10313  isf32lem3  10314  isf32lem4  10315  domtriomlem  10401  axdc3lem2  10410  axdc3lem4  10412  canthp1lem2  10613  elni2  10837  piord  10840  addnidpi  10861  indpi  10867  om2uzf1oi  13968  fzennn  13983  hashp1i  14418  om2noseqf1o  28396  bnj529  35039  bnj1098  35081  bnj570  35202  bnj594  35209  bnj580  35210  bnj967  35242  bnj1001  35256  bnj1053  35273  bnj1071  35274  fineqvnttrclselem2  35422  fineqvnttrclselem3  35423  nnuni  36082  hfun  36533  finminlem  36683  mh-inf3f1  36906  finxpsuclem  37896  finxpsuc  37897  wepwso  43625  dflim5  43911