Theorem cmptop 23718

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086   ∩ cin 4089  𝒫 cpw 4556  ∪ cuni 4866  Fincfn 8976  Topctop 23216  Compccmp 23709

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-pw 4558  df-uni 4867  df-cmp 23710

This theorem is used by:  imacmp  23720  cmpcld  23725  fiuncmp  23727  cmpfii  23732  bwth  23733  locfincmp  23850  kgeni  23861  kgentopon  23862  kgencmp  23869  kgencmp2  23870  cmpkgen  23875  txcmplem1  23965  txcmp  23967  qtopcmp  24032  cmphaushmeo  24124  ptcmpfi  24137  fclscmpi  24353  alexsubALTlem1  24371  ptcmplem1  24376  ptcmpg  24381  evth  25285  evth2  25286  cmppcmp  34536  ordcmp  37327  poimirlem30  38661  heibor1lem  38836  cmpfiiin  43801  kelac1  44158  kelac2  44160  stoweidlem28  47131  stoweidlem50  47153  stoweidlem53  47156  stoweidlem57  47160  stoweidlem62  47165