Theorem cmptop 22000

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107   ∩ cin 3880  𝒫 cpw 4497  ∪ cuni 4800  Fincfn 8492  Topctop 21498  Compccmp 21991

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499  df-uni 4801  df-cmp 21992

This theorem is referenced by:  imacmp  22002  cmpcld  22007  fiuncmp  22009  cmpfii  22014  bwth  22015  locfincmp  22131  kgeni  22142  kgentopon  22143  kgencmp  22150  kgencmp2  22151  cmpkgen  22156  txcmplem1  22246  txcmp  22248  qtopcmp  22313  cmphaushmeo  22405  ptcmpfi  22418  fclscmpi  22634  alexsubALTlem1  22652  ptcmplem1  22657  ptcmpg  22662  evth  23564  evth2  23565  cmppcmp  31211  ordcmp  33908  poimirlem30  35087  heibor1lem  35247  cmpfiiin  39638  kelac1  40007  kelac2  40009  stoweidlem28  42670  stoweidlem50  42692  stoweidlem53  42695  stoweidlem57  42699  stoweidlem62  42704