Theorem nnord 7870

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

Syntax hints:   → wi 4   ∈ wcel 2149  Ord word 6360  Oncon0 6361  ωcom 7862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rab 3423  df-v 3463  df-ss 3928  df-uni 4875  df-tr 5221  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-ord 6364  df-on 6365  df-om 7863

This theorem is referenced by:  nnlim  7876  nnsuc  7880  omsucne  7881  omun  7884  nnaordi  8604  nnaord  8605  nnaword  8613  nnmord  8618  nnmwordi  8621  nnawordex  8623  nnaordex2  8625  omsmo  8644  eldifsucnn  8650  enrefnn  9043  pssnn  9153  unfi  9155  phplem2  9189  php  9191  php4  9194  nndomog  9197  onomeneq  9198  ominf  9224  isinf  9225  dif1ennnALT  9237  findcard3  9243  unblem1  9252  isfinite2  9258  unfilem1  9265  inf3lem5  9601  inf3lem6  9602  cantnfp1lem2  9648  cantnfp1lem3  9649  ttrcltr  9685  ttrclss  9689  dmttrcl  9690  rnttrcl  9691  ttrclselem2  9695  dif1card  9994  nnadju  10181  pwsdompw  10186  ackbij1lem5  10206  ackbij1lem14  10215  ackbij1lem16  10217  ackbij1b  10221  ackbij2  10225  sornom  10261  infpssrlem4  10290  infpssrlem5  10291  fin23lem26  10309  fin23lem23  10310  isf32lem2  10338  isf32lem3  10339  isf32lem4  10340  domtriomlem  10426  axdc3lem2  10435  axdc3lem4  10437  canthp1lem2  10638  elni2  10862  piord  10865  addnidpi  10886  indpi  10892  om2uzf1oi  13989  fzennn  14004  hashp1i  14439  om2noseqf1o  28460  bnj529  35075  bnj1098  35117  bnj570  35238  bnj594  35245  bnj580  35246  bnj967  35278  bnj1001  35292  bnj1053  35309  bnj1071  35310  fineqvnttrclselem2  35468  fineqvnttrclselem3  35469  nnuni  36152  hfun  36603  finminlem  36752  mh-inf3f1  36975  finxpsuclem  37966  finxpsuc  37967  wepwso  43697  dflim5  43983  hashnnlt  45658