Theorem perflp

Description: The limit points of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Hypothesis	lpfval.1	$$⊢X=\bigcup J$$
Assertion	perflp	$$⊢J\in \mathrm{Perf}\to \mathrm{limPt}\left(J\right)\left(X\right)=X$$

Proof

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