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 } |
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 } |