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

Theorem cmptop 19003
Description: A compact topology is a topology. (Contributed by Jeff Hankins, 29-Jun-2009.)
Assertion
Ref Expression
cmptop  |-  ( J  e.  Comp  ->  J  e. 
Top )

Proof of Theorem cmptop
Dummy variables  s 
r are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2443 . . 3  |-  U. J  =  U. J
21iscmp 18996 . 2  |-  ( J  e.  Comp  <->  ( J  e. 
Top  /\  A. r  e.  ~P  J ( U. J  =  U. r  ->  E. s  e.  ( ~P r  i^i  Fin ) U. J  =  U. s ) ) )
32simplbi 460 1  |-  ( J  e.  Comp  ->  J  e. 
Top )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756   A.wral 2720   E.wrex 2721    i^i cin 3332   ~Pcpw 3865   U.cuni 4096   Fincfn 7315   Topctop 18503   Compccmp 18994
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-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-in 3340  df-ss 3347  df-pw 3867  df-uni 4097  df-cmp 18995
This theorem is referenced by:  imacmp  19005  cmpcld  19010  fiuncmp  19012  cmpfii  19017  bwth  19018  bwthOLD  19019  kgeni  19115  kgentopon  19116  kgencmp  19123  kgencmp2  19124  cmpkgen  19129  txcmplem1  19219  txcmp  19221  qtopcmp  19286  cmphaushmeo  19378  ptcmpfi  19391  fclscmpi  19607  alexsubALTlem1  19624  ptcmplem1  19629  ptcmpg  19634  evth  20536  evth2  20537  ordcmp  28298  locfincmp  28581  heibor1lem  28713  cmpfiiin  29038  kelac1  29421  kelac2  29423  stoweidlem28  29828  stoweidlem50  29850  stoweidlem53  29853  stoweidlem57  29857  stoweidlem59  29859  stoweidlem62  29862
  Copyright terms: Public domain W3C validator