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

Theorem nnon 6690
Description: A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.)
Assertion
Ref Expression
nnon  |-  ( A  e.  om  ->  A  e.  On )

Proof of Theorem nnon
StepHypRef Expression
1 omsson 6688 . 2  |-  om  C_  On
21sseli 3500 1  |-  ( A  e.  om  ->  A  e.  On )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   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:  nnoni  6691  nnord  6692  peano4  6706  findsg  6711  onasuc  7178  onmsuc  7179  nna0  7253  nnm0  7254  nnasuc  7255  nnmsuc  7256  nnesuc  7257  nnecl  7262  nnawordi  7270  nnmword  7282  nnawordex  7286  nnaordex  7287  oaabslem  7292  oaabs  7293  oaabs2  7294  omabslem  7295  omabs  7296  nnneo  7300  nneob  7301  onfin2  7709  findcard3  7763  dffi3  7891  card2inf  7981  elom3  8065  cantnfp1lem3  8099  cantnfp1lem3OLD  8125  cnfcomlem  8143  cnfcom  8144  cnfcom3  8148  cnfcomlemOLD  8151  cnfcomOLD  8152  cnfcom3OLD  8156  finnum  8329  cardnn  8344  nnsdomel  8371  nnacda  8581  ficardun2  8583  ackbij1lem15  8614  ackbij2lem2  8620  ackbij2lem3  8621  ackbij2  8623  fin23lem22  8707  isf32lem5  8737  fin1a2lem4  8783  fin1a2lem9  8788  pwfseqlem3  9038  winainflem  9071  wunr1om  9097  tskr1om  9145  grothomex  9207  pion  9257  om2uzlt2i  12030  elhf2  29437  findreccl  29523  harinf  30608  bnj168  32883
  Copyright terms: Public domain W3C validator