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

Theorem nnon 7570
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 7568 . 2 ω ⊆ On
21sseli 3914 1 (𝐴 ∈ ω → 𝐴 ∈ On)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  Oncon0 6163  ωcom 7564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-tr 5140  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-om 7565
This theorem is referenced by:  nnoni  7571  nnord  7572  peano4  7588  findsg  7594  onasuc  8140  onmsuc  8141  nna0  8217  nnm0  8218  nnasuc  8219  nnmsuc  8220  nnesuc  8221  nnecl  8226  nnawordi  8234  nnmword  8246  nnawordex  8250  nnaordex  8251  oaabslem  8257  oaabs  8258  oaabs2  8259  omabslem  8260  omabs  8261  nnneo  8265  nneob  8266  onfin2  8699  nndomo  8701  findcard3  8749  dffi3  8883  card2inf  9007  elom3  9099  cantnfp1lem3  9131  cnfcomlem  9150  cnfcom  9151  cnfcom3  9155  finnum  9365  cardnn  9380  nnsdomel  9407  harsucnn  9415  nnadjuALT  9613  ficardun2  9617  ficardun2OLD  9618  ackbij1lem15  9649  ackbij2lem2  9655  ackbij2lem3  9656  ackbij2  9658  fin23lem22  9742  isf32lem5  9772  fin1a2lem4  9818  fin1a2lem9  9823  pwfseqlem3  10075  winainflem  10108  wunr1om  10134  tskr1om  10182  grothomex  10244  pion  10294  om2uzlt2i  13318  bnj168  32114  satfvsuc  32722  satf0suc  32737  sat1el2xp  32740  fmlasuc0  32745  elhf2  33750  findreccl  33915  rdgeqoa  34788  exrecfnlem  34797  finxpreclem4  34812  finxpreclem6  34814  harinf  39968
  Copyright terms: Public domain W3C validator