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	$$⊢\mathrm{Perf}=\left\{j\in \mathrm{Top}|\mathrm{limPt}\left(j\right)\left(\bigcup j\right)=\bigcup j\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cperf	$$class\mathrm{Perf}$$
1		vj	$$setvarj$$
2		ctop	$$class\mathrm{Top}$$
3		clp	$$class\mathrm{limPt}$$
4	1	cv	$$setvarj$$
5	4 3	cfv	$$class\mathrm{limPt}\left(j\right)$$
6	4	cuni	$$class\bigcup j$$
7	6 5	cfv	$$class\mathrm{limPt}\left(j\right)\left(\bigcup j\right)$$
8	7 6	wceq	$$wff\mathrm{limPt}\left(j\right)\left(\bigcup j\right)=\bigcup j$$
9	8 1 2	crab	$$class\left\{j\in \mathrm{Top}|\mathrm{limPt}\left(j\right)\left(\bigcup j\right)=\bigcup j\right\}$$
10	0 9	wceq	$$wff\mathrm{Perf}=\left\{j\in \mathrm{Top}|\mathrm{limPt}\left(j\right)\left(\bigcup j\right)=\bigcup j\right\}$$