Theorem cmptop 23746

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090   ∩ cin 4092  𝒫 cpw 4560  ∪ cuni 4870  Fincfn 9004  Topctop 23244  Compccmp 23737

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pw 4562  df-uni 4871  df-cmp 23738

This theorem is used by:  imacmp  23748  cmpcld  23753  fiuncmp  23755  cmpfii  23760  bwth  23761  locfincmp  23878  kgeni  23889  kgentopon  23890  kgencmp  23897  kgencmp2  23898  cmpkgen  23903  txcmplem1  23993  txcmp  23995  qtopcmp  24060  cmphaushmeo  24152  ptcmpfi  24165  fclscmpi  24381  alexsubALTlem1  24399  ptcmplem1  24404  ptcmpg  24409  evth  25313  evth2  25314  cmppcmp  34573  ordcmp  37426  poimirlem30  38773  heibor1lem  38946  cmpfiiin  43912  kelac1  44269  kelac2  44271  stoweidlem28  47253  stoweidlem50  47275  stoweidlem53  47278  stoweidlem57  47282  stoweidlem62  47287