This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = \{j \in Top \| limPt (j) (⋃ j) = ⋃ j\}$

Detailed syntax breakdown

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