Theorem omelon 9671

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 9668	. 2 ⊢ ω ∈ V
2		omelon2 7884	. 2 ⊢ (ω ∈ V → ω ∈ On)
3	1, 2	ax-mp 5	1 ⊢ ω ∈ On

Syntax hints:   ∈ wcel 2098  Vcvv 3461  Oncon0 6371  ωcom 7871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429  ax-un 7741  ax-inf2 9666

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-om 7872

This theorem is referenced by:  oancom  9676  cnfcomlem  9724  cnfcom  9725  cnfcom2lem  9726  cnfcom2  9727  cnfcom3lem  9728  cnfcom3  9729  cnfcom3clem  9730  cardom  10011  infxpenlem  10038  xpomen  10040  infxpidm2  10042  infxpenc  10043  infxpenc2lem1  10044  infxpenc2  10047  alephon  10094  infenaleph  10116  iunfictbso  10139  dfac12k  10172  infunsdom1  10238  domtriomlem  10467  iunctb  10599  pwcfsdom  10608  canthp1lem2  10678  pwfseqlem4a  10686  pwfseqlem4  10687  pwfseqlem5  10688  wunex3  10766  znnen  16192  qnnen  16193  cygctb  19859  2ndcctbss  23403  2ndcomap  23406  2ndcsep  23407  tx1stc  23598  tx2ndc  23599  met1stc  24474  met2ndci  24475  re2ndc  24761  uniiccdif  25551  dyadmbl  25573  opnmblALT  25576  mbfimaopnlem  25628  aannenlem3  26310  n0ssold  28270  exrecfnlem  36989  poimirlem32  37256  numinfctb  42669  onexomgt  42811  onexlimgt  42813  onexoegt  42814  1oaomeqom  42864  oaabsb  42865  oaordnrex  42866  oaordnr  42867  2omomeqom  42874  omnord1ex  42875  omnord1  42876  nnoeomeqom  42883  oenord1  42887  oaomoencom  42888  cantnftermord  42891  cantnfub  42892  cantnf2  42896  nnawordexg  42898  dflim5  42900  oacl2g  42901  onmcl  42902  omabs2  42903  omcl2  42904  tfsnfin  42923  ofoaf  42926  ofoafo  42927  naddcnff  42933  naddcnffo  42935  naddcnfcom  42937  naddcnfid1  42938  naddcnfid2  42939  naddcnfass  42940  naddwordnexlem0  42968  naddwordnexlem1  42969  naddwordnexlem3  42971  oawordex3  42972  naddwordnexlem4  42973  infordmin  43104  minregex  43106  omiscard  43115  sucomisnotcard  43116  aleph1min  43129  alephiso3  43131