Theorem omelon 9599

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  Oncon0 6346  ωcom 7846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391  ax-un 7718  ax-inf2 9594

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-tr 5209  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-om 7847

This theorem is referenced by:  oancom  9604  cnfcomlem  9652  cnfcom  9653  cnfcom2lem  9654  cnfcom2  9655  cnfcom3lem  9656  cnfcom3  9657  cnfcom3clem  9658  cardom  9956  infxpenlem  9981  xpomen  9983  infxpidm2  9985  infxpenc  9986  infxpenc2lem1  9987  infxpenc2  9990  alephon  10037  infenaleph  10059  iunfictbso  10082  dfac12k  10115  infunsdom1  10179  domtriomlem  10410  iunctb  10543  pwcfsdom  10552  canthp1lem2  10622  pwfseqlem4a  10630  pwfseqlem4  10631  pwfseqlem5  10632  wunex3  10710  znnen  16254  qnnen  16255  cygctb  19942  2ndcctbss  23522  2ndcomap  23525  2ndcsep  23526  tx1stc  23717  tx2ndc  23718  met1stc  24588  met2ndci  24589  re2ndc  24868  uniiccdif  25647  dyadmbl  25669  opnmblALT  25672  mbfimaopnlem  25724  aannenlem3  26401  dfz12s2  28588  exrecfnlem  37878  poimirlem32  38156  numinfctb  43685  onexomgt  43823  onexlimgt  43825  onexoegt  43826  1oaomeqom  43875  oaabsb  43876  oaordnrex  43877  oaordnr  43878  2omomeqom  43885  omnord1ex  43886  omnord1  43887  nnoeomeqom  43894  oenord1  43898  oaomoencom  43899  cantnftermord  43902  cantnfub  43903  cantnf2  43907  nnawordexg  43909  dflim5  43911  oacl2g  43912  onmcl  43913  omabs2  43914  omcl2  43915  tfsnfin  43934  ofoaf  43937  ofoafo  43938  naddcnff  43944  naddcnffo  43946  naddcnfcom  43948  naddcnfid1  43949  naddcnfid2  43950  naddcnfass  43951  naddwordnexlem0  43978  naddwordnexlem1  43979  naddwordnexlem3  43981  oawordex3  43982  naddwordnexlem4  43983  infordmin  44113  minregex  44115  omiscard  44124  sucomisnotcard  44125  aleph1min  44138  alephiso3  44140  wfaxinf2  45568