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  9563  inf3lem6  9564  cantnfp1lem2  9610  cantnfp1lem3  9611  ttrcltr  9647  ttrclss  9651  dmttrcl  9652  rnttrcl  9653  ttrclselem2  9657  dif1card  9941  nnadju  10129  pwsdompw  10134  ackbij1lem5  10154  ackbij1lem14  10163  ackbij1lem16  10165  ackbij1b  10169  ackbij2  10173  sornom  10208  infpssrlem4  10237  infpssrlem5  10238  fin23lem26  10256  fin23lem23  10257  isf32lem2  10285  isf32lem3  10286  isf32lem4  10287  domtriomlem  10373  axdc3lem2  10382  axdc3lem4  10384  canthp1lem2  10584  elni2  10808  piord  10811  addnidpi  10832  indpi  10838  om2uzf1oi  13896  fzennn  13911  hashp1i  14346  om2noseqf1o  28236  bnj529  34725  bnj1098  34767  bnj570  34889  bnj594  34896  bnj580  34897  bnj967  34929  bnj1001  34943  bnj1053  34960  bnj1071  34961  nnuni  35708  hfun  36160  finminlem  36300  finxpsuclem  37379  finxpsuc  37380  wepwso  43026  dflim5  43312