Theorem omelon 9531

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

Syntax hints:   ∈ wcel 2110  Vcvv 3434  Oncon0 6302  ωcom 7791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7663  ax-inf2 9526

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-pss 3920  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-tr 5197  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-om 7792

This theorem is referenced by:  oancom  9536  cnfcomlem  9584  cnfcom  9585  cnfcom2lem  9586  cnfcom2  9587  cnfcom3lem  9588  cnfcom3  9589  cnfcom3clem  9590  cardom  9871  infxpenlem  9896  xpomen  9898  infxpidm2  9900  infxpenc  9901  infxpenc2lem1  9902  infxpenc2  9905  alephon  9952  infenaleph  9974  iunfictbso  9997  dfac12k  10031  infunsdom1  10095  domtriomlem  10325  iunctb  10457  pwcfsdom  10466  canthp1lem2  10536  pwfseqlem4a  10544  pwfseqlem4  10545  pwfseqlem5  10546  wunex3  10624  znnen  16113  qnnen  16114  cygctb  19797  2ndcctbss  23363  2ndcomap  23366  2ndcsep  23367  tx1stc  23558  tx2ndc  23559  met1stc  24429  met2ndci  24430  re2ndc  24709  uniiccdif  25499  dyadmbl  25521  opnmblALT  25524  mbfimaopnlem  25576  aannenlem3  26258  n0ssold  28274  exrecfnlem  37392  poimirlem32  37671  numinfctb  43115  onexomgt  43253  onexlimgt  43255  onexoegt  43256  1oaomeqom  43305  oaabsb  43306  oaordnrex  43307  oaordnr  43308  2omomeqom  43315  omnord1ex  43316  omnord1  43317  nnoeomeqom  43324  oenord1  43328  oaomoencom  43329  cantnftermord  43332  cantnfub  43333  cantnf2  43337  nnawordexg  43339  dflim5  43341  oacl2g  43342  onmcl  43343  omabs2  43344  omcl2  43345  tfsnfin  43364  ofoaf  43367  ofoafo  43368  naddcnff  43374  naddcnffo  43376  naddcnfcom  43378  naddcnfid1  43379  naddcnfid2  43380  naddcnfass  43381  naddwordnexlem0  43408  naddwordnexlem1  43409  naddwordnexlem3  43411  oawordex3  43412  naddwordnexlem4  43413  infordmin  43544  minregex  43546  omiscard  43555  sucomisnotcard  43556  aleph1min  43569  alephiso3  43571  wfaxinf2  45013