Theorem nnord 7863

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

Syntax hints:   → wi 4   ∈ wcel 2107  Ord word 6364  Oncon0 6365  ωcom 7855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-tr 5267  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-ord 6368  df-on 6369  df-om 7856

This theorem is referenced by:  nnlim  7869  nnsuc  7873  omsucne  7874  omun  7878  nnaordi  8618  nnaord  8619  nnaword  8627  nnmord  8632  nnmwordi  8635  nnawordex  8637  omsmo  8657  eldifsucnn  8663  enrefnn  9047  dif1enlemOLD  9157  pssnn  9168  unfi  9172  phplem2  9208  php  9210  php4  9213  nndomog  9216  phplem1OLD  9217  phplem2OLD  9218  phplem3OLD  9219  phplem4OLD  9220  phpOLD  9222  nndomogOLD  9226  onomeneq  9228  ominf  9258  ominfOLD  9259  isinf  9260  isinfOLD  9261  pssnnOLD  9265  dif1ennnALT  9277  findcard3  9285  unblem1  9295  isfinite2  9301  unfilem1  9310  inf3lem5  9627  inf3lem6  9628  cantnfp1lem2  9674  cantnfp1lem3  9675  ttrcltr  9711  ttrclss  9715  dmttrcl  9716  rnttrcl  9717  ttrclselem2  9721  dif1card  10005  nnadju  10192  pwsdompw  10199  ackbij1lem5  10219  ackbij1lem14  10228  ackbij1lem16  10230  ackbij1b  10234  ackbij2  10238  sornom  10272  infpssrlem4  10301  infpssrlem5  10302  fin23lem26  10320  fin23lem23  10321  isf32lem2  10349  isf32lem3  10350  isf32lem4  10351  domtriomlem  10437  axdc3lem2  10446  axdc3lem4  10448  canthp1lem2  10648  elni2  10872  piord  10875  addnidpi  10896  indpi  10902  om2uzf1oi  13918  fzennn  13933  hashp1i  14363  bnj529  33783  bnj1098  33825  bnj570  33947  bnj594  33954  bnj580  33955  bnj967  33987  bnj1001  34001  bnj1053  34018  bnj1071  34019  nnuni  34727  hfun  35181  finminlem  35251  finxpsuclem  36326  finxpsuc  36327  wepwso  41833  dflim5  42127