Metamath Proof Explorer


Theorem isperf

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

Ref Expression
Hypothesis lpfval.1 X = J
Assertion isperf J Perf J Top limPt J X = X

Proof

Step Hyp Ref Expression
1 lpfval.1 X = J
2 fveq2 j = J limPt j = limPt J
3 unieq j = J j = J
4 3 1 eqtr4di j = J j = X
5 2 4 fveq12d j = J limPt j j = limPt J X
6 5 4 eqeq12d j = J limPt j j = j limPt J X = X
7 df-perf Perf = j Top | limPt j j = j
8 6 7 elrab2 J Perf J Top limPt J X = X