Theorem cmptop 23378

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ∀wral 3053  ∃wrex 3063   ∩ cin 3882  𝒫 cpw 4529  ∪ cuni 4838  Fincfn 8883  Topctop 22876  Compccmp 23369

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 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-ss 3900  df-pw 4531  df-uni 4839  df-cmp 23370

This theorem is referenced by:  imacmp  23380  cmpcld  23385  fiuncmp  23387  cmpfii  23392  bwth  23393  locfincmp  23509  kgeni  23520  kgentopon  23521  kgencmp  23528  kgencmp2  23529  cmpkgen  23534  txcmplem1  23624  txcmp  23626  qtopcmp  23691  cmphaushmeo  23783  ptcmpfi  23796  fclscmpi  24012  alexsubALTlem1  24030  ptcmplem1  24035  ptcmpg  24040  evth  24944  evth2  24945  cmppcmp  34042  ordcmp  36675  poimirlem30  38017  heibor1lem  38176  cmpfiiin  43146  kelac1  43508  kelac2  43510  stoweidlem28  46471  stoweidlem50  46493  stoweidlem53  46496  stoweidlem57  46500  stoweidlem62  46505