Step |
Hyp |
Ref |
Expression |
1 |
|
lpfval.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
1
|
topopn |
⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 ) |
3 |
|
pwexg |
⊢ ( 𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V ) |
4 |
|
mptexg |
⊢ ( 𝒫 𝑋 ∈ V → ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } ) ∈ V ) |
5 |
2 3 4
|
3syl |
⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } ) ∈ V ) |
6 |
|
unieq |
⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽 ) |
7 |
6 1
|
eqtr4di |
⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = 𝑋 ) |
8 |
7
|
pweqd |
⊢ ( 𝑗 = 𝐽 → 𝒫 ∪ 𝑗 = 𝒫 𝑋 ) |
9 |
|
fveq2 |
⊢ ( 𝑗 = 𝐽 → ( cls ‘ 𝑗 ) = ( cls ‘ 𝐽 ) ) |
10 |
9
|
fveq1d |
⊢ ( 𝑗 = 𝐽 → ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) ) |
11 |
10
|
eleq2d |
⊢ ( 𝑗 = 𝐽 → ( 𝑦 ∈ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) ↔ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) ) ) |
12 |
11
|
abbidv |
⊢ ( 𝑗 = 𝐽 → { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } = { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } ) |
13 |
8 12
|
mpteq12dv |
⊢ ( 𝑗 = 𝐽 → ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } ) = ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } ) ) |
14 |
|
df-lp |
⊢ limPt = ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } ) ) |
15 |
13 14
|
fvmptg |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } ) ∈ V ) → ( limPt ‘ 𝐽 ) = ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } ) ) |
16 |
5 15
|
mpdan |
⊢ ( 𝐽 ∈ Top → ( limPt ‘ 𝐽 ) = ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } ) ) |