Theorem cmptop 23513

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  ∀wral 3079  ∃wrex 3089   ∩ cin 3906  𝒫 cpw 4558  ∪ cuni 4868  Fincfn 8931  Topctop 23011  Compccmp 23504

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-ss 3924  df-pw 4560  df-uni 4869  df-cmp 23505

This theorem is referenced by:  imacmp  23515  cmpcld  23520  fiuncmp  23522  cmpfii  23527  bwth  23528  locfincmp  23644  kgeni  23655  kgentopon  23656  kgencmp  23663  kgencmp2  23664  cmpkgen  23669  txcmplem1  23759  txcmp  23761  qtopcmp  23826  cmphaushmeo  23918  ptcmpfi  23931  fclscmpi  24147  alexsubALTlem1  24165  ptcmplem1  24170  ptcmpg  24175  evth  25079  evth2  25080  cmppcmp  34165  ordcmp  36820  poimirlem30  38161  heibor1lem  38320  cmpfiiin  43290  kelac1  43652  kelac2  43654  stoweidlem28  46600  stoweidlem50  46622  stoweidlem53  46625  stoweidlem57  46629  stoweidlem62  46634