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 = { j e. Top | ( ( limPt ` j ) ` U. j ) = U. j }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cperf
 |-  Perf
1 vj
 |-  j
2 ctop
 |-  Top
3 clp
 |-  limPt
4 1 cv
 |-  j
5 4 3 cfv
 |-  ( limPt ` j )
6 4 cuni
 |-  U. j
7 6 5 cfv
 |-  ( ( limPt ` j ) ` U. j )
8 7 6 wceq
 |-  ( ( limPt ` j ) ` U. j ) = U. j
9 8 1 2 crab
 |-  { j e. Top | ( ( limPt ` j ) ` U. j ) = U. j }
10 0 9 wceq
 |-  Perf = { j e. Top | ( ( limPt ` j ) ` U. j ) = U. j }