Theorem cmptop 22146

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3053  ∃wrex 3054   ∩ cin 3842  𝒫 cpw 4488  ∪ cuni 4796  Fincfn 8555  Topctop 21644  Compccmp 22137

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-in 3850  df-ss 3860  df-pw 4490  df-uni 4797  df-cmp 22138

This theorem is referenced by:  imacmp  22148  cmpcld  22153  fiuncmp  22155  cmpfii  22160  bwth  22161  locfincmp  22277  kgeni  22288  kgentopon  22289  kgencmp  22296  kgencmp2  22297  cmpkgen  22302  txcmplem1  22392  txcmp  22394  qtopcmp  22459  cmphaushmeo  22551  ptcmpfi  22564  fclscmpi  22780  alexsubALTlem1  22798  ptcmplem1  22803  ptcmpg  22808  evth  23711  evth2  23712  cmppcmp  31380  ordcmp  34274  poimirlem30  35430  heibor1lem  35590  cmpfiiin  40091  kelac1  40460  kelac2  40462  stoweidlem28  43111  stoweidlem50  43133  stoweidlem53  43136  stoweidlem57  43140  stoweidlem62  43145