Theorem cmptop 22546

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  ∀wral 3064  ∃wrex 3065   ∩ cin 3886  𝒫 cpw 4533  ∪ cuni 4839  Fincfn 8733  Topctop 22042  Compccmp 22537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-pw 4535  df-uni 4840  df-cmp 22538

This theorem is referenced by:  imacmp  22548  cmpcld  22553  fiuncmp  22555  cmpfii  22560  bwth  22561  locfincmp  22677  kgeni  22688  kgentopon  22689  kgencmp  22696  kgencmp2  22697  cmpkgen  22702  txcmplem1  22792  txcmp  22794  qtopcmp  22859  cmphaushmeo  22951  ptcmpfi  22964  fclscmpi  23180  alexsubALTlem1  23198  ptcmplem1  23203  ptcmpg  23208  evth  24122  evth2  24123  cmppcmp  31808  ordcmp  34636  poimirlem30  35807  heibor1lem  35967  cmpfiiin  40519  kelac1  40888  kelac2  40890  stoweidlem28  43569  stoweidlem50  43591  stoweidlem53  43594  stoweidlem57  43598  stoweidlem62  43603