Theorem cmptop 23589

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  ∀wral 3082  ∃wrex 3092   ∩ cin 3907  𝒫 cpw 4567  ∪ cuni 4877  Fincfn 8952  Topctop 23087  Compccmp 23580

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-ss 3925  df-pw 4569  df-uni 4878  df-cmp 23581

This theorem is used by:  imacmp  23591  cmpcld  23596  fiuncmp  23598  cmpfii  23603  bwth  23604  locfincmp  23720  kgeni  23731  kgentopon  23732  kgencmp  23739  kgencmp2  23740  cmpkgen  23745  txcmplem1  23835  txcmp  23837  qtopcmp  23902  cmphaushmeo  23994  ptcmpfi  24007  fclscmpi  24223  alexsubALTlem1  24241  ptcmplem1  24246  ptcmpg  24251  evth  25155  evth2  25156  cmppcmp  34279  ordcmp  36999  poimirlem30  38342  heibor1lem  38501  cmpfiiin  43469  kelac1  43831  kelac2  43833  stoweidlem28  46783  stoweidlem50  46805  stoweidlem53  46808  stoweidlem57  46812  stoweidlem62  46817