Theorem perflp

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

	Ref	Expression
Hypothesis	lpfval.1	|- X = U. J
Assertion	perflp	|- ( J e. Perf -> ( ( limPt ` J ) ` X ) = X )

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	|- X = U. J
2	1	isperf	|- ( J e. Perf <-> ( J e. Top /\ ( ( limPt ` J ) ` X ) = X ) )
3	2	simprbi	|- ( J e. Perf -> ( ( limPt ` J ) ` X ) = X )