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

Theorem nnord 7223
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 7221 . 2 (𝐴 ∈ ω → 𝐴 ∈ On)
2 eloni 5875 . 2 (𝐴 ∈ On → Ord 𝐴)
31, 2syl 17 1 (𝐴 ∈ ω → Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145  Ord word 5864  Oncon0 5865  ωcom 7215
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pr 5035  ax-un 7099
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-tr 4888  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-om 7216
This theorem is referenced by:  nnlim  7228  nnsuc  7232  nnaordi  7855  nnaord  7856  nnaword  7864  nnmord  7869  nnmwordi  7872  nnawordex  7874  omsmo  7891  phplem1  8298  phplem2  8299  phplem3  8300  phplem4  8301  php  8303  php4  8306  nndomo  8313  ominf  8331  isinf  8332  pssnn  8337  dif1en  8352  unblem1  8371  isfinite2  8377  unfilem1  8383  inf3lem5  8696  inf3lem6  8697  cantnfp1lem2  8743  cantnfp1lem3  8744  dif1card  9036  pwsdompw  9231  ackbij1lem5  9251  ackbij1lem14  9260  ackbij1lem16  9262  ackbij1b  9266  ackbij2  9270  sornom  9304  infpssrlem4  9333  infpssrlem5  9334  fin23lem26  9352  fin23lem23  9353  isf32lem2  9381  isf32lem3  9382  isf32lem4  9383  domtriomlem  9469  axdc3lem2  9478  axdc3lem4  9480  canthp1lem2  9680  elni2  9904  piord  9907  addnidpi  9928  indpi  9934  om2uzf1oi  12959  fzennn  12974  hashp1i  13392  bnj529  31148  bnj1098  31191  bnj570  31312  bnj594  31319  bnj580  31320  bnj967  31352  bnj1001  31365  bnj1053  31381  bnj1071  31382  hfun  32621  finminlem  32648  finxpsuclem  33570  finxpsuc  33571  wepwso  38139
  Copyright terms: Public domain W3C validator