Theorem cmptop 23308

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056   ∩ cin 3901  𝒫 cpw 4550  ∪ cuni 4859  Fincfn 8869  Topctop 22806  Compccmp 23299

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-ss 3919  df-pw 4552  df-uni 4860  df-cmp 23300

This theorem is referenced by:  imacmp  23310  cmpcld  23315  fiuncmp  23317  cmpfii  23322  bwth  23323  locfincmp  23439  kgeni  23450  kgentopon  23451  kgencmp  23458  kgencmp2  23459  cmpkgen  23464  txcmplem1  23554  txcmp  23556  qtopcmp  23621  cmphaushmeo  23713  ptcmpfi  23726  fclscmpi  23942  alexsubALTlem1  23960  ptcmplem1  23965  ptcmpg  23970  evth  24883  evth2  24884  cmppcmp  33866  ordcmp  36480  poimirlem30  37689  heibor1lem  37848  cmpfiiin  42729  kelac1  43095  kelac2  43097  stoweidlem28  46065  stoweidlem50  46087  stoweidlem53  46090  stoweidlem57  46094  stoweidlem62  46099