df-lp

Description: Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval . (Contributed by NM, 10-Feb-2007)

		Ref	Expression
	Assertion	df-lp	$⊢ limPt = (j \in Top ⟼ (x \in 𝒫 ⋃ j ⟼ \{y \| y \in cls (j) (x ∖ \{y\})\}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clp	$class limPt$
1		vj	$setvar j$
2		ctop	$class Top$
3		vx	$setvar x$
4	1	cv	$setvar j$
5	4	cuni	$class ⋃ j$
6	5	cpw	$class 𝒫 ⋃ j$
7		vy	$setvar y$
8	7	cv	$setvar y$
9		ccl	$class cls$
10	4 9	cfv	$class cls (j)$
11	3	cv	$setvar x$
12	8	csn	$class \{y\}$
13	11 12	cdif	$class (x ∖ \{y\})$
14	13 10	cfv	$class cls (j) (x ∖ \{y\})$
15	8 14	wcel	$wff y \in cls (j) (x ∖ \{y\})$
16	15 7	cab	$class \{y \| y \in cls (j) (x ∖ \{y\})\}$
17	3 6 16	cmpt	$class (x \in 𝒫 ⋃ j ⟼ \{y \| y \in cls (j) (x ∖ \{y\})\})$
18	1 2 17	cmpt	$class (j \in Top ⟼ (x \in 𝒫 ⋃ j ⟼ \{y \| y \in cls (j) (x ∖ \{y\})\}))$
19	0 18	wceq	$wff limPt = (j \in Top ⟼ (x \in 𝒫 ⋃ j ⟼ \{y \| y \in cls (j) (x ∖ \{y\})\}))$

Metamath Proof Explorer

Definition df-lp

Detailed syntax breakdown