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

Theorem omelon 9590
Description: Omega is an ordinal number. Theorem 1.22 of [Schloeder] p. 3. (Contributed by NM, 10-May-1998.) (Revised by Mario Carneiro, 30-Jan-2013.)
Assertion
Ref Expression
omelon ω ∈ On

Proof of Theorem omelon
StepHypRef Expression
1 omex 9587 . 2 ω ∈ V
2 omelon2 7819 . 2 (ω ∈ V → ω ∈ On)
31, 2ax-mp 5 1 ω ∈ On
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3447  Oncon0 6321  ωcom 7806
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 2704  ax-sep 5260  ax-nul 5267  ax-pr 5388  ax-un 7676  ax-inf2 9585
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-opab 5172  df-tr 5227  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-we 5594  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-om 7807
This theorem is referenced by:  oancom  9595  cnfcomlem  9643  cnfcom  9644  cnfcom2lem  9645  cnfcom2  9646  cnfcom3lem  9647  cnfcom3  9648  cnfcom3clem  9649  cardom  9930  infxpenlem  9957  xpomen  9959  infxpidm2  9961  infxpenc  9962  infxpenc2lem1  9963  infxpenc2  9966  alephon  10013  infenaleph  10035  iunfictbso  10058  dfac12k  10091  infunsdom1  10157  domtriomlem  10386  iunctb  10518  pwcfsdom  10527  canthp1lem2  10597  pwfseqlem4a  10605  pwfseqlem4  10606  pwfseqlem5  10607  wunex3  10685  znnen  16102  qnnen  16103  cygctb  19677  2ndcctbss  22829  2ndcomap  22832  2ndcsep  22833  tx1stc  23024  tx2ndc  23025  met1stc  23900  met2ndci  23901  re2ndc  24187  uniiccdif  24965  dyadmbl  24987  opnmblALT  24990  mbfimaopnlem  25042  aannenlem3  25713  exrecfnlem  35900  poimirlem32  36160  numinfctb  41477  onexomgt  41622  onexlimgt  41624  onexoegt  41625  1oaomeqom  41675  oaabsb  41676  oaordnrex  41677  oaordnr  41678  2omomeqom  41685  omnord1ex  41686  omnord1  41687  nnoeomeqom  41694  oenord1  41698  oaomoencom  41699  cantnftermord  41702  cantnfub  41703  cantnf2  41707  nnawordexg  41709  dflim5  41711  oacl2g  41712  onmcl  41713  omabs2  41714  omcl2  41715  ofoaf  41718  ofoafo  41719  naddcnff  41725  naddcnffo  41727  naddcnfcom  41729  naddcnfid1  41730  naddcnfid2  41731  naddcnfass  41732  naddwordnexlem0  41760  naddwordnexlem1  41761  naddwordnexlem3  41763  oawordex3  41764  naddwordnexlem4  41765  infordmin  41896  minregex  41898  omiscard  41907  sucomisnotcard  41908  aleph1min  41921  alephiso3  41923
  Copyright terms: Public domain W3C validator