Theorem cmptop 23370

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062   ∩ cin 3889  𝒫 cpw 4542  ∪ cuni 4851  Fincfn 8886  Topctop 22868  Compccmp 23361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-ss 3907  df-pw 4544  df-uni 4852  df-cmp 23362

This theorem is referenced by:  imacmp  23372  cmpcld  23377  fiuncmp  23379  cmpfii  23384  bwth  23385  locfincmp  23501  kgeni  23512  kgentopon  23513  kgencmp  23520  kgencmp2  23521  cmpkgen  23526  txcmplem1  23616  txcmp  23618  qtopcmp  23683  cmphaushmeo  23775  ptcmpfi  23788  fclscmpi  24004  alexsubALTlem1  24022  ptcmplem1  24027  ptcmpg  24032  evth  24936  evth2  24937  cmppcmp  34018  ordcmp  36645  poimirlem30  37985  heibor1lem  38144  cmpfiiin  43143  kelac1  43509  kelac2  43511  stoweidlem28  46474  stoweidlem50  46496  stoweidlem53  46499  stoweidlem57  46503  stoweidlem62  46508