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

Theorem cmptop 21406
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 2802 . . 3 𝐽 = 𝐽
21iscmp 21399 . 2 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑟 ∈ 𝒫 𝐽( 𝐽 = 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑠)))
32simplbi 487 1 (𝐽 ∈ Comp → 𝐽 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2155  wral 3092  wrex 3093  cin 3762  𝒫 cpw 4345   cuni 4623  Fincfn 8186  Topctop 20905  Compccmp 21397
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ral 3097  df-rex 3098  df-rab 3101  df-v 3389  df-in 3770  df-ss 3777  df-pw 4347  df-uni 4624  df-cmp 21398
This theorem is referenced by:  imacmp  21408  cmpcld  21413  fiuncmp  21415  cmpfii  21420  bwth  21421  locfincmp  21537  kgeni  21548  kgentopon  21549  kgencmp  21556  kgencmp2  21557  cmpkgen  21562  txcmplem1  21652  txcmp  21654  qtopcmp  21719  cmphaushmeo  21811  ptcmpfi  21824  fclscmpi  22040  alexsubALTlem1  22058  ptcmplem1  22063  ptcmpg  22068  evth  22965  evth2  22966  cmppcmp  30244  ordcmp  32757  poimirlem30  33746  heibor1lem  33913  cmpfiiin  37756  kelac1  38128  kelac2  38130  stoweidlem28  40718  stoweidlem50  40740  stoweidlem53  40743  stoweidlem57  40747  stoweidlem62  40752
  Copyright terms: Public domain W3C validator