Theorem nnord 7818

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

Syntax hints:   → wi 4   ∈ wcel 2114  Ord word 6317  Oncon0 6318  ωcom 7810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rab 3401  df-v 3443  df-ss 3919  df-uni 4865  df-tr 5207  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6321  df-on 6322  df-om 7811

This theorem is referenced by:  nnlim  7824  nnsuc  7828  omsucne  7829  omun  7832  nnaordi  8548  nnaord  8549  nnaword  8557  nnmord  8562  nnmwordi  8565  nnawordex  8567  nnaordex2  8569  omsmo  8588  eldifsucnn  8594  enrefnn  8987  pssnn  9097  unfi  9099  phplem2  9133  php  9135  php4  9138  nndomog  9141  onomeneq  9142  ominf  9168  isinf  9169  dif1ennnALT  9181  findcard3  9187  unblem1  9196  isfinite2  9202  unfilem1  9209  inf3lem5  9545  inf3lem6  9546  cantnfp1lem2  9592  cantnfp1lem3  9593  ttrcltr  9629  ttrclss  9633  dmttrcl  9634  rnttrcl  9635  ttrclselem2  9639  dif1card  9924  nnadju  10112  pwsdompw  10117  ackbij1lem5  10137  ackbij1lem14  10146  ackbij1lem16  10148  ackbij1b  10152  ackbij2  10156  sornom  10191  infpssrlem4  10220  infpssrlem5  10221  fin23lem26  10239  fin23lem23  10240  isf32lem2  10268  isf32lem3  10269  isf32lem4  10270  domtriomlem  10356  axdc3lem2  10365  axdc3lem4  10367  canthp1lem2  10568  elni2  10792  piord  10795  addnidpi  10816  indpi  10822  om2uzf1oi  13880  fzennn  13895  hashp1i  14330  om2noseqf1o  28301  bnj529  34899  bnj1098  34941  bnj570  35063  bnj594  35070  bnj580  35071  bnj967  35103  bnj1001  35117  bnj1053  35134  bnj1071  35135  fineqvnttrclselem2  35280  fineqvnttrclselem3  35281  nnuni  35923  hfun  36374  finminlem  36514  finxpsuclem  37604  finxpsuc  37605  wepwso  43352  dflim5  43638