Theorem cmptop 23626

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3078  ∃wrex 3088   ∩ cin 3901  𝒫 cpw 4560  ∪ cuni 4870  Fincfn 8956  Topctop 23124  Compccmp 23617

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-ss 3919  df-pw 4562  df-uni 4871  df-cmp 23618

This theorem is used by:  imacmp  23628  cmpcld  23633  fiuncmp  23635  cmpfii  23640  bwth  23641  locfincmp  23758  kgeni  23769  kgentopon  23770  kgencmp  23777  kgencmp2  23778  cmpkgen  23783  txcmplem1  23873  txcmp  23875  qtopcmp  23940  cmphaushmeo  24032  ptcmpfi  24045  fclscmpi  24261  alexsubALTlem1  24279  ptcmplem1  24284  ptcmpg  24289  evth  25193  evth2  25194  cmppcmp  34376  ordcmp  37074  poimirlem30  38407  heibor1lem  38567  cmpfiiin  43550  kelac1  43912  kelac2  43914  stoweidlem28  46864  stoweidlem50  46886  stoweidlem53  46889  stoweidlem57  46893  stoweidlem62  46898