Theorem omelon 9715

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488  Oncon0 6395  ωcom 7903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-inf2 9710

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-tr 5284  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-om 7904

This theorem is referenced by:  oancom  9720  cnfcomlem  9768  cnfcom  9769  cnfcom2lem  9770  cnfcom2  9771  cnfcom3lem  9772  cnfcom3  9773  cnfcom3clem  9774  cardom  10055  infxpenlem  10082  xpomen  10084  infxpidm2  10086  infxpenc  10087  infxpenc2lem1  10088  infxpenc2  10091  alephon  10138  infenaleph  10160  iunfictbso  10183  dfac12k  10217  infunsdom1  10281  domtriomlem  10511  iunctb  10643  pwcfsdom  10652  canthp1lem2  10722  pwfseqlem4a  10730  pwfseqlem4  10731  pwfseqlem5  10732  wunex3  10810  znnen  16260  qnnen  16261  cygctb  19934  2ndcctbss  23484  2ndcomap  23487  2ndcsep  23488  tx1stc  23679  tx2ndc  23680  met1stc  24555  met2ndci  24556  re2ndc  24842  uniiccdif  25632  dyadmbl  25654  opnmblALT  25657  mbfimaopnlem  25709  aannenlem3  26390  n0ssold  28373  exrecfnlem  37345  poimirlem32  37612  numinfctb  43060  onexomgt  43202  onexlimgt  43204  onexoegt  43205  1oaomeqom  43255  oaabsb  43256  oaordnrex  43257  oaordnr  43258  2omomeqom  43265  omnord1ex  43266  omnord1  43267  nnoeomeqom  43274  oenord1  43278  oaomoencom  43279  cantnftermord  43282  cantnfub  43283  cantnf2  43287  nnawordexg  43289  dflim5  43291  oacl2g  43292  onmcl  43293  omabs2  43294  omcl2  43295  tfsnfin  43314  ofoaf  43317  ofoafo  43318  naddcnff  43324  naddcnffo  43326  naddcnfcom  43328  naddcnfid1  43329  naddcnfid2  43330  naddcnfass  43331  naddwordnexlem0  43358  naddwordnexlem1  43359  naddwordnexlem3  43361  oawordex3  43362  naddwordnexlem4  43363  infordmin  43494  minregex  43496  omiscard  43505  sucomisnotcard  43506  aleph1min  43519  alephiso3  43521