Theorem perflp

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

	Ref	Expression
Hypothesis	lpfval.1	⊢ 𝑋 = ∪ 𝐽
Assertion	perflp	⊢ ( 𝐽 ∈ Perf → ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	⊢ 𝑋 = ∪ 𝐽
2	1	isperf	⊢ ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ) )
3	2	simprbi	⊢ ( 𝐽 ∈ Perf → ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 )