Theorem nnord 7885

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Ord word 6361  Oncon0 6362  ωcom 7877

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rab 3413  df-v 3452  df-ss 3896  df-uni 4867  df-tr 5212  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366  df-om 7878

This theorem is used by:  nnlim  7891  nnsuc  7895  omsucne  7896  omun  7899  nnaordi  8627  nnaord  8628  nnaword  8636  nnmord  8641  nnmwordi  8644  nnawordex  8646  nnaordex2  8648  omsmo  8667  eldifsucnn  8673  enrefnn  9074  pssnn  9184  unfi  9186  phplem2  9220  php  9222  php4  9225  nndomog  9228  onomeneq  9229  ominf  9255  isinf  9256  dif1ennnALT  9268  findcard3  9274  unblem1  9284  isfinite2  9290  unfilem1  9297  inf3lem5  9633  inf3lem6  9634  cantnfp1lem2  9680  cantnfp1lem3  9681  ttrcltr  9717  ttrclss  9721  dmttrcl  9722  rnttrcl  9723  ttrclselem2  9727  hfunOLD  9919  dif1card  10089  nnadju  10276  pwsdompw  10281  ackbij1lem5  10301  ackbij1lem14  10310  ackbij1lem16  10312  ackbij1b  10316  ackbij2  10320  sornom  10355  infpssrlem4  10384  infpssrlem5  10385  fin23lem26  10403  fin23lem23  10404  isf32lem2  10432  isf32lem3  10433  isf32lem4  10434  domtriomlem  10520  axdc3lem2  10529  axdc3lem4  10531  canthp1lem2  10738  elni2  10962  piord  10965  addnidpi  10986  indpi  10992  om2uzf1oi  14096  fzennn  14111  hashp1i  14547  om2noseqf1o  28687  bnj529  35372  bnj1098  35414  bnj570  35535  bnj594  35542  bnj580  35543  bnj967  35575  bnj1001  35589  bnj1053  35606  bnj1071  35607  fineqvnttrclselem2  35790  fineqvnttrclselem3  35791  nnuni  36492  finminlem  37106  mh-inf3f1  37329  finxpsuclem  38321  finxpsuc  38322  wepwso  44050  dflim5  44331  hashnnlt  46012