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

Syntax hints:   → wi 4   ∈ wcel 2114  Ord word 6311  Oncon0 6312  ωcom 7806

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 3050  df-rab 3388  df-v 3429  df-ss 3902  df-uni 4841  df-tr 5182  df-po 5528  df-so 5529  df-fr 5573  df-we 5575  df-ord 6315  df-on 6316  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  8982  pssnn  9092  unfi  9094  phplem2  9128  php  9130  php4  9133  nndomog  9136  onomeneq  9137  ominf  9163  isinf  9164  dif1ennnALT  9176  findcard3  9182  unblem1  9191  isfinite2  9197  unfilem1  9204  inf3lem5  9542  inf3lem6  9543  cantnfp1lem2  9589  cantnfp1lem3  9590  ttrcltr  9626  ttrclss  9630  dmttrcl  9631  rnttrcl  9632  ttrclselem2  9636  dif1card  9921  nnadju  10109  pwsdompw  10114  ackbij1lem5  10134  ackbij1lem14  10143  ackbij1lem16  10145  ackbij1b  10149  ackbij2  10153  sornom  10188  infpssrlem4  10217  infpssrlem5  10218  fin23lem26  10236  fin23lem23  10237  isf32lem2  10265  isf32lem3  10266  isf32lem4  10267  domtriomlem  10353  axdc3lem2  10362  axdc3lem4  10364  canthp1lem2  10565  elni2  10789  piord  10792  addnidpi  10813  indpi  10819  om2uzf1oi  13904  fzennn  13919  hashp1i  14354  om2noseqf1o  28281  bnj529  34872  bnj1098  34914  bnj570  35035  bnj594  35042  bnj580  35043  bnj967  35075  bnj1001  35089  bnj1053  35106  bnj1071  35107  fineqvnttrclselem2  35254  fineqvnttrclselem3  35255  nnuni  35897  hfun  36348  finminlem  36488  mh-inf3f1  36711  finxpsuclem  37701  finxpsuc  37702  wepwso  43459  dflim5  43745