Theorem perftop

Description: A perfect space is a topology. (Contributed by Mario Carneiro, 25-Dec-2016)

	Ref	Expression
Assertion	perftop	$$⊢J\in \mathrm{Perf}\to J\in \mathrm{Top}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\bigcup J=\bigcup J$$
2	1	isperf	$$⊢J\in \mathrm{Perf}\leftrightarrow \left(J\in \mathrm{Top}\wedge \mathrm{limPt}\left(J\right)\left(\bigcup J\right)=\bigcup J\right)$$
3	2	simplbi	$$⊢J\in \mathrm{Perf}\to J\in \mathrm{Top}$$