Theorem cmptop

Description: A compact topology is a topology. (Contributed by Jeff Hankins, 29-Jun-2009)

	Ref	Expression
Assertion	cmptop	⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
2	1	iscmp	⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑟 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑟 → ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) ∪ 𝐽 = ∪ 𝑠 ) ) )
3	2	simplbi	⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )