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

Theorem cmptop 22146
Description: A compact topology is a topology. (Contributed by Jeff Hankins, 29-Jun-2009.)
Assertion
Ref Expression
cmptop (𝐽 ∈ Comp → 𝐽 ∈ Top)

Proof of Theorem cmptop
Dummy variables 𝑠 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2738 . . 3 𝐽 = 𝐽
21iscmp 22139 . 2 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑟 ∈ 𝒫 𝐽( 𝐽 = 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑠)))
32simplbi 501 1 (𝐽 ∈ Comp → 𝐽 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2114  wral 3053  wrex 3054  cin 3842  𝒫 cpw 4488   cuni 4796  Fincfn 8555  Topctop 21644  Compccmp 22137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-in 3850  df-ss 3860  df-pw 4490  df-uni 4797  df-cmp 22138
This theorem is referenced by:  imacmp  22148  cmpcld  22153  fiuncmp  22155  cmpfii  22160  bwth  22161  locfincmp  22277  kgeni  22288  kgentopon  22289  kgencmp  22296  kgencmp2  22297  cmpkgen  22302  txcmplem1  22392  txcmp  22394  qtopcmp  22459  cmphaushmeo  22551  ptcmpfi  22564  fclscmpi  22780  alexsubALTlem1  22798  ptcmplem1  22803  ptcmpg  22808  evth  23711  evth2  23712  cmppcmp  31380  ordcmp  34274  poimirlem30  35430  heibor1lem  35590  cmpfiiin  40091  kelac1  40460  kelac2  40462  stoweidlem28  43111  stoweidlem50  43133  stoweidlem53  43136  stoweidlem57  43140  stoweidlem62  43145
  Copyright terms: Public domain W3C validator