Theorem omelon 9661

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

Syntax hints:   ∈ wcel 2099  Vcvv 3469  Oncon0 6363  ωcom 7864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734  ax-inf2 9656

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ne 2936  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-tr 5260  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-om 7865

This theorem is referenced by:  oancom  9666  cnfcomlem  9714  cnfcom  9715  cnfcom2lem  9716  cnfcom2  9717  cnfcom3lem  9718  cnfcom3  9719  cnfcom3clem  9720  cardom  10001  infxpenlem  10028  xpomen  10030  infxpidm2  10032  infxpenc  10033  infxpenc2lem1  10034  infxpenc2  10037  alephon  10084  infenaleph  10106  iunfictbso  10129  dfac12k  10162  infunsdom1  10228  domtriomlem  10457  iunctb  10589  pwcfsdom  10598  canthp1lem2  10668  pwfseqlem4a  10676  pwfseqlem4  10677  pwfseqlem5  10678  wunex3  10756  znnen  16180  qnnen  16181  cygctb  19838  2ndcctbss  23346  2ndcomap  23349  2ndcsep  23350  tx1stc  23541  tx2ndc  23542  met1stc  24417  met2ndci  24418  re2ndc  24704  uniiccdif  25494  dyadmbl  25516  opnmblALT  25519  mbfimaopnlem  25571  aannenlem3  26252  n0ssold  28205  exrecfnlem  36794  poimirlem32  37060  numinfctb  42449  onexomgt  42592  onexlimgt  42594  onexoegt  42595  1oaomeqom  42645  oaabsb  42646  oaordnrex  42647  oaordnr  42648  2omomeqom  42655  omnord1ex  42656  omnord1  42657  nnoeomeqom  42664  oenord1  42668  oaomoencom  42669  cantnftermord  42672  cantnfub  42673  cantnf2  42677  nnawordexg  42679  dflim5  42681  oacl2g  42682  onmcl  42683  omabs2  42684  omcl2  42685  tfsnfin  42704  ofoaf  42707  ofoafo  42708  naddcnff  42714  naddcnffo  42716  naddcnfcom  42718  naddcnfid1  42719  naddcnfid2  42720  naddcnfass  42721  naddwordnexlem0  42749  naddwordnexlem1  42750  naddwordnexlem3  42752  oawordex3  42753  naddwordnexlem4  42754  infordmin  42885  minregex  42887  omiscard  42896  sucomisnotcard  42897  aleph1min  42910  alephiso3  42912