This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem perflp

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

		Ref	Expression
	Hypothesis	lpfval.1	$⊢ X = ⋃ J$
	Assertion	perflp	$⊢ J \in Perf \to limPt (J) (X) = X$

Step	Hyp	Ref	Expression
1		lpfval.1	$⊢ X = ⋃ J$
2	1	isperf	$⊢ J \in Perf \leftrightarrow (J \in Top \land limPt (J) (X) = X)$
3	2	simprbi	$⊢ J \in Perf \to limPt (J) (X) = X$