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

Theorem nnord 6692
Description: A natural number is ordinal. (Contributed by NM, 17-Oct-1995.)
Assertion
Ref Expression
nnord  |-  ( A  e.  om  ->  Ord  A )

Proof of Theorem nnord
StepHypRef Expression
1 nnon 6690 . 2  |-  ( A  e.  om  ->  A  e.  On )
2 eloni 4888 . 2  |-  ( A  e.  On  ->  Ord  A )
31, 2syl 16 1  |-  ( A  e.  om  ->  Ord  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   Ord word 4877   Oncon0 4878   omcom 6684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686  ax-un 6576
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-tr 4541  df-eprel 4791  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-om 6685
This theorem is referenced by:  nnlim  6697  nnsuc  6701  nnaordi  7267  nnaord  7268  nnaword  7276  nnmord  7281  nnmwordi  7284  nnawordex  7286  omsmo  7303  phplem1  7696  phplem2  7697  phplem3  7698  phplem4  7699  php  7701  php4  7704  nndomo  7711  omsucdomOLD  7713  ominf  7732  isinf  7733  pssnn  7738  dif1enOLD  7752  dif1en  7753  unblem1  7772  isfinite2  7778  unfilem1  7784  inf3lem5  8049  inf3lem6  8050  cantnfp1lem2  8098  cantnfp1lem3  8099  cantnfp1lem2OLD  8124  cantnfp1lem3OLD  8125  dif1card  8388  pwsdompw  8584  ackbij1lem5  8604  ackbij1lem14  8613  ackbij1lem16  8615  ackbij1b  8619  ackbij2  8623  sornom  8657  infpssrlem4  8686  infpssrlem5  8687  fin23lem26  8705  fin23lem23  8706  isf32lem2  8734  isf32lem3  8735  isf32lem4  8736  domtriomlem  8822  axdc3lem2  8831  axdc3lem4  8833  canthp1lem2  9031  elni2  9255  piord  9258  addnidpi  9279  indpi  9285  om2uzf1oi  12032  fzennn  12046  hashp1i  12434  hfun  29440  finminlem  29741  wepwso  30620  bnj529  32895  bnj1098  32939  bnj570  33060  bnj594  33067  bnj580  33068  bnj967  33100  bnj1001  33113  bnj1053  33129  bnj1071  33130
  Copyright terms: Public domain W3C validator