Theorem cmptop

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

	Ref	Expression
Assertion	cmptop	$$⊢J\in \mathrm{Comp}\to J\in \mathrm{Top}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\bigcup J=\bigcup J$$
2	1	iscmp	$$⊢J\in \mathrm{Comp}\leftrightarrow \left(J\in \mathrm{Top}\wedge \forall r\in 𝒫J\left(\bigcup J=\bigcup r\to \exists s\in \left(𝒫r\cap \mathrm{Fin}\right)\bigcup J=\bigcup s\right)\right)$$
3	2	simplbi	$$⊢J\in \mathrm{Comp}\to J\in \mathrm{Top}$$