Theorem cmptop 23282

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053   ∩ cin 3913  𝒫 cpw 4563  ∪ cuni 4871  Fincfn 8918  Topctop 22780  Compccmp 23273

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-ss 3931  df-pw 4565  df-uni 4872  df-cmp 23274

This theorem is referenced by:  imacmp  23284  cmpcld  23289  fiuncmp  23291  cmpfii  23296  bwth  23297  locfincmp  23413  kgeni  23424  kgentopon  23425  kgencmp  23432  kgencmp2  23433  cmpkgen  23438  txcmplem1  23528  txcmp  23530  qtopcmp  23595  cmphaushmeo  23687  ptcmpfi  23700  fclscmpi  23916  alexsubALTlem1  23934  ptcmplem1  23939  ptcmpg  23944  evth  24858  evth2  24859  cmppcmp  33848  ordcmp  36435  poimirlem30  37644  heibor1lem  37803  cmpfiiin  42685  kelac1  43052  kelac2  43054  stoweidlem28  46026  stoweidlem50  46048  stoweidlem53  46051  stoweidlem57  46055  stoweidlem62  46060