Theorem omelon 9587

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

Syntax hints:   ∈ wcel 2132  Vcvv 3444  Oncon0 6331  ωcom 7831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pr 5380  ax-un 7703  ax-inf2 9582

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ne 2948  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-pss 3915  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-tr 5198  df-eprel 5536  df-po 5544  df-so 5545  df-fr 5589  df-we 5591  df-ord 6334  df-on 6335  df-lim 6336  df-suc 6337  df-om 7832

This theorem is referenced by:  oancom  9592  cnfcomlem  9640  cnfcom  9641  cnfcom2lem  9642  cnfcom2  9643  cnfcom3lem  9644  cnfcom3  9645  cnfcom3clem  9646  cardom  9930  infxpenlem  9955  xpomen  9957  infxpidm2  9959  infxpenc  9960  infxpenc2lem1  9961  infxpenc2  9964  alephon  10011  infenaleph  10033  iunfictbso  10056  dfac12k  10090  infunsdom1  10154  domtriomlem  10385  iunctb  10518  pwcfsdom  10527  canthp1lem2  10597  pwfseqlem4a  10605  pwfseqlem4  10606  pwfseqlem5  10607  wunex3  10685  znnen  16216  qnnen  16217  cygctb  19904  2ndcctbss  23484  2ndcomap  23487  2ndcsep  23488  tx1stc  23679  tx2ndc  23680  met1stc  24550  met2ndci  24551  re2ndc  24830  uniiccdif  25609  dyadmbl  25631  opnmblALT  25634  mbfimaopnlem  25686  aannenlem3  26360  dfz12s2  28547  exrecfnlem  37811  poimirlem32  38089  numinfctb  43618  onexomgt  43756  onexlimgt  43758  onexoegt  43759  1oaomeqom  43808  oaabsb  43809  oaordnrex  43810  oaordnr  43811  2omomeqom  43818  omnord1ex  43819  omnord1  43820  nnoeomeqom  43827  oenord1  43831  oaomoencom  43832  cantnftermord  43835  cantnfub  43836  cantnf2  43840  nnawordexg  43842  dflim5  43844  oacl2g  43845  onmcl  43846  omabs2  43847  omcl2  43848  tfsnfin  43867  ofoaf  43870  ofoafo  43871  naddcnff  43877  naddcnffo  43879  naddcnfcom  43881  naddcnfid1  43882  naddcnfid2  43883  naddcnfass  43884  naddwordnexlem0  43911  naddwordnexlem1  43912  naddwordnexlem3  43914  oawordex3  43915  naddwordnexlem4  43916  infordmin  44046  minregex  44048  omiscard  44057  sucomisnotcard  44058  aleph1min  44071  alephiso3  44073  wfaxinf2  45515