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

Theorem cmptop 17381
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 2388 . . 3  |-  U. J  =  U. J
21iscmp 17374 . 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 447 1  |-  ( J  e.  Comp  ->  J  e. 
Top )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717   A.wral 2650   E.wrex 2651    i^i cin 3263   ~Pcpw 3743   U.cuni 3958   Fincfn 7046   Topctop 16882   Compccmp 17372
This theorem is referenced by:  imacmp  17383  cmpcld  17388  fiuncmp  17390  cmpfii  17395  kgeni  17491  kgentopon  17492  kgencmp  17499  kgencmp2  17500  cmpkgen  17505  txcmplem1  17595  txcmp  17597  qtopcmp  17662  cmphaushmeo  17754  ptcmpfi  17767  fclscmpi  17983  alexsubALTlem1  18000  ptcmplem1  18005  ptcmpg  18010  evth  18856  evth2  18857  ordcmp  25912  locfincmp  26076  heibor1lem  26210  cmpfiiin  26443  kelac1  26831  kelac2  26833  stoweidlem28  27446  stoweidlem50  27468  stoweidlem53  27471  stoweidlem57  27475  stoweidlem59  27477  stoweidlem62  27480
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-in 3271  df-ss 3278  df-pw 3745  df-uni 3959  df-cmp 17373
  Copyright terms: Public domain W3C validator