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

Theorem cmptop 17450
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 2435 . . 3  |-  U. J  =  U. J
21iscmp 17443 . 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 1652    e. wcel 1725   A.wral 2697   E.wrex 2698    i^i cin 3311   ~Pcpw 3791   U.cuni 4007   Fincfn 7101   Topctop 16950   Compccmp 17441
This theorem is referenced by:  imacmp  17452  cmpcld  17457  fiuncmp  17459  cmpfii  17464  bwth  17465  kgeni  17561  kgentopon  17562  kgencmp  17569  kgencmp2  17570  cmpkgen  17575  txcmplem1  17665  txcmp  17667  qtopcmp  17732  cmphaushmeo  17824  ptcmpfi  17837  fclscmpi  18053  alexsubALTlem1  18070  ptcmplem1  18075  ptcmpg  18080  evth  18976  evth2  18977  ordcmp  26189  locfincmp  26365  heibor1lem  26499  cmpfiiin  26732  kelac1  27119  kelac2  27121  stoweidlem28  27734  stoweidlem50  27756  stoweidlem53  27759  stoweidlem57  27763  stoweidlem59  27765  stoweidlem62  27768
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-in 3319  df-ss 3326  df-pw 3793  df-uni 4008  df-cmp 17442
  Copyright terms: Public domain W3C validator