Theorem nnord 7828

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

Syntax hints:   → wi 4   ∈ wcel 2114  Ord word 6326  Oncon0 6327  ωcom 7820

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rab 3402  df-v 3444  df-ss 3920  df-uni 4866  df-tr 5208  df-po 5542  df-so 5543  df-fr 5587  df-we 5589  df-ord 6330  df-on 6331  df-om 7821

This theorem is referenced by:  nnlim  7834  nnsuc  7838  omsucne  7839  omun  7842  nnaordi  8558  nnaord  8559  nnaword  8567  nnmord  8572  nnmwordi  8575  nnawordex  8577  nnaordex2  8579  omsmo  8598  eldifsucnn  8604  enrefnn  8997  pssnn  9107  unfi  9109  phplem2  9143  php  9145  php4  9148  nndomog  9151  onomeneq  9152  ominf  9178  isinf  9179  dif1ennnALT  9191  findcard3  9197  unblem1  9206  isfinite2  9212  unfilem1  9219  inf3lem5  9555  inf3lem6  9556  cantnfp1lem2  9602  cantnfp1lem3  9603  ttrcltr  9639  ttrclss  9643  dmttrcl  9644  rnttrcl  9645  ttrclselem2  9649  dif1card  9934  nnadju  10122  pwsdompw  10127  ackbij1lem5  10147  ackbij1lem14  10156  ackbij1lem16  10158  ackbij1b  10162  ackbij2  10166  sornom  10201  infpssrlem4  10230  infpssrlem5  10231  fin23lem26  10249  fin23lem23  10250  isf32lem2  10278  isf32lem3  10279  isf32lem4  10280  domtriomlem  10366  axdc3lem2  10375  axdc3lem4  10377  canthp1lem2  10578  elni2  10802  piord  10805  addnidpi  10826  indpi  10832  om2uzf1oi  13890  fzennn  13905  hashp1i  14340  om2noseqf1o  28314  bnj529  34924  bnj1098  34966  bnj570  35087  bnj594  35094  bnj580  35095  bnj967  35127  bnj1001  35141  bnj1053  35158  bnj1071  35159  fineqvnttrclselem2  35306  fineqvnttrclselem3  35307  nnuni  35949  hfun  36400  finminlem  36540  finxpsuclem  37679  finxpsuc  37680  wepwso  43429  dflim5  43715