Theorem nnord 7896

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

Syntax hints:   → wi 4   ∈ wcel 2107  Ord word 6382  Oncon0 6383  ωcom 7888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rab 3436  df-v 3481  df-ss 3967  df-uni 4907  df-tr 5259  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-ord 6386  df-on 6387  df-om 7889

This theorem is referenced by:  nnlim  7902  nnsuc  7906  omsucne  7907  omun  7910  nnaordi  8657  nnaord  8658  nnaword  8666  nnmord  8671  nnmwordi  8674  nnawordex  8676  nnaordex2  8678  omsmo  8697  eldifsucnn  8703  enrefnn  9088  dif1enlemOLD  9198  pssnn  9209  unfi  9212  phplem2  9246  php  9248  php4  9251  nndomog  9254  phplem1OLD  9255  phplem2OLD  9256  phplem3OLD  9257  phplem4OLD  9258  phpOLD  9260  nndomogOLD  9264  onomeneq  9266  ominf  9295  ominfOLD  9296  isinf  9297  isinfOLD  9298  dif1ennnALT  9312  findcard3  9319  unblem1  9329  isfinite2  9335  unfilem1  9344  inf3lem5  9673  inf3lem6  9674  cantnfp1lem2  9720  cantnfp1lem3  9721  ttrcltr  9757  ttrclss  9761  dmttrcl  9762  rnttrcl  9763  ttrclselem2  9767  dif1card  10051  nnadju  10239  pwsdompw  10244  ackbij1lem5  10264  ackbij1lem14  10273  ackbij1lem16  10275  ackbij1b  10279  ackbij2  10283  sornom  10318  infpssrlem4  10347  infpssrlem5  10348  fin23lem26  10366  fin23lem23  10367  isf32lem2  10395  isf32lem3  10396  isf32lem4  10397  domtriomlem  10483  axdc3lem2  10492  axdc3lem4  10494  canthp1lem2  10694  elni2  10918  piord  10921  addnidpi  10942  indpi  10948  om2uzf1oi  13995  fzennn  14010  hashp1i  14443  om2noseqf1o  28308  bnj529  34756  bnj1098  34798  bnj570  34920  bnj594  34927  bnj580  34928  bnj967  34960  bnj1001  34974  bnj1053  34991  bnj1071  34992  nnuni  35728  hfun  36180  finminlem  36320  finxpsuclem  37399  finxpsuc  37400  wepwso  43060  dflim5  43347