Theorem omelon 9111

Description: Omega is an ordinal number. (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 9108	. 2 ⊢ ω ∈ V
2		omelon2 7594	. 2 ⊢ (ω ∈ V → ω ∈ On)
3	1, 2	ax-mp 5	1 ⊢ ω ∈ On

Syntax hints:   ∈ wcel 2114  Vcvv 3496  Oncon0 6193  ωcom 7582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332  ax-un 7463  ax-inf2 9106

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-tr 5175  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-om 7583

This theorem is referenced by:  oancom  9116  cnfcomlem  9164  cnfcom  9165  cnfcom2lem  9166  cnfcom2  9167  cnfcom3lem  9168  cnfcom3  9169  cnfcom3clem  9170  cardom  9417  infxpenlem  9441  xpomen  9443  infxpidm2  9445  infxpenc  9446  infxpenc2lem1  9447  infxpenc2  9450  alephon  9497  infenaleph  9519  iunfictbso  9542  dfac12k  9575  infunsdom1  9637  domtriomlem  9866  iunctb  9998  pwcfsdom  10007  canthp1lem2  10077  pwfseqlem4a  10085  pwfseqlem4  10086  pwfseqlem5  10087  wunex3  10165  znnen  15567  qnnen  15568  cygctb  19014  2ndcctbss  22065  2ndcomap  22068  2ndcsep  22069  tx1stc  22260  tx2ndc  22261  met1stc  23133  met2ndci  23134  re2ndc  23411  uniiccdif  24181  dyadmbl  24203  opnmblALT  24206  mbfimaopnlem  24258  aannenlem3  24921  exrecfnlem  34662  poimirlem32  34926  numinfctb  39710  infordmin  39906  aleph1min  39923  alephiso3  39925