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

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 limPt = ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clp ⊢ limPt
1 vj ⊢ 𝑗
2 ctop ⊢ Top
3 vx ⊢ 𝑥
4 1 cv ⊢ 𝑗
5 4 cuni ⊢ ∪ 𝑗
6 5 cpw ⊢ 𝒫 ∪ 𝑗
7 vy ⊢ 𝑦
8 7 cv ⊢ 𝑦
9 ccl ⊢ cls
10 4 9 cfv ⊢ ( cls ‘ 𝑗 )
11 3 cv ⊢ 𝑥
12 8 csn ⊢ { 𝑦 }
13 11 12 cdif ⊢ ( 𝑥 ∖ { 𝑦 } )
14 13 10 cfv ⊢ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) )
15 8 14 wcel ⊢ 𝑦 ∈ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) )
16 15 7 cab ⊢ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) }
17 3 6 16 cmpt ⊢ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } )
18 1 2 17 cmpt ⊢ ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } ) )
19 0 18 wceq ⊢ limPt = ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } ) )