Definition df-perf 17156

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 17154	. 2 class Perf
2		vj	. . . . . . 7 set j
3	2	cv 1648	. . . . . 6 class j
4	3	cuni 3975	. . . . 5 class U. j
5		clp 17153	. . . . . 6 class limPt
6	3, 5	cfv 5413	. . . . 5 class ( limPt ` j )
7	4, 6	cfv 5413	. . . 4 class ( ( limPt ` j ) ` U. j )
8	7, 4	wceq 1649	. . 3 wff ( ( limPt ` j ) ` U. j ) = U. j
9		ctop 16913	. . 3 class Top
10	8, 2, 9	crab 2670	. 2 class { j e. Top | ( ( limPt ` j ) ` U. j ) = U. j }
11	1, 10	wceq 1649	1 wff Perf = { j e. Top | ( ( limPt ` j ) ` U. j ) = U. j }

This definition is referenced by:  isperf  17169