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

Theorem cmptop 23403
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 2737 . . 3 𝐽 = 𝐽
21iscmp 23396 . 2 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑟 ∈ 𝒫 𝐽( 𝐽 = 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑠)))
32simplbi 497 1 (𝐽 ∈ Comp → 𝐽 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wcel 2108  wral 3061  wrex 3070  cin 3950  𝒫 cpw 4600   cuni 4907  Fincfn 8985  Topctop 22899  Compccmp 23394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-ss 3968  df-pw 4602  df-uni 4908  df-cmp 23395
This theorem is referenced by:  imacmp  23405  cmpcld  23410  fiuncmp  23412  cmpfii  23417  bwth  23418  locfincmp  23534  kgeni  23545  kgentopon  23546  kgencmp  23553  kgencmp2  23554  cmpkgen  23559  txcmplem1  23649  txcmp  23651  qtopcmp  23716  cmphaushmeo  23808  ptcmpfi  23821  fclscmpi  24037  alexsubALTlem1  24055  ptcmplem1  24060  ptcmpg  24065  evth  24991  evth2  24992  cmppcmp  33857  ordcmp  36448  poimirlem30  37657  heibor1lem  37816  cmpfiiin  42708  kelac1  43075  kelac2  43077  stoweidlem28  46043  stoweidlem50  46065  stoweidlem53  46068  stoweidlem57  46072  stoweidlem62  46077
  Copyright terms: Public domain W3C validator