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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  Oncon0 6315  ωcom 7808

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 5231  ax-nul 5241  ax-pr 5368  ax-un 7680  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 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 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-om 7809

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  16138  qnnen  16139  cygctb  19825  2ndcctbss  23398  2ndcomap  23401  2ndcsep  23402  tx1stc  23593  tx2ndc  23594  met1stc  24464  met2ndci  24465  re2ndc  24744  uniiccdif  25523  dyadmbl  25545  opnmblALT  25548  mbfimaopnlem  25600  aannenlem3  26278  dfz12s2  28468  exrecfnlem  37691  poimirlem32  37964  numinfctb  43534  onexomgt  43672  onexlimgt  43674  onexoegt  43675  1oaomeqom  43724  oaabsb  43725  oaordnrex  43726  oaordnr  43727  2omomeqom  43734  omnord1ex  43735  omnord1  43736  nnoeomeqom  43743  oenord1  43747  oaomoencom  43748  cantnftermord  43751  cantnfub  43752  cantnf2  43756  nnawordexg  43758  dflim5  43760  oacl2g  43761  onmcl  43762  omabs2  43763  omcl2  43764  tfsnfin  43783  ofoaf  43786  ofoafo  43787  naddcnff  43793  naddcnffo  43795  naddcnfcom  43797  naddcnfid1  43798  naddcnfid2  43799  naddcnfass  43800  naddwordnexlem0  43827  naddwordnexlem1  43828  naddwordnexlem3  43830  oawordex3  43831  naddwordnexlem4  43832  infordmin  43962  minregex  43964  omiscard  43973  sucomisnotcard  43974  aleph1min  43987  alephiso3  43989  wfaxinf2  45431