Theorem nnord 7818

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

Syntax hints:   → wi 4   ∈ wcel 2121  Ord word 6313  Oncon0 6314  ωcom 7810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rab 3394  df-v 3435  df-ss 3902  df-uni 4842  df-tr 5183  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-ord 6317  df-on 6318  df-om 7811

This theorem is referenced by:  nnlim  7824  nnsuc  7828  omsucne  7829  omun  7832  nnaordi  8548  nnaord  8549  nnaword  8557  nnmord  8562  nnmwordi  8565  nnawordex  8567  nnaordex2  8569  omsmo  8588  eldifsucnn  8594  enrefnn  8987  pssnn  9097  unfi  9099  phplem2  9133  php  9135  php4  9138  nndomog  9141  onomeneq  9142  ominf  9168  isinf  9169  dif1ennnALT  9181  findcard3  9187  unblem1  9196  isfinite2  9202  unfilem1  9209  inf3lem5  9548  inf3lem6  9549  cantnfp1lem2  9595  cantnfp1lem3  9596  ttrcltr  9632  ttrclss  9636  dmttrcl  9637  rnttrcl  9638  ttrclselem2  9642  dif1card  9927  nnadju  10115  pwsdompw  10120  ackbij1lem5  10140  ackbij1lem14  10149  ackbij1lem16  10151  ackbij1b  10155  ackbij2  10159  sornom  10194  infpssrlem4  10223  infpssrlem5  10224  fin23lem26  10242  fin23lem23  10243  isf32lem2  10271  isf32lem3  10272  isf32lem4  10273  domtriomlem  10359  axdc3lem2  10368  axdc3lem4  10370  canthp1lem2  10571  elni2  10795  piord  10798  addnidpi  10819  indpi  10825  om2uzf1oi  13910  fzennn  13925  hashp1i  14360  om2noseqf1o  28315  bnj529  34939  bnj1098  34981  bnj570  35102  bnj594  35109  bnj580  35110  bnj967  35142  bnj1001  35156  bnj1053  35173  bnj1071  35174  fineqvnttrclselem2  35318  fineqvnttrclselem3  35319  nnuni  35970  hfun  36421  finminlem  36561  mh-inf3f1  36784  finxpsuclem  37774  finxpsuc  37775  wepwso  43503  dflim5  43789