Definition df-perf 22861

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

Detailed syntax breakdown of Definition df-perf

Step	Hyp	Ref	Expression
1		cperf 22859	. 2 class Perf
2		vj	. . . . . . 7 setvar 𝑗
3	2	cv 1538	. . . . . 6 class 𝑗
4	3	cuni 4907	. . . . 5 class ∪ 𝑗
5		clp 22858	. . . . . 6 class limPt
6	3, 5	cfv 6542	. . . . 5 class (limPt‘𝑗)
7	4, 6	cfv 6542	. . . 4 class ((limPt‘𝑗)‘∪ 𝑗)
8	7, 4	wceq 1539	. . 3 wff ((limPt‘𝑗)‘∪ 𝑗) = ∪ 𝑗
9		ctop 22615	. . 3 class Top
10	8, 2, 9	crab 3430	. 2 class {𝑗 ∈ Top ∣ ((limPt‘𝑗)‘∪ 𝑗) = ∪ 𝑗}
11	1, 10	wceq 1539	1 wff Perf = {𝑗 ∈ Top ∣ ((limPt‘𝑗)‘∪ 𝑗) = ∪ 𝑗}

This definition is referenced by:  isperf  22875