Theorem cmptop 23693

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 2761	. . 3 ⊢ ∪ 𝐽 = ∪ 𝐽
2	1	iscmp 23686	. 2 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑟 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 = ∪ 𝑠)))
3	2	simplbi 502	1 ⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087   ∩ cin 3898  𝒫 cpw 4557  ∪ cuni 4867  Fincfn 8957  Topctop 23191  Compccmp 23684

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-ss 3916  df-pw 4559  df-uni 4868  df-cmp 23685

This theorem is used by:  imacmp  23695  cmpcld  23700  fiuncmp  23702  cmpfii  23707  bwth  23708  locfincmp  23825  kgeni  23836  kgentopon  23837  kgencmp  23844  kgencmp2  23845  cmpkgen  23850  txcmplem1  23940  txcmp  23942  qtopcmp  24007  cmphaushmeo  24099  ptcmpfi  24112  fclscmpi  24328  alexsubALTlem1  24346  ptcmplem1  24351  ptcmpg  24356  evth  25260  evth2  25261  cmppcmp  34472  ordcmp  37205  poimirlem30  38536  heibor1lem  38711  cmpfiiin  43661  kelac1  44023  kelac2  44025  stoweidlem28  46982  stoweidlem50  47004  stoweidlem53  47007  stoweidlem57  47011  stoweidlem62  47016