Theorem cmptop 22783

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ∀wral 3060  ∃wrex 3069   ∩ cin 3912  𝒫 cpw 4565  ∪ cuni 4870  Fincfn 8890  Topctop 22279  Compccmp 22774

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 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-in 3920  df-ss 3930  df-pw 4567  df-uni 4871  df-cmp 22775

This theorem is referenced by:  imacmp  22785  cmpcld  22790  fiuncmp  22792  cmpfii  22797  bwth  22798  locfincmp  22914  kgeni  22925  kgentopon  22926  kgencmp  22933  kgencmp2  22934  cmpkgen  22939  txcmplem1  23029  txcmp  23031  qtopcmp  23096  cmphaushmeo  23188  ptcmpfi  23201  fclscmpi  23417  alexsubALTlem1  23435  ptcmplem1  23440  ptcmpg  23445  evth  24359  evth2  24360  cmppcmp  32528  ordcmp  34995  poimirlem30  36181  heibor1lem  36341  cmpfiiin  41078  kelac1  41448  kelac2  41450  stoweidlem28  44389  stoweidlem50  44411  stoweidlem53  44414  stoweidlem57  44418  stoweidlem62  44423