Theorem cmptop 23360

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3051  ∃wrex 3061   ∩ cin 3888  𝒫 cpw 4541  ∪ cuni 4850  Fincfn 8893  Topctop 22858  Compccmp 23351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-ss 3906  df-pw 4543  df-uni 4851  df-cmp 23352

This theorem is referenced by:  imacmp  23362  cmpcld  23367  fiuncmp  23369  cmpfii  23374  bwth  23375  locfincmp  23491  kgeni  23502  kgentopon  23503  kgencmp  23510  kgencmp2  23511  cmpkgen  23516  txcmplem1  23606  txcmp  23608  qtopcmp  23673  cmphaushmeo  23765  ptcmpfi  23778  fclscmpi  23994  alexsubALTlem1  24012  ptcmplem1  24017  ptcmpg  24022  evth  24926  evth2  24927  cmppcmp  34002  ordcmp  36629  poimirlem30  37971  heibor1lem  38130  cmpfiiin  43129  kelac1  43491  kelac2  43493  stoweidlem28  46456  stoweidlem50  46478  stoweidlem53  46481  stoweidlem57  46485  stoweidlem62  46490