Theorem nnord 7807

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

Syntax hints:   → wi 4   ∈ wcel 2109  Ord word 6306  Oncon0 6307  ωcom 7799

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 3395  df-v 3438  df-ss 3920  df-uni 4859  df-tr 5200  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6310  df-on 6311  df-om 7800

This theorem is referenced by:  nnlim  7813  nnsuc  7817  omsucne  7818  omun  7821  nnaordi  8536  nnaord  8537  nnaword  8545  nnmord  8550  nnmwordi  8553  nnawordex  8555  nnaordex2  8557  omsmo  8576  eldifsucnn  8582  enrefnn  8972  pssnn  9082  unfi  9085  phplem2  9119  php  9121  php4  9124  nndomog  9127  onomeneq  9128  ominf  9153  isinf  9154  dif1ennnALT  9166  findcard3  9172  unblem1  9181  isfinite2  9187  unfilem1  9194  inf3lem5  9528  inf3lem6  9529  cantnfp1lem2  9575  cantnfp1lem3  9576  ttrcltr  9612  ttrclss  9616  dmttrcl  9617  rnttrcl  9618  ttrclselem2  9622  dif1card  9904  nnadju  10092  pwsdompw  10097  ackbij1lem5  10117  ackbij1lem14  10126  ackbij1lem16  10128  ackbij1b  10132  ackbij2  10136  sornom  10171  infpssrlem4  10200  infpssrlem5  10201  fin23lem26  10219  fin23lem23  10220  isf32lem2  10248  isf32lem3  10249  isf32lem4  10250  domtriomlem  10336  axdc3lem2  10345  axdc3lem4  10347  canthp1lem2  10547  elni2  10771  piord  10774  addnidpi  10795  indpi  10801  om2uzf1oi  13860  fzennn  13875  hashp1i  14310  om2noseqf1o  28202  bnj529  34724  bnj1098  34766  bnj570  34888  bnj594  34895  bnj580  34896  bnj967  34928  bnj1001  34942  bnj1053  34959  bnj1071  34960  fineqvnttrclselem2  35091  fineqvnttrclselem3  35092  nnuni  35720  hfun  36172  finminlem  36312  finxpsuclem  37391  finxpsuc  37392  wepwso  43036  dflim5  43322