Definition df-perf 19511

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

Assertion

Ref	Expression
df-perf	|- Perf = { j e. Top | ( ( limPt ` j ) ` U. j ) = U. j }

Detailed syntax breakdown of Definition df-perf

Step	Hyp	Ref	Expression
1		cperf 19509	. 2 class Perf
2		vj	. . . . . . 7 setvar j
3	2	cv 1382	. . . . . 6 class j
4	3	cuni 4234	. . . . 5 class U. j
5		clp 19508	. . . . . 6 class limPt
6	3, 5	cfv 5578	. . . . 5 class ( limPt ` j )
7	4, 6	cfv 5578	. . . 4 class ( ( limPt ` j ) ` U. j )
8	7, 4	wceq 1383	. . 3 wff ( ( limPt ` j ) ` U. j ) = U. j
9		ctop 19267	. . 3 class Top
10	8, 2, 9	crab 2797	. 2 class { j e. Top | ( ( limPt ` j ) ` U. j ) = U. j }
11	1, 10	wceq 1383	1 wff Perf = { j e. Top | ( ( limPt ` j ) ` U. j ) = U. j }

This definition is referenced by:  isperf  19525