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

Theorem nnon 6487
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 6485 . 2  |-  om  C_  On
21sseli 3357 1  |-  ( A  e.  om  ->  A  e.  On )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   Oncon0 4724   omcom 6481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pr 4536  ax-un 6377
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-sbc 3192  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-pss 3349  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-tp 3887  df-op 3889  df-uni 4097  df-br 4298  df-opab 4356  df-tr 4391  df-eprel 4637  df-po 4646  df-so 4647  df-fr 4684  df-we 4686  df-ord 4727  df-on 4728  df-lim 4729  df-suc 4730  df-om 6482
This theorem is referenced by:  nnoni  6488  nnord  6489  peano4  6503  findsg  6508  onasuc  6973  onmsuc  6974  nna0  7048  nnm0  7049  nnasuc  7050  nnmsuc  7051  nnesuc  7052  nnecl  7057  nnawordi  7065  nnmword  7077  nnawordex  7081  nnaordex  7082  oaabslem  7087  oaabs  7088  oaabs2  7089  omabslem  7090  omabs  7091  nnneo  7095  nneob  7096  onfin2  7507  findcard3  7560  dffi3  7686  card2inf  7775  elom3  7859  cantnfp1lem3  7893  cantnfp1lem3OLD  7919  cnfcomlem  7937  cnfcom  7938  cnfcom3  7942  cnfcomlemOLD  7945  cnfcomOLD  7946  cnfcom3OLD  7950  finnum  8123  cardnn  8138  nnsdomel  8165  nnacda  8375  ficardun2  8377  ackbij1lem15  8408  ackbij2lem2  8414  ackbij2lem3  8415  ackbij2  8417  fin23lem22  8501  isf32lem5  8531  fin1a2lem4  8577  fin1a2lem9  8582  pwfseqlem3  8832  winainflem  8865  wunr1om  8891  tskr1om  8939  grothomex  9001  pion  9053  om2uzlt2i  11779  elhf2  28218  findreccl  28304  harinf  29388  bnj168  31726
  Copyright terms: Public domain W3C validator