Theorem cmptop 23298

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053   ∩ cin 3904  𝒫 cpw 4553  ∪ cuni 4861  Fincfn 8879  Topctop 22796  Compccmp 23289

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-ss 3922  df-pw 4555  df-uni 4862  df-cmp 23290

This theorem is referenced by:  imacmp  23300  cmpcld  23305  fiuncmp  23307  cmpfii  23312  bwth  23313  locfincmp  23429  kgeni  23440  kgentopon  23441  kgencmp  23448  kgencmp2  23449  cmpkgen  23454  txcmplem1  23544  txcmp  23546  qtopcmp  23611  cmphaushmeo  23703  ptcmpfi  23716  fclscmpi  23932  alexsubALTlem1  23950  ptcmplem1  23955  ptcmpg  23960  evth  24874  evth2  24875  cmppcmp  33824  ordcmp  36420  poimirlem30  37629  heibor1lem  37788  cmpfiiin  42670  kelac1  43036  kelac2  43038  stoweidlem28  46010  stoweidlem50  46032  stoweidlem53  46035  stoweidlem57  46039  stoweidlem62  46044