Theorem omelon 9559

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

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

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 7682  ax-inf2 9554

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 7811

This theorem is referenced by:  oancom  9564  cnfcomlem  9612  cnfcom  9613  cnfcom2lem  9614  cnfcom2  9615  cnfcom3lem  9616  cnfcom3  9617  cnfcom3clem  9618  cardom  9902  infxpenlem  9927  xpomen  9929  infxpidm2  9931  infxpenc  9932  infxpenc2lem1  9933  infxpenc2  9936  alephon  9983  infenaleph  10005  iunfictbso  10028  dfac12k  10062  infunsdom1  10126  domtriomlem  10356  iunctb  10489  pwcfsdom  10498  canthp1lem2  10568  pwfseqlem4a  10576  pwfseqlem4  10577  pwfseqlem5  10578  wunex3  10656  znnen  16141  qnnen  16142  cygctb  19825  2ndcctbss  23403  2ndcomap  23406  2ndcsep  23407  tx1stc  23598  tx2ndc  23599  met1stc  24469  met2ndci  24470  re2ndc  24749  uniiccdif  25539  dyadmbl  25561  opnmblALT  25564  mbfimaopnlem  25616  aannenlem3  26298  dfzs122  28467  exrecfnlem  37555  poimirlem32  37824  numinfctb  43381  onexomgt  43519  onexlimgt  43521  onexoegt  43522  1oaomeqom  43571  oaabsb  43572  oaordnrex  43573  oaordnr  43574  2omomeqom  43581  omnord1ex  43582  omnord1  43583  nnoeomeqom  43590  oenord1  43594  oaomoencom  43595  cantnftermord  43598  cantnfub  43599  cantnf2  43603  nnawordexg  43605  dflim5  43607  oacl2g  43608  onmcl  43609  omabs2  43610  omcl2  43611  tfsnfin  43630  ofoaf  43633  ofoafo  43634  naddcnff  43640  naddcnffo  43642  naddcnfcom  43644  naddcnfid1  43645  naddcnfid2  43646  naddcnfass  43647  naddwordnexlem0  43674  naddwordnexlem1  43675  naddwordnexlem3  43677  oawordex3  43678  naddwordnexlem4  43679  infordmin  43809  minregex  43811  omiscard  43820  sucomisnotcard  43821  aleph1min  43834  alephiso3  43836  wfaxinf2  45278