MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnord Structured version   Visualization version   GIF version

Theorem nnord 7027
Description: A natural number is ordinal. (Contributed by NM, 17-Oct-1995.)
Assertion
Ref Expression
nnord (𝐴 ∈ ω → Ord 𝐴)

Proof of Theorem nnord
StepHypRef Expression
1 nnon 7025 . 2 (𝐴 ∈ ω → 𝐴 ∈ On)
2 eloni 5697 . 2 (𝐴 ∈ On → Ord 𝐴)
31, 2syl 17 1 (𝐴 ∈ ω → Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  Ord word 5686  Oncon0 5687  ωcom 7019
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-tr 4718  df-eprel 4990  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-om 7020
This theorem is referenced by:  nnlim  7032  nnsuc  7036  nnaordi  7650  nnaord  7651  nnaword  7659  nnmord  7664  nnmwordi  7667  nnawordex  7669  omsmo  7686  phplem1  8091  phplem2  8092  phplem3  8093  phplem4  8094  php  8096  php4  8099  nndomo  8106  ominf  8124  isinf  8125  pssnn  8130  dif1en  8145  unblem1  8164  isfinite2  8170  unfilem1  8176  inf3lem5  8481  inf3lem6  8482  cantnfp1lem2  8528  cantnfp1lem3  8529  dif1card  8785  pwsdompw  8978  ackbij1lem5  8998  ackbij1lem14  9007  ackbij1lem16  9009  ackbij1b  9013  ackbij2  9017  sornom  9051  infpssrlem4  9080  infpssrlem5  9081  fin23lem26  9099  fin23lem23  9100  isf32lem2  9128  isf32lem3  9129  isf32lem4  9130  domtriomlem  9216  axdc3lem2  9225  axdc3lem4  9227  canthp1lem2  9427  elni2  9651  piord  9654  addnidpi  9675  indpi  9681  om2uzf1oi  12700  fzennn  12715  hashp1i  13139  bnj529  30554  bnj1098  30597  bnj570  30718  bnj594  30725  bnj580  30726  bnj967  30758  bnj1001  30771  bnj1053  30787  bnj1071  30788  hfun  31962  finminlem  31989  finxpsuclem  32901  finxpsuc  32902  wepwso  37128
  Copyright terms: Public domain W3C validator