Theorem cmptop 23533

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ∃wrex 3089   ∩ cin 3905  𝒫 cpw 4563  ∪ cuni 4873  Fincfn 8944  Topctop 23031  Compccmp 23524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-ss 3923  df-pw 4565  df-uni 4874  df-cmp 23525

This theorem is referenced by:  imacmp  23535  cmpcld  23540  fiuncmp  23542  cmpfii  23547  bwth  23548  locfincmp  23664  kgeni  23675  kgentopon  23676  kgencmp  23683  kgencmp2  23684  cmpkgen  23689  txcmplem1  23779  txcmp  23781  qtopcmp  23846  cmphaushmeo  23938  ptcmpfi  23951  fclscmpi  24167  alexsubALTlem1  24185  ptcmplem1  24190  ptcmpg  24195  evth  25099  evth2  25100  cmppcmp  34226  ordcmp  36936  poimirlem30  38279  heibor1lem  38438  cmpfiiin  43408  kelac1  43770  kelac2  43772  stoweidlem28  46722  stoweidlem50  46744  stoweidlem53  46747  stoweidlem57  46751  stoweidlem62  46756