Theorem cmptop 23418

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  ∀wral 3058  ∃wrex 3067   ∩ cin 3961  𝒫 cpw 4604  ∪ cuni 4911  Fincfn 8983  Topctop 22914  Compccmp 23409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-ss 3979  df-pw 4606  df-uni 4912  df-cmp 23410

This theorem is referenced by:  imacmp  23420  cmpcld  23425  fiuncmp  23427  cmpfii  23432  bwth  23433  locfincmp  23549  kgeni  23560  kgentopon  23561  kgencmp  23568  kgencmp2  23569  cmpkgen  23574  txcmplem1  23664  txcmp  23666  qtopcmp  23731  cmphaushmeo  23823  ptcmpfi  23836  fclscmpi  24052  alexsubALTlem1  24070  ptcmplem1  24075  ptcmpg  24080  evth  25004  evth2  25005  cmppcmp  33818  ordcmp  36429  poimirlem30  37636  heibor1lem  37795  cmpfiiin  42684  kelac1  43051  kelac2  43053  stoweidlem28  45983  stoweidlem50  46005  stoweidlem53  46008  stoweidlem57  46012  stoweidlem62  46017