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 = 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 )