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

Theorem cmptop 19763
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 2467 . . 3  |-  U. J  =  U. J
21iscmp 19756 . 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 1379    e. wcel 1767   A.wral 2817   E.wrex 2818    i^i cin 3480   ~Pcpw 4016   U.cuni 4251   Fincfn 7528   Topctop 19263   Compccmp 19754
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-in 3488  df-ss 3495  df-pw 4018  df-uni 4252  df-cmp 19755
This theorem is referenced by:  imacmp  19765  cmpcld  19770  fiuncmp  19772  cmpfii  19777  bwth  19778  bwthOLD  19779  locfincmp  19895  kgeni  19906  kgentopon  19907  kgencmp  19914  kgencmp2  19915  cmpkgen  19920  txcmplem1  20010  txcmp  20012  qtopcmp  20077  cmphaushmeo  20169  ptcmpfi  20182  fclscmpi  20398  alexsubALTlem1  20415  ptcmplem1  20420  ptcmpg  20425  evth  21327  evth2  21328  cmppcmp  27686  ordcmp  29839  heibor1lem  30232  cmpfiiin  30557  kelac1  30937  kelac2  30939  stoweidlem28  31651  stoweidlem50  31673  stoweidlem53  31676  stoweidlem57  31680  stoweidlem59  31682  stoweidlem62  31685
  Copyright terms: Public domain W3C validator