MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  omelon Structured version   Unicode version

Theorem omelon 7850
Description: Omega is an ordinal number. (Contributed by NM, 10-May-1998.) (Revised by Mario Carneiro, 30-Jan-2013.)
Assertion
Ref Expression
omelon  |-  om  e.  On

Proof of Theorem omelon
StepHypRef Expression
1 omex 7847 . 2  |-  om  e.  _V
2 omelon2 6486 . 2  |-  ( om  e.  _V  ->  om  e.  On )
31, 2ax-mp 5 1  |-  om  e.  On
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   _Vcvv 2970   Oncon0 4717   omcom 6474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-sep 4411  ax-nul 4419  ax-pr 4529  ax-un 6370  ax-inf2 7845
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3185  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-pss 3342  df-nul 3636  df-if 3790  df-pw 3860  df-sn 3876  df-pr 3878  df-tp 3880  df-op 3882  df-uni 4090  df-br 4291  df-opab 4349  df-tr 4384  df-eprel 4630  df-po 4639  df-so 4640  df-fr 4677  df-we 4679  df-ord 4720  df-on 4721  df-lim 4722  df-suc 4723  df-om 6475
This theorem is referenced by:  oancom  7855  cnfcomlem  7930  cnfcom  7931  cnfcom2lem  7932  cnfcom2  7933  cnfcom3lem  7934  cnfcom3  7935  cnfcom3clem  7936  cnfcomlemOLD  7938  cnfcomOLD  7939  cnfcom2lemOLD  7940  cnfcom2OLD  7941  cnfcom3lemOLD  7942  cnfcom3OLD  7943  cnfcom3clemOLD  7944  cardom  8154  infxpenlem  8178  xpomen  8180  infxpidm2  8181  infxpenc  8182  infxpenc2lem1  8183  infxpenc2  8186  infxpencOLD  8187  infxpenc2OLD  8190  alephon  8237  infenaleph  8259  iunfictbso  8282  dfac12k  8314  infunsdom1  8380  domtriomlem  8609  iunctb  8736  pwcfsdom  8745  canthp1lem2  8818  pwfseqlem4a  8826  pwfseqlem4  8827  pwfseqlem5  8828  wunex3  8906  znnen  13493  qnnen  13494  cygctb  16366  2ndcctbss  19057  2ndcomap  19060  2ndcsep  19061  tx1stc  19221  tx2ndc  19222  met1stc  20094  met2ndci  20095  re2ndc  20376  uniiccdif  21056  dyadmbl  21078  opnmblALT  21081  mbfimaopnlem  21131  aannenlem3  21794  numinfctb  29456
  Copyright terms: Public domain W3C validator