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

Theorem cmptop 22546
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 22539 . 2 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑟 ∈ 𝒫 𝐽( 𝐽 = 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑠)))
32simplbi 498 1 (𝐽 ∈ Comp → 𝐽 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  wcel 2106  wral 3064  wrex 3065  cin 3886  𝒫 cpw 4533   cuni 4839  Fincfn 8733  Topctop 22042  Compccmp 22537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-pw 4535  df-uni 4840  df-cmp 22538
This theorem is referenced by:  imacmp  22548  cmpcld  22553  fiuncmp  22555  cmpfii  22560  bwth  22561  locfincmp  22677  kgeni  22688  kgentopon  22689  kgencmp  22696  kgencmp2  22697  cmpkgen  22702  txcmplem1  22792  txcmp  22794  qtopcmp  22859  cmphaushmeo  22951  ptcmpfi  22964  fclscmpi  23180  alexsubALTlem1  23198  ptcmplem1  23203  ptcmpg  23208  evth  24122  evth2  24123  cmppcmp  31808  ordcmp  34636  poimirlem30  35807  heibor1lem  35967  cmpfiiin  40519  kelac1  40888  kelac2  40890  stoweidlem28  43569  stoweidlem50  43591  stoweidlem53  43594  stoweidlem57  43598  stoweidlem62  43603
  Copyright terms: Public domain W3C validator