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 }