Theorem cmptop 23311

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.

Step	Hyp	Ref	Expression
1		eqid 2733	. . 3 ⊢ ∪ 𝐽 = ∪ 𝐽
2	1	iscmp 23304	. 2 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑟 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 = ∪ 𝑠)))
3	2	simplbi 497	1 ⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∀wral 3048  ∃wrex 3057   ∩ cin 3897  𝒫 cpw 4549  ∪ cuni 4858  Fincfn 8875  Topctop 22809  Compccmp 23302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-ss 3915  df-pw 4551  df-uni 4859  df-cmp 23303

This theorem is referenced by:  imacmp  23313  cmpcld  23318  fiuncmp  23320  cmpfii  23325  bwth  23326  locfincmp  23442  kgeni  23453  kgentopon  23454  kgencmp  23461  kgencmp2  23462  cmpkgen  23467  txcmplem1  23557  txcmp  23559  qtopcmp  23624  cmphaushmeo  23716  ptcmpfi  23729  fclscmpi  23945  alexsubALTlem1  23963  ptcmplem1  23968  ptcmpg  23973  evth  24886  evth2  24887  cmppcmp  33892  ordcmp  36512  poimirlem30  37710  heibor1lem  37869  cmpfiiin  42814  kelac1  43180  kelac2  43182  stoweidlem28  46150  stoweidlem50  46172  stoweidlem53  46175  stoweidlem57  46179  stoweidlem62  46184