Theorem cmptop 23403

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ∀wral 3061  ∃wrex 3070   ∩ cin 3950  𝒫 cpw 4600  ∪ cuni 4907  Fincfn 8985  Topctop 22899  Compccmp 23394

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-ss 3968  df-pw 4602  df-uni 4908  df-cmp 23395

This theorem is referenced by:  imacmp  23405  cmpcld  23410  fiuncmp  23412  cmpfii  23417  bwth  23418  locfincmp  23534  kgeni  23545  kgentopon  23546  kgencmp  23553  kgencmp2  23554  cmpkgen  23559  txcmplem1  23649  txcmp  23651  qtopcmp  23716  cmphaushmeo  23808  ptcmpfi  23821  fclscmpi  24037  alexsubALTlem1  24055  ptcmplem1  24060  ptcmpg  24065  evth  24991  evth2  24992  cmppcmp  33857  ordcmp  36448  poimirlem30  37657  heibor1lem  37816  cmpfiiin  42708  kelac1  43075  kelac2  43077  stoweidlem28  46043  stoweidlem50  46065  stoweidlem53  46068  stoweidlem57  46072  stoweidlem62  46077