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

Theorem nnord 7577
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 7575 . 2 (𝐴 ∈ ω → 𝐴 ∈ On)
2 eloni 6194 . 2 (𝐴 ∈ On → Ord 𝐴)
31, 2syl 17 1 (𝐴 ∈ ω → Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  Ord word 6183  Oncon0 6184  ωcom 7569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-tr 5164  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-om 7570
This theorem is referenced by:  nnlim  7582  nnsuc  7586  omsucne  7587  nnaordi  8233  nnaord  8234  nnaword  8242  nnmord  8247  nnmwordi  8250  nnawordex  8252  omsmo  8270  phplem1  8684  phplem2  8685  phplem3  8686  phplem4  8687  php  8689  php4  8692  nndomo  8700  ominf  8718  isinf  8719  pssnn  8724  dif1en  8739  unblem1  8758  isfinite2  8764  unfilem1  8770  inf3lem5  9083  inf3lem6  9084  cantnfp1lem2  9130  cantnfp1lem3  9131  dif1card  9424  pwsdompw  9614  ackbij1lem5  9634  ackbij1lem14  9643  ackbij1lem16  9645  ackbij1b  9649  ackbij2  9653  sornom  9687  infpssrlem4  9716  infpssrlem5  9717  fin23lem26  9735  fin23lem23  9736  isf32lem2  9764  isf32lem3  9765  isf32lem4  9766  domtriomlem  9852  axdc3lem2  9861  axdc3lem4  9863  canthp1lem2  10063  elni2  10287  piord  10290  addnidpi  10311  indpi  10317  om2uzf1oi  13309  fzennn  13324  hashp1i  13752  bnj529  31911  bnj1098  31954  bnj570  32076  bnj594  32083  bnj580  32084  bnj967  32116  bnj1001  32129  bnj1053  32145  bnj1071  32146  hfun  33536  finminlem  33563  finxpsuclem  34560  finxpsuc  34561  wepwso  39521  nndomog  39775
  Copyright terms: Public domain W3C validator