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

Theorem nnon 6703
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 6701 . 2  |-  om  C_  On
21sseli 3457 1  |-  ( A  e.  om  ->  A  e.  On )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1867   Oncon0 5433   omcom 6697
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pr 4652  ax-un 6588
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-sbc 3297  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-tr 4512  df-eprel 4756  df-po 4766  df-so 4767  df-fr 4804  df-we 4806  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-om 6698
This theorem is referenced by:  nnoni  6704  nnord  6705  peano4  6720  findsg  6725  onasuc  7229  onmsuc  7230  nna0  7304  nnm0  7305  nnasuc  7306  nnmsuc  7307  nnesuc  7308  nnecl  7313  nnawordi  7321  nnmword  7333  nnawordex  7337  nnaordex  7338  oaabslem  7343  oaabs  7344  oaabs2  7345  omabslem  7346  omabs  7347  nnneo  7351  nneob  7352  onfin2  7761  findcard3  7811  dffi3  7942  card2inf  8061  elom3  8144  cantnfp1lem3  8175  cnfcomlem  8194  cnfcom  8195  cnfcom3  8199  finnum  8372  cardnn  8387  nnsdomel  8414  nnacda  8620  ficardun2  8622  ackbij1lem15  8653  ackbij2lem2  8659  ackbij2lem3  8660  ackbij2  8662  fin23lem22  8746  isf32lem5  8776  fin1a2lem4  8822  fin1a2lem9  8827  pwfseqlem3  9074  winainflem  9107  wunr1om  9133  tskr1om  9181  grothomex  9243  pion  9293  om2uzlt2i  12151  bnj168  29352  elhf2  30753  findreccl  30924  harinf  35628
  Copyright terms: Public domain W3C validator