Theorem cmptop 23385

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ∀wral 3054  ∃wrex 3064   ∩ cin 3889  𝒫 cpw 4536  ∪ cuni 4845  Fincfn 8890  Topctop 22883  Compccmp 23376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-ss 3907  df-pw 4538  df-uni 4846  df-cmp 23377

This theorem is referenced by:  imacmp  23387  cmpcld  23392  fiuncmp  23394  cmpfii  23399  bwth  23400  locfincmp  23516  kgeni  23527  kgentopon  23528  kgencmp  23535  kgencmp2  23536  cmpkgen  23541  txcmplem1  23631  txcmp  23633  qtopcmp  23698  cmphaushmeo  23790  ptcmpfi  23803  fclscmpi  24019  alexsubALTlem1  24037  ptcmplem1  24042  ptcmpg  24047  evth  24951  evth2  24952  cmppcmp  34049  ordcmp  36682  poimirlem30  38024  heibor1lem  38183  cmpfiiin  43153  kelac1  43515  kelac2  43517  stoweidlem28  46478  stoweidlem50  46500  stoweidlem53  46503  stoweidlem57  46507  stoweidlem62  46512