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

Theorem nnon 7813
Description: A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.)
Assertion
Ref Expression
nnon (𝐴 ∈ ω → 𝐴 ∈ On)

Proof of Theorem nnon
StepHypRef Expression
1 omsson 7811 . 2 ω ⊆ On
21sseli 3945 1 (𝐴 ∈ ω → 𝐴 ∈ On)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Oncon0 6322  ωcom 7807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-v 3450  df-in 3922  df-ss 3932  df-om 7808
This theorem is referenced by:  nnoni  7814  nnord  7815  peano4  7834  findsg  7841  onasuc  8479  onmsuc  8480  nna0  8556  nnm0  8557  nnasuc  8558  nnmsuc  8559  nnesuc  8560  nnecl  8565  nnawordi  8573  nnmword  8585  nnawordex  8589  nnaordex  8590  oaabslem  8598  oaabs  8599  oaabs2  8600  omabslem  8601  omabs  8602  nnneo  8606  nneob  8607  dif1ennn  9112  findcard2  9115  onfin2  9182  nndomo  9184  findcard3  9236  findcard3OLD  9237  dffi3  9374  card2inf  9498  elom3  9591  cantnfp1lem3  9623  cnfcomlem  9642  cnfcom  9643  cnfcom3  9647  ttrcltr  9659  ttrclselem1  9668  ttrclselem2  9669  finnum  9891  cardnn  9906  nnsdomel  9933  harsucnn  9941  nnadjuALT  10141  ficardun2  10145  ficardun2OLD  10146  ackbij1lem15  10177  ackbij2lem2  10183  ackbij2lem3  10184  ackbij2  10186  fin23lem22  10270  isf32lem5  10300  fin1a2lem4  10346  fin1a2lem9  10351  pwfseqlem3  10603  winainflem  10636  wunr1om  10662  tskr1om  10710  grothomex  10772  pion  10822  om2uzlt2i  13863  bnj168  33382  satfvsuc  33995  satf0suc  34010  sat1el2xp  34013  fmlasuc0  34018  elhf2  34789  findreccl  34954  rdgeqoa  35870  exrecfnlem  35879  finxpreclem4  35894  finxpreclem6  35896  harinf  41387  onexoegt  41607  oaabsb  41658  nnoeomeqom  41676  cantnfub  41685  dflim5  41693  onmcl  41695  omabs2  41696  naddcnffo  41709  naddonnn  41741  naddwordnexlem0  41742  naddwordnexlem3  41745  oawordex3  41746  naddwordnexlem4  41747  omssrncard  41886  nna1iscard  41891
  Copyright terms: Public domain W3C validator