Theorem omelon 9611

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

Syntax hints:   ∈ wcel 2149  Vcvv 3463  Oncon0 6357  ωcom 7858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402  ax-un 7730  ax-inf2 9606

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-tr 5220  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-om 7859

This theorem is referenced by:  oancom  9616  cnfcomlem  9664  cnfcom  9665  cnfcom2lem  9666  cnfcom2  9667  cnfcom3lem  9668  cnfcom3  9669  cnfcom3clem  9670  cardom  9968  infxpenlem  9993  xpomen  9995  infxpidm2  9997  infxpenc  9998  infxpenc2lem1  9999  infxpenc2  10002  alephon  10049  infenaleph  10071  iunfictbso  10094  dfac12k  10127  infunsdom1  10191  domtriomlem  10422  iunctb  10555  pwcfsdom  10564  canthp1lem2  10634  pwfseqlem4a  10642  pwfseqlem4  10643  pwfseqlem5  10644  wunex3  10722  znnen  16264  qnnen  16265  cygctb  19958  2ndcctbss  23577  2ndcomap  23580  2ndcsep  23581  tx1stc  23772  tx2ndc  23773  met1stc  24643  met2ndci  24644  re2ndc  24923  uniiccdif  25702  dyadmbl  25724  opnmblALT  25727  mbfimaopnlem  25779  aannenlem3  26456  dfz12s2  28643  exrecfnlem  37908  poimirlem32  38186  numinfctb  43715  onexomgt  43853  onexlimgt  43855  onexoegt  43856  1oaomeqom  43905  oaabsb  43906  oaordnrex  43907  oaordnr  43908  2omomeqom  43915  omnord1ex  43916  omnord1  43917  nnoeomeqom  43924  oenord1  43928  oaomoencom  43929  cantnftermord  43932  cantnfub  43933  cantnf2  43937  nnawordexg  43939  dflim5  43941  oacl2g  43942  onmcl  43943  omabs2  43944  omcl2  43945  tfsnfin  43964  ofoaf  43967  ofoafo  43968  naddcnff  43974  naddcnffo  43976  naddcnfcom  43978  naddcnfid1  43979  naddcnfid2  43980  naddcnfass  43981  naddwordnexlem0  44008  naddwordnexlem1  44009  naddwordnexlem3  44011  oawordex3  44012  naddwordnexlem4  44013  infordmin  44143  minregex  44145  omiscard  44154  sucomisnotcard  44155  aleph1min  44168  alephiso3  44170  wfaxinf2  45595