Theorem nnord 7830

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

Syntax hints:   → wi 4   ∈ wcel 2109  Ord word 6319  Oncon0 6320  ωcom 7822

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 3403  df-v 3446  df-ss 3928  df-uni 4868  df-tr 5210  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6323  df-on 6324  df-om 7823

This theorem is referenced by:  nnlim  7836  nnsuc  7840  omsucne  7841  omun  7844  nnaordi  8559  nnaord  8560  nnaword  8568  nnmord  8573  nnmwordi  8576  nnawordex  8578  nnaordex2  8580  omsmo  8599  eldifsucnn  8605  enrefnn  8995  dif1enlemOLD  9098  pssnn  9109  unfi  9112  phplem2  9146  php  9148  php4  9151  nndomog  9154  onomeneq  9155  ominf  9181  ominfOLD  9182  isinf  9183  isinfOLD  9184  dif1ennnALT  9198  findcard3  9205  unblem1  9215  isfinite2  9221  unfilem1  9230  inf3lem5  9561  inf3lem6  9562  cantnfp1lem2  9608  cantnfp1lem3  9609  ttrcltr  9645  ttrclss  9649  dmttrcl  9650  rnttrcl  9651  ttrclselem2  9655  dif1card  9939  nnadju  10127  pwsdompw  10132  ackbij1lem5  10152  ackbij1lem14  10161  ackbij1lem16  10163  ackbij1b  10167  ackbij2  10171  sornom  10206  infpssrlem4  10235  infpssrlem5  10236  fin23lem26  10254  fin23lem23  10255  isf32lem2  10283  isf32lem3  10284  isf32lem4  10285  domtriomlem  10371  axdc3lem2  10380  axdc3lem4  10382  canthp1lem2  10582  elni2  10806  piord  10809  addnidpi  10830  indpi  10836  om2uzf1oi  13894  fzennn  13909  hashp1i  14344  om2noseqf1o  28235  bnj529  34724  bnj1098  34766  bnj570  34888  bnj594  34895  bnj580  34896  bnj967  34928  bnj1001  34942  bnj1053  34959  bnj1071  34960  nnuni  35707  hfun  36159  finminlem  36299  finxpsuclem  37378  finxpsuc  37379  wepwso  43025  dflim5  43311