Theorem omelon 9567

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

Step	Hyp	Ref	Expression
1		omex 9564	. 2 ⊢ ω ∈ V
2		omelon2 7830	. 2 ⊢ (ω ∈ V → ω ∈ On)
3	1, 2	ax-mp 5	1 ⊢ ω ∈ On

Syntax hints:   ∈ wcel 2114  Vcvv 3430  Oncon0 6324  ωcom 7817

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5376  ax-un 7689  ax-inf2 9562

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6327  df-on 6328  df-lim 6329  df-suc 6330  df-om 7818

This theorem is referenced by:  oancom  9572  cnfcomlem  9620  cnfcom  9621  cnfcom2lem  9622  cnfcom2  9623  cnfcom3lem  9624  cnfcom3  9625  cnfcom3clem  9626  cardom  9910  infxpenlem  9935  xpomen  9937  infxpidm2  9939  infxpenc  9940  infxpenc2lem1  9941  infxpenc2  9944  alephon  9991  infenaleph  10013  iunfictbso  10036  dfac12k  10070  infunsdom1  10134  domtriomlem  10364  iunctb  10497  pwcfsdom  10506  canthp1lem2  10576  pwfseqlem4a  10584  pwfseqlem4  10585  pwfseqlem5  10586  wunex3  10664  znnen  16179  qnnen  16180  cygctb  19867  2ndcctbss  23420  2ndcomap  23423  2ndcsep  23424  tx1stc  23615  tx2ndc  23616  met1stc  24486  met2ndci  24487  re2ndc  24766  uniiccdif  25545  dyadmbl  25567  opnmblALT  25570  mbfimaopnlem  25622  aannenlem3  26296  dfz12s2  28480  exrecfnlem  37695  poimirlem32  37973  numinfctb  43531  onexomgt  43669  onexlimgt  43671  onexoegt  43672  1oaomeqom  43721  oaabsb  43722  oaordnrex  43723  oaordnr  43724  2omomeqom  43731  omnord1ex  43732  omnord1  43733  nnoeomeqom  43740  oenord1  43744  oaomoencom  43745  cantnftermord  43748  cantnfub  43749  cantnf2  43753  nnawordexg  43755  dflim5  43757  oacl2g  43758  onmcl  43759  omabs2  43760  omcl2  43761  tfsnfin  43780  ofoaf  43783  ofoafo  43784  naddcnff  43790  naddcnffo  43792  naddcnfcom  43794  naddcnfid1  43795  naddcnfid2  43796  naddcnfass  43797  naddwordnexlem0  43824  naddwordnexlem1  43825  naddwordnexlem3  43827  oawordex3  43828  naddwordnexlem4  43829  infordmin  43959  minregex  43961  omiscard  43970  sucomisnotcard  43971  aleph1min  43984  alephiso3  43986  wfaxinf2  45428