Theorem omelon 9640

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

Syntax hints:   ∈ wcel 2106  Vcvv 3474  Oncon0 6364  ωcom 7854

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7724  ax-inf2 9635

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-om 7855

This theorem is referenced by:  oancom  9645  cnfcomlem  9693  cnfcom  9694  cnfcom2lem  9695  cnfcom2  9696  cnfcom3lem  9697  cnfcom3  9698  cnfcom3clem  9699  cardom  9980  infxpenlem  10007  xpomen  10009  infxpidm2  10011  infxpenc  10012  infxpenc2lem1  10013  infxpenc2  10016  alephon  10063  infenaleph  10085  iunfictbso  10108  dfac12k  10141  infunsdom1  10207  domtriomlem  10436  iunctb  10568  pwcfsdom  10577  canthp1lem2  10647  pwfseqlem4a  10655  pwfseqlem4  10656  pwfseqlem5  10657  wunex3  10735  znnen  16154  qnnen  16155  cygctb  19759  2ndcctbss  22958  2ndcomap  22961  2ndcsep  22962  tx1stc  23153  tx2ndc  23154  met1stc  24029  met2ndci  24030  re2ndc  24316  uniiccdif  25094  dyadmbl  25116  opnmblALT  25119  mbfimaopnlem  25171  aannenlem3  25842  exrecfnlem  36255  poimirlem32  36515  numinfctb  41835  onexomgt  41980  onexlimgt  41982  onexoegt  41983  1oaomeqom  42033  oaabsb  42034  oaordnrex  42035  oaordnr  42036  2omomeqom  42043  omnord1ex  42044  omnord1  42045  nnoeomeqom  42052  oenord1  42056  oaomoencom  42057  cantnftermord  42060  cantnfub  42061  cantnf2  42065  nnawordexg  42067  dflim5  42069  oacl2g  42070  onmcl  42071  omabs2  42072  omcl2  42073  tfsnfin  42092  ofoaf  42095  ofoafo  42096  naddcnff  42102  naddcnffo  42104  naddcnfcom  42106  naddcnfid1  42107  naddcnfid2  42108  naddcnfass  42109  naddwordnexlem0  42137  naddwordnexlem1  42138  naddwordnexlem3  42140  oawordex3  42141  naddwordnexlem4  42142  infordmin  42273  minregex  42275  omiscard  42284  sucomisnotcard  42285  aleph1min  42298  alephiso3  42300