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

Theorem nnon 7575
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 7573 . 2 ω ⊆ On
21sseli 3960 1 (𝐴 ∈ ω → 𝐴 ∈ On)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  Oncon0 6184  ωcom 7569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-tr 5164  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-om 7570
This theorem is referenced by:  nnoni  7576  nnord  7577  peano4  7593  findsg  7598  onasuc  8142  onmsuc  8143  nna0  8219  nnm0  8220  nnasuc  8221  nnmsuc  8222  nnesuc  8223  nnecl  8228  nnawordi  8236  nnmword  8248  nnawordex  8252  nnaordex  8253  oaabslem  8259  oaabs  8260  oaabs2  8261  omabslem  8262  omabs  8263  nnneo  8267  nneob  8268  onfin2  8698  findcard3  8749  dffi3  8883  card2inf  9007  elom3  9099  cantnfp1lem3  9131  cnfcomlem  9150  cnfcom  9151  cnfcom3  9155  finnum  9365  cardnn  9380  nnsdomel  9407  nnadju  9611  ficardun2  9613  ackbij1lem15  9644  ackbij2lem2  9650  ackbij2lem3  9651  ackbij2  9653  fin23lem22  9737  isf32lem5  9767  fin1a2lem4  9813  fin1a2lem9  9818  pwfseqlem3  10070  winainflem  10103  wunr1om  10129  tskr1om  10177  grothomex  10239  pion  10289  om2uzlt2i  13307  bnj168  31899  satfvsuc  32505  satf0suc  32520  sat1el2xp  32523  fmlasuc0  32528  elhf2  33533  findreccl  33698  rdgeqoa  34533  exrecfnlem  34542  finxpreclem4  34557  finxpreclem6  34559  harinf  39509  harsucnn  39781
  Copyright terms: Public domain W3C validator