Theorem nnord 7859

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

Syntax hints:   → wi 4   ∈ wcel 2106  Ord word 6360  Oncon0 6361  ωcom 7851

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rab 3433  df-v 3476  df-in 3954  df-ss 3964  df-uni 4908  df-tr 5265  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-ord 6364  df-on 6365  df-om 7852

This theorem is referenced by:  nnlim  7865  nnsuc  7869  omsucne  7870  omun  7874  nnaordi  8614  nnaord  8615  nnaword  8623  nnmord  8628  nnmwordi  8631  nnawordex  8633  omsmo  8653  eldifsucnn  8659  enrefnn  9043  dif1enlemOLD  9153  pssnn  9164  unfi  9168  phplem2  9204  php  9206  php4  9209  nndomog  9212  phplem1OLD  9213  phplem2OLD  9214  phplem3OLD  9215  phplem4OLD  9216  phpOLD  9218  nndomogOLD  9222  onomeneq  9224  ominf  9254  ominfOLD  9255  isinf  9256  isinfOLD  9257  pssnnOLD  9261  dif1ennnALT  9273  findcard3  9281  unblem1  9291  isfinite2  9297  unfilem1  9306  inf3lem5  9623  inf3lem6  9624  cantnfp1lem2  9670  cantnfp1lem3  9671  ttrcltr  9707  ttrclss  9711  dmttrcl  9712  rnttrcl  9713  ttrclselem2  9717  dif1card  10001  nnadju  10188  pwsdompw  10195  ackbij1lem5  10215  ackbij1lem14  10224  ackbij1lem16  10226  ackbij1b  10230  ackbij2  10234  sornom  10268  infpssrlem4  10297  infpssrlem5  10298  fin23lem26  10316  fin23lem23  10317  isf32lem2  10345  isf32lem3  10346  isf32lem4  10347  domtriomlem  10433  axdc3lem2  10442  axdc3lem4  10444  canthp1lem2  10644  elni2  10868  piord  10871  addnidpi  10892  indpi  10898  om2uzf1oi  13914  fzennn  13929  hashp1i  14359  bnj529  33740  bnj1098  33782  bnj570  33904  bnj594  33911  bnj580  33912  bnj967  33944  bnj1001  33958  bnj1053  33975  bnj1071  33976  nnuni  34684  hfun  35138  finminlem  35191  finxpsuclem  36266  finxpsuc  36267  wepwso  41770  dflim5  42064