Theorem nnord 7850

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

Syntax hints:   → wi 4   ∈ wcel 2109  Ord word 6331  Oncon0 6332  ωcom 7842

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 3406  df-v 3449  df-ss 3931  df-uni 4872  df-tr 5215  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336  df-om 7843

This theorem is referenced by:  nnlim  7856  nnsuc  7860  omsucne  7861  omun  7864  nnaordi  8582  nnaord  8583  nnaword  8591  nnmord  8596  nnmwordi  8599  nnawordex  8601  nnaordex2  8603  omsmo  8622  eldifsucnn  8628  enrefnn  9018  dif1enlemOLD  9121  pssnn  9132  unfi  9135  phplem2  9169  php  9171  php4  9174  nndomog  9177  onomeneq  9178  ominf  9205  ominfOLD  9206  isinf  9207  isinfOLD  9208  dif1ennnALT  9222  findcard3  9229  unblem1  9239  isfinite2  9245  unfilem1  9254  inf3lem5  9585  inf3lem6  9586  cantnfp1lem2  9632  cantnfp1lem3  9633  ttrcltr  9669  ttrclss  9673  dmttrcl  9674  rnttrcl  9675  ttrclselem2  9679  dif1card  9963  nnadju  10151  pwsdompw  10156  ackbij1lem5  10176  ackbij1lem14  10185  ackbij1lem16  10187  ackbij1b  10191  ackbij2  10195  sornom  10230  infpssrlem4  10259  infpssrlem5  10260  fin23lem26  10278  fin23lem23  10279  isf32lem2  10307  isf32lem3  10308  isf32lem4  10309  domtriomlem  10395  axdc3lem2  10404  axdc3lem4  10406  canthp1lem2  10606  elni2  10830  piord  10833  addnidpi  10854  indpi  10860  om2uzf1oi  13918  fzennn  13933  hashp1i  14368  om2noseqf1o  28195  bnj529  34731  bnj1098  34773  bnj570  34895  bnj594  34902  bnj580  34903  bnj967  34935  bnj1001  34949  bnj1053  34966  bnj1071  34967  nnuni  35714  hfun  36166  finminlem  36306  finxpsuclem  37385  finxpsuc  37386  wepwso  43032  dflim5  43318