Theorem cmptop 23119

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ∀wral 3061  ∃wrex 3070   ∩ cin 3947  𝒫 cpw 4602  ∪ cuni 4908  Fincfn 8941  Topctop 22615  Compccmp 23110

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-in 3955  df-ss 3965  df-pw 4604  df-uni 4909  df-cmp 23111

This theorem is referenced by:  imacmp  23121  cmpcld  23126  fiuncmp  23128  cmpfii  23133  bwth  23134  locfincmp  23250  kgeni  23261  kgentopon  23262  kgencmp  23269  kgencmp2  23270  cmpkgen  23275  txcmplem1  23365  txcmp  23367  qtopcmp  23432  cmphaushmeo  23524  ptcmpfi  23537  fclscmpi  23753  alexsubALTlem1  23771  ptcmplem1  23776  ptcmpg  23781  evth  24699  evth2  24700  cmppcmp  33124  ordcmp  35635  poimirlem30  36821  heibor1lem  36980  cmpfiiin  41737  kelac1  42107  kelac2  42109  stoweidlem28  45043  stoweidlem50  45065  stoweidlem53  45068  stoweidlem57  45072  stoweidlem62  45077