Theorem cmptop 23333

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ∀wral 3051  ∃wrex 3060   ∩ cin 3925  𝒫 cpw 4575  ∪ cuni 4883  Fincfn 8959  Topctop 22831  Compccmp 23324

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-ss 3943  df-pw 4577  df-uni 4884  df-cmp 23325

This theorem is referenced by:  imacmp  23335  cmpcld  23340  fiuncmp  23342  cmpfii  23347  bwth  23348  locfincmp  23464  kgeni  23475  kgentopon  23476  kgencmp  23483  kgencmp2  23484  cmpkgen  23489  txcmplem1  23579  txcmp  23581  qtopcmp  23646  cmphaushmeo  23738  ptcmpfi  23751  fclscmpi  23967  alexsubALTlem1  23985  ptcmplem1  23990  ptcmpg  23995  evth  24909  evth2  24910  cmppcmp  33889  ordcmp  36465  poimirlem30  37674  heibor1lem  37833  cmpfiiin  42720  kelac1  43087  kelac2  43089  stoweidlem28  46057  stoweidlem50  46079  stoweidlem53  46082  stoweidlem57  46086  stoweidlem62  46091