Metamath Proof Explorer

Theorem lpfval

Description: The limit point function on the subsets of a topology's base set. (Contributed by NM, 10-Feb-2007) (Revised by Mario Carneiro, 11-Nov-2013)

		Ref	Expression
	Hypothesis	lpfval.1	$⊢ X = ⋃ J$
	Assertion	lpfval	$⊢ J \in Top \to limPt (J) = (x \in 𝒫 X ⟼ \{y \| y \in cls (J) (x ∖ \{y\})\})$

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	$⊢ X = ⋃ J$
2	1	topopn	$⊢ J \in Top \to X \in J$
3		pwexg	$⊢ X \in J \to 𝒫 X \in V$
4		mptexg	$⊢ 𝒫 X \in V \to (x \in 𝒫 X ⟼ \{y \| y \in cls (J) (x ∖ \{y\})\}) \in V$
5	2 3 4	3syl	$⊢ J \in Top \to (x \in 𝒫 X ⟼ \{y \| y \in cls (J) (x ∖ \{y\})\}) \in V$
6		unieq	$⊢ j = J \to ⋃ j = ⋃ J$
7	6 1	eqtr4di	$⊢ j = J \to ⋃ j = X$
8	7	pweqd	$⊢ j = J \to 𝒫 ⋃ j = 𝒫 X$
9		fveq2	$⊢ j = J \to cls (j) = cls (J)$
10	9	fveq1d	$⊢ j = J \to cls (j) (x ∖ \{y\}) = cls (J) (x ∖ \{y\})$
11	10	eleq2d	$⊢ j = J \to (y \in cls (j) (x ∖ \{y\}) \leftrightarrow y \in cls (J) (x ∖ \{y\}))$
12	11	abbidv	$⊢ j = J \to \{y \| y \in cls (j) (x ∖ \{y\})\} = \{y \| y \in cls (J) (x ∖ \{y\})\}$
13	8 12	mpteq12dv	$⊢ j = J \to (x \in 𝒫 ⋃ j ⟼ \{y \| y \in cls (j) (x ∖ \{y\})\}) = (x \in 𝒫 X ⟼ \{y \| y \in cls (J) (x ∖ \{y\})\})$
14		df-lp	$⊢ limPt = (j \in Top ⟼ (x \in 𝒫 ⋃ j ⟼ \{y \| y \in cls (j) (x ∖ \{y\})\}))$
15	13 14	fvmptg	$⊢ (J \in Top \land (x \in 𝒫 X ⟼ \{y \| y \in cls (J) (x ∖ \{y\})\}) \in V) \to limPt (J) = (x \in 𝒫 X ⟼ \{y \| y \in cls (J) (x ∖ \{y\})\})$
16	5 15	mpdan	$⊢ J \in Top \to limPt (J) = (x \in 𝒫 X ⟼ \{y \| y \in cls (J) (x ∖ \{y\})\})$