Theorem omelon 9561

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

Syntax hints:   ∈ wcel 2109  Vcvv 3438  Oncon0 6311  ωcom 7806

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 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-inf2 9556

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-tr 5203  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-om 7807

This theorem is referenced by:  oancom  9566  cnfcomlem  9614  cnfcom  9615  cnfcom2lem  9616  cnfcom2  9617  cnfcom3lem  9618  cnfcom3  9619  cnfcom3clem  9620  cardom  9901  infxpenlem  9926  xpomen  9928  infxpidm2  9930  infxpenc  9931  infxpenc2lem1  9932  infxpenc2  9935  alephon  9982  infenaleph  10004  iunfictbso  10027  dfac12k  10061  infunsdom1  10125  domtriomlem  10355  iunctb  10487  pwcfsdom  10496  canthp1lem2  10566  pwfseqlem4a  10574  pwfseqlem4  10575  pwfseqlem5  10576  wunex3  10654  znnen  16139  qnnen  16140  cygctb  19789  2ndcctbss  23358  2ndcomap  23361  2ndcsep  23362  tx1stc  23553  tx2ndc  23554  met1stc  24425  met2ndci  24426  re2ndc  24705  uniiccdif  25495  dyadmbl  25517  opnmblALT  25520  mbfimaopnlem  25572  aannenlem3  26254  n0ssold  28268  exrecfnlem  37352  poimirlem32  37631  numinfctb  43076  onexomgt  43214  onexlimgt  43216  onexoegt  43217  1oaomeqom  43266  oaabsb  43267  oaordnrex  43268  oaordnr  43269  2omomeqom  43276  omnord1ex  43277  omnord1  43278  nnoeomeqom  43285  oenord1  43289  oaomoencom  43290  cantnftermord  43293  cantnfub  43294  cantnf2  43298  nnawordexg  43300  dflim5  43302  oacl2g  43303  onmcl  43304  omabs2  43305  omcl2  43306  tfsnfin  43325  ofoaf  43328  ofoafo  43329  naddcnff  43335  naddcnffo  43337  naddcnfcom  43339  naddcnfid1  43340  naddcnfid2  43341  naddcnfass  43342  naddwordnexlem0  43369  naddwordnexlem1  43370  naddwordnexlem3  43372  oawordex3  43373  naddwordnexlem4  43374  infordmin  43505  minregex  43507  omiscard  43516  sucomisnotcard  43517  aleph1min  43530  alephiso3  43532  wfaxinf2  44975