Theorem omelon 9560

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

Syntax hints:   ∈ wcel 2114  Vcvv 3441  Oncon0 6318  ωcom 7811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378  ax-un 7683  ax-inf2 9555

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-tr 5207  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-om 7812

This theorem is referenced by:  oancom  9565  cnfcomlem  9613  cnfcom  9614  cnfcom2lem  9615  cnfcom2  9616  cnfcom3lem  9617  cnfcom3  9618  cnfcom3clem  9619  cardom  9903  infxpenlem  9928  xpomen  9930  infxpidm2  9932  infxpenc  9933  infxpenc2lem1  9934  infxpenc2  9937  alephon  9984  infenaleph  10006  iunfictbso  10029  dfac12k  10063  infunsdom1  10127  domtriomlem  10357  iunctb  10490  pwcfsdom  10499  canthp1lem2  10569  pwfseqlem4a  10577  pwfseqlem4  10578  pwfseqlem5  10579  wunex3  10657  znnen  16142  qnnen  16143  cygctb  19826  2ndcctbss  23404  2ndcomap  23407  2ndcsep  23408  tx1stc  23599  tx2ndc  23600  met1stc  24470  met2ndci  24471  re2ndc  24750  uniiccdif  25540  dyadmbl  25562  opnmblALT  25565  mbfimaopnlem  25617  aannenlem3  26299  dfz12s2  28489  exrecfnlem  37597  poimirlem32  37866  numinfctb  43423  onexomgt  43561  onexlimgt  43563  onexoegt  43564  1oaomeqom  43613  oaabsb  43614  oaordnrex  43615  oaordnr  43616  2omomeqom  43623  omnord1ex  43624  omnord1  43625  nnoeomeqom  43632  oenord1  43636  oaomoencom  43637  cantnftermord  43640  cantnfub  43641  cantnf2  43645  nnawordexg  43647  dflim5  43649  oacl2g  43650  onmcl  43651  omabs2  43652  omcl2  43653  tfsnfin  43672  ofoaf  43675  ofoafo  43676  naddcnff  43682  naddcnffo  43684  naddcnfcom  43686  naddcnfid1  43687  naddcnfid2  43688  naddcnfass  43689  naddwordnexlem0  43716  naddwordnexlem1  43717  naddwordnexlem3  43719  oawordex3  43720  naddwordnexlem4  43721  infordmin  43851  minregex  43853  omiscard  43862  sucomisnotcard  43863  aleph1min  43876  alephiso3  43878  wfaxinf2  45320