Theorem omelon 9556

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

Syntax hints:   ∈ wcel 2114  Vcvv 3427  Oncon0 6312  ωcom 7806

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 2707  ax-sep 5220  ax-nul 5230  ax-pr 5364  ax-un 7678  ax-inf2 9551

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 2714  df-cleq 2727  df-clel 2810  df-ne 2931  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-tr 5182  df-eprel 5520  df-po 5528  df-so 5529  df-fr 5573  df-we 5575  df-ord 6315  df-on 6316  df-lim 6317  df-suc 6318  df-om 7807

This theorem is referenced by:  oancom  9561  cnfcomlem  9609  cnfcom  9610  cnfcom2lem  9611  cnfcom2  9612  cnfcom3lem  9613  cnfcom3  9614  cnfcom3clem  9615  cardom  9899  infxpenlem  9924  xpomen  9926  infxpidm2  9928  infxpenc  9929  infxpenc2lem1  9930  infxpenc2  9933  alephon  9980  infenaleph  10002  iunfictbso  10025  dfac12k  10059  infunsdom1  10123  domtriomlem  10353  iunctb  10486  pwcfsdom  10495  canthp1lem2  10565  pwfseqlem4a  10573  pwfseqlem4  10574  pwfseqlem5  10575  wunex3  10653  znnen  16168  qnnen  16169  cygctb  19856  2ndcctbss  23408  2ndcomap  23411  2ndcsep  23412  tx1stc  23603  tx2ndc  23604  met1stc  24474  met2ndci  24475  re2ndc  24754  uniiccdif  25533  dyadmbl  25555  opnmblALT  25558  mbfimaopnlem  25610  aannenlem3  26284  dfz12s2  28468  exrecfnlem  37683  poimirlem32  37961  numinfctb  43519  onexomgt  43657  onexlimgt  43659  onexoegt  43660  1oaomeqom  43709  oaabsb  43710  oaordnrex  43711  oaordnr  43712  2omomeqom  43719  omnord1ex  43720  omnord1  43721  nnoeomeqom  43728  oenord1  43732  oaomoencom  43733  cantnftermord  43736  cantnfub  43737  cantnf2  43741  nnawordexg  43743  dflim5  43745  oacl2g  43746  onmcl  43747  omabs2  43748  omcl2  43749  tfsnfin  43768  ofoaf  43771  ofoafo  43772  naddcnff  43778  naddcnffo  43780  naddcnfcom  43782  naddcnfid1  43783  naddcnfid2  43784  naddcnfass  43785  naddwordnexlem0  43812  naddwordnexlem1  43813  naddwordnexlem3  43815  oawordex3  43816  naddwordnexlem4  43817  infordmin  43947  minregex  43949  omiscard  43958  sucomisnotcard  43959  aleph1min  43972  alephiso3  43974  wfaxinf2  45416