Theorem nnord 7911

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

Syntax hints:   → wi 4   ∈ wcel 2108  Ord word 6394  Oncon0 6395  ωcom 7903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rab 3444  df-v 3490  df-ss 3993  df-uni 4932  df-tr 5284  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-ord 6398  df-on 6399  df-om 7904

This theorem is referenced by:  nnlim  7917  nnsuc  7921  omsucne  7922  omun  7926  nnaordi  8674  nnaord  8675  nnaword  8683  nnmord  8688  nnmwordi  8691  nnawordex  8693  nnaordex2  8695  omsmo  8714  eldifsucnn  8720  enrefnn  9113  dif1enlemOLD  9223  pssnn  9234  unfi  9238  phplem2  9271  php  9273  php4  9276  nndomog  9279  phplem1OLD  9280  phplem2OLD  9281  phplem3OLD  9282  phplem4OLD  9283  phpOLD  9285  nndomogOLD  9289  onomeneq  9291  ominf  9321  ominfOLD  9322  isinf  9323  isinfOLD  9324  dif1ennnALT  9339  findcard3  9346  unblem1  9356  isfinite2  9362  unfilem1  9371  inf3lem5  9701  inf3lem6  9702  cantnfp1lem2  9748  cantnfp1lem3  9749  ttrcltr  9785  ttrclss  9789  dmttrcl  9790  rnttrcl  9791  ttrclselem2  9795  dif1card  10079  nnadju  10267  pwsdompw  10272  ackbij1lem5  10292  ackbij1lem14  10301  ackbij1lem16  10303  ackbij1b  10307  ackbij2  10311  sornom  10346  infpssrlem4  10375  infpssrlem5  10376  fin23lem26  10394  fin23lem23  10395  isf32lem2  10423  isf32lem3  10424  isf32lem4  10425  domtriomlem  10511  axdc3lem2  10520  axdc3lem4  10522  canthp1lem2  10722  elni2  10946  piord  10949  addnidpi  10970  indpi  10976  om2uzf1oi  14004  fzennn  14019  hashp1i  14452  om2noseqf1o  28325  bnj529  34717  bnj1098  34759  bnj570  34881  bnj594  34888  bnj580  34889  bnj967  34921  bnj1001  34935  bnj1053  34952  bnj1071  34953  nnuni  35689  hfun  36142  finminlem  36284  finxpsuclem  37363  finxpsuc  37364  wepwso  43000  dflim5  43291