Metamath Proof Explorer


Definition df-perf

Description: Define the class of all perfect spaces. A perfect space is one for which every point in the set is a limit point of the whole space. (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion df-perf Perf=jTop|limPtjj=j

Detailed syntax breakdown

Step Hyp Ref Expression
0 cperf classPerf
1 vj setvarj
2 ctop classTop
3 clp classlimPt
4 1 cv setvarj
5 4 3 cfv classlimPtj
6 4 cuni classj
7 6 5 cfv classlimPtjj
8 7 6 wceq wfflimPtjj=j
9 8 1 2 crab classjTop|limPtjj=j
10 0 9 wceq wffPerf=jTop|limPtjj=j