Theorem omelon 9605

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450  Oncon0 6334  ωcom 7844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pr 5389  ax-un 7713  ax-inf2 9600

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-pss 3936  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-tr 5217  df-eprel 5540  df-po 5548  df-so 5549  df-fr 5593  df-we 5595  df-ord 6337  df-on 6338  df-lim 6339  df-suc 6340  df-om 7845

This theorem is referenced by:  oancom  9610  cnfcomlem  9658  cnfcom  9659  cnfcom2lem  9660  cnfcom2  9661  cnfcom3lem  9662  cnfcom3  9663  cnfcom3clem  9664  cardom  9945  infxpenlem  9972  xpomen  9974  infxpidm2  9976  infxpenc  9977  infxpenc2lem1  9978  infxpenc2  9981  alephon  10028  infenaleph  10050  iunfictbso  10073  dfac12k  10107  infunsdom1  10171  domtriomlem  10401  iunctb  10533  pwcfsdom  10542  canthp1lem2  10612  pwfseqlem4a  10620  pwfseqlem4  10621  pwfseqlem5  10622  wunex3  10700  znnen  16186  qnnen  16187  cygctb  19828  2ndcctbss  23348  2ndcomap  23351  2ndcsep  23352  tx1stc  23543  tx2ndc  23544  met1stc  24415  met2ndci  24416  re2ndc  24695  uniiccdif  25485  dyadmbl  25507  opnmblALT  25510  mbfimaopnlem  25562  aannenlem3  26244  n0ssold  28251  exrecfnlem  37362  poimirlem32  37641  numinfctb  43085  onexomgt  43223  onexlimgt  43225  onexoegt  43226  1oaomeqom  43275  oaabsb  43276  oaordnrex  43277  oaordnr  43278  2omomeqom  43285  omnord1ex  43286  omnord1  43287  nnoeomeqom  43294  oenord1  43298  oaomoencom  43299  cantnftermord  43302  cantnfub  43303  cantnf2  43307  nnawordexg  43309  dflim5  43311  oacl2g  43312  onmcl  43313  omabs2  43314  omcl2  43315  tfsnfin  43334  ofoaf  43337  ofoafo  43338  naddcnff  43344  naddcnffo  43346  naddcnfcom  43348  naddcnfid1  43349  naddcnfid2  43350  naddcnfass  43351  naddwordnexlem0  43378  naddwordnexlem1  43379  naddwordnexlem3  43381  oawordex3  43382  naddwordnexlem4  43383  infordmin  43514  minregex  43516  omiscard  43525  sucomisnotcard  43526  aleph1min  43539  alephiso3  43541  wfaxinf2  44984