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

Theorem nnord 6681
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 6679 . 2  |-  ( A  e.  om  ->  A  e.  On )
2 eloni 4877 . 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 1823   Ord word 4866   Oncon0 4867   omcom 6673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-tr 4533  df-eprel 4780  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-om 6674
This theorem is referenced by:  nnlim  6686  nnsuc  6690  nnaordi  7259  nnaord  7260  nnaword  7268  nnmord  7273  nnmwordi  7276  nnawordex  7278  omsmo  7295  phplem1  7689  phplem2  7690  phplem3  7691  phplem4  7692  php  7694  php4  7697  nndomo  7704  omsucdomOLD  7706  ominf  7725  isinf  7726  pssnn  7731  dif1en  7745  unblem1  7764  isfinite2  7770  unfilem1  7776  inf3lem5  8040  inf3lem6  8041  cantnfp1lem2  8089  cantnfp1lem3  8090  cantnfp1lem2OLD  8115  cantnfp1lem3OLD  8116  dif1card  8379  pwsdompw  8575  ackbij1lem5  8595  ackbij1lem14  8604  ackbij1lem16  8606  ackbij1b  8610  ackbij2  8614  sornom  8648  infpssrlem4  8677  infpssrlem5  8678  fin23lem26  8696  fin23lem23  8697  isf32lem2  8725  isf32lem3  8726  isf32lem4  8727  domtriomlem  8813  axdc3lem2  8822  axdc3lem4  8824  canthp1lem2  9020  elni2  9244  piord  9247  addnidpi  9268  indpi  9274  om2uzf1oi  12046  fzennn  12060  hashp1i  12452  hfun  30063  finminlem  30376  wepwso  31227  bnj529  34199  bnj1098  34243  bnj570  34364  bnj594  34371  bnj580  34372  bnj967  34404  bnj1001  34417  bnj1053  34433  bnj1071  34434
  Copyright terms: Public domain W3C validator