# Metamath Proof Explorer

## Definition 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 ${⊢}\mathrm{limPt}=\left({j}\in \mathrm{Top}⟼\left({x}\in 𝒫\bigcup {j}⟼\left\{{y}|{y}\in \mathrm{cls}\left({j}\right)\left({x}\setminus \left\{{y}\right\}\right)\right\}\right)\right)$

### Detailed syntax breakdown

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