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 = { 𝑗 ∈ Top ∣ ( ( limPt ‘ 𝑗 ) ‘ ∪ 𝑗 ) = ∪ 𝑗 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cperf	⊢ Perf
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		clp	⊢ limPt
4	1	cv	⊢ 𝑗
5	4 3	cfv	⊢ ( limPt ‘ 𝑗 )
6	4	cuni	⊢ ∪ 𝑗
7	6 5	cfv	⊢ ( ( limPt ‘ 𝑗 ) ‘ ∪ 𝑗 )
8	7 6	wceq	⊢ ( ( limPt ‘ 𝑗 ) ‘ ∪ 𝑗 ) = ∪ 𝑗
9	8 1 2	crab	⊢ { 𝑗 ∈ Top ∣ ( ( limPt ‘ 𝑗 ) ‘ ∪ 𝑗 ) = ∪ 𝑗 }
10	0 9	wceq	⊢ Perf = { 𝑗 ∈ Top ∣ ( ( limPt ‘ 𝑗 ) ‘ ∪ 𝑗 ) = ∪ 𝑗 }