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

Theorem cmptop 18839
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 2433 . . 3  |-  U. J  =  U. J
21iscmp 18832 . 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 457 1  |-  ( J  e.  Comp  ->  J  e. 
Top )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    e. wcel 1755   A.wral 2705   E.wrex 2706    i^i cin 3315   ~Pcpw 3848   U.cuni 4079   Fincfn 7298   Topctop 18339   Compccmp 18830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-in 3323  df-ss 3330  df-pw 3850  df-uni 4080  df-cmp 18831
This theorem is referenced by:  imacmp  18841  cmpcld  18846  fiuncmp  18848  cmpfii  18853  bwth  18854  bwthOLD  18855  kgeni  18951  kgentopon  18952  kgencmp  18959  kgencmp2  18960  cmpkgen  18965  txcmplem1  19055  txcmp  19057  qtopcmp  19122  cmphaushmeo  19214  ptcmpfi  19227  fclscmpi  19443  alexsubALTlem1  19460  ptcmplem1  19465  ptcmpg  19470  evth  20372  evth2  20373  ordcmp  28140  locfincmp  28417  heibor1lem  28549  cmpfiiin  28875  kelac1  29258  kelac2  29260  stoweidlem28  29666  stoweidlem50  29688  stoweidlem53  29691  stoweidlem57  29695  stoweidlem59  29697  stoweidlem62  29700
  Copyright terms: Public domain W3C validator