Theorem omelon 9647

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  Oncon0 6362  ωcom 7877

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751  ax-inf2 9642

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-om 7878

This theorem is used by:  oancom  9652  cnfcomlem  9700  cnfcom  9701  cnfcom2lem  9702  cnfcom2  9703  cnfcom3lem  9704  cnfcom3  9705  cnfcom3clem  9706  cardom  10067  infxpenlem  10092  xpomen  10094  infxpidm2  10096  infxpenc  10097  infxpenc2lem1  10098  infxpenc2  10101  alephon  10148  infenaleph  10170  iunfictbso  10193  dfac12k  10226  infunsdom1  10290  domtriomlem  10520  dmct  10602  fimact  10615  fnct  10620  iunctb  10659  pwcfsdom  10668  canthp1lem2  10738  pwfseqlem4a  10746  pwfseqlem4  10747  pwfseqlem5  10748  wunex3  10826  znnen  16380  qnnen  16381  cygctb  20106  2ndcctbss  23774  2ndcomap  23777  2ndcsep  23778  tx1stc  23969  tx2ndc  23970  met1stc  24840  met2ndci  24841  re2ndc  25120  uniiccdif  25899  dyadmbl  25921  opnmblALT  25924  mbfimaopnlem  25976  aannenlem3  26657  dfz12s2  28874  exrecfnlem  38345  poimirlem32  38613  numinfctb  44148  onexomgt  44286  onexlimgt  44288  onexoegt  44289  1oaomeqom  44338  oaabsb  44339  oaordnrex  44340  oaordnr  44341  2omomeqom  44348  omnord1ex  44349  omnord1  44350  nnoeomeqom  44357  oenord1  44361  oaomoencom  44362  cantnftermord  44365  cantnfub  44366  cantnf2  44370  nnawordexg  44372  dflim5  44374  oacl2g  44375  onmcl  44376  omabs2  44377  omcl2  44378  tfsnfin  44397  ofoaf  44400  ofoafo  44401  naddcnff  44407  naddcnffo  44409  naddcnfcom  44411  naddcnfid1  44412  naddcnfid2  44413  naddcnfass  44414  naddwordnexlem0  44441  naddwordnexlem1  44442  naddwordnexlem3  44444  oawordex3  44445  naddwordnexlem4  44446  infordmin  44576  minregex  44578  omiscard  44587  sucomisnotcard  44588  aleph1min  44601  alephiso3  44603  wfaxinf2  46034  subsaliuncl  47411  smflimlem6  47829