Theorem omelon 9669

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

Syntax hints:   ∈ wcel 2098  Vcvv 3463  Oncon0 6369  ωcom 7869

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5299  ax-nul 5306  ax-pr 5428  ax-un 7739  ax-inf2 9664

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3465  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3965  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-om 7870

This theorem is referenced by:  oancom  9674  cnfcomlem  9722  cnfcom  9723  cnfcom2lem  9724  cnfcom2  9725  cnfcom3lem  9726  cnfcom3  9727  cnfcom3clem  9728  cardom  10009  infxpenlem  10036  xpomen  10038  infxpidm2  10040  infxpenc  10041  infxpenc2lem1  10042  infxpenc2  10045  alephon  10092  infenaleph  10114  iunfictbso  10137  dfac12k  10170  infunsdom1  10236  domtriomlem  10465  iunctb  10597  pwcfsdom  10606  canthp1lem2  10676  pwfseqlem4a  10684  pwfseqlem4  10685  pwfseqlem5  10686  wunex3  10764  znnen  16188  qnnen  16189  cygctb  19851  2ndcctbss  23389  2ndcomap  23392  2ndcsep  23393  tx1stc  23584  tx2ndc  23585  met1stc  24460  met2ndci  24461  re2ndc  24747  uniiccdif  25537  dyadmbl  25559  opnmblALT  25562  mbfimaopnlem  25614  aannenlem3  26295  n0ssold  28254  exrecfnlem  36928  poimirlem32  37195  numinfctb  42592  onexomgt  42734  onexlimgt  42736  onexoegt  42737  1oaomeqom  42787  oaabsb  42788  oaordnrex  42789  oaordnr  42790  2omomeqom  42797  omnord1ex  42798  omnord1  42799  nnoeomeqom  42806  oenord1  42810  oaomoencom  42811  cantnftermord  42814  cantnfub  42815  cantnf2  42819  nnawordexg  42821  dflim5  42823  oacl2g  42824  onmcl  42825  omabs2  42826  omcl2  42827  tfsnfin  42846  ofoaf  42849  ofoafo  42850  naddcnff  42856  naddcnffo  42858  naddcnfcom  42860  naddcnfid1  42861  naddcnfid2  42862  naddcnfass  42863  naddwordnexlem0  42891  naddwordnexlem1  42892  naddwordnexlem3  42894  oawordex3  42895  naddwordnexlem4  42896  infordmin  43027  minregex  43029  omiscard  43038  sucomisnotcard  43039  aleph1min  43052  alephiso3  43054