Step | Hyp | Ref
| Expression |
1 | | lpfval.1 |
. . . 4
β’ π = βͺ
π½ |
2 | 1 | topopn 22239 |
. . 3
β’ (π½ β Top β π β π½) |
3 | | pwexg 5331 |
. . 3
β’ (π β π½ β π« π β V) |
4 | | mptexg 7167 |
. . 3
β’
(π« π β
V β (π₯ β
π« π β¦ {π¦ β£ π¦ β ((clsβπ½)β(π₯ β {π¦}))}) β V) |
5 | 2, 3, 4 | 3syl 18 |
. 2
β’ (π½ β Top β (π₯ β π« π β¦ {π¦ β£ π¦ β ((clsβπ½)β(π₯ β {π¦}))}) β V) |
6 | | unieq 4874 |
. . . . . 6
β’ (π = π½ β βͺ π = βͺ
π½) |
7 | 6, 1 | eqtr4di 2794 |
. . . . 5
β’ (π = π½ β βͺ π = π) |
8 | 7 | pweqd 4575 |
. . . 4
β’ (π = π½ β π« βͺ π =
π« π) |
9 | | fveq2 6839 |
. . . . . . 7
β’ (π = π½ β (clsβπ) = (clsβπ½)) |
10 | 9 | fveq1d 6841 |
. . . . . 6
β’ (π = π½ β ((clsβπ)β(π₯ β {π¦})) = ((clsβπ½)β(π₯ β {π¦}))) |
11 | 10 | eleq2d 2823 |
. . . . 5
β’ (π = π½ β (π¦ β ((clsβπ)β(π₯ β {π¦})) β π¦ β ((clsβπ½)β(π₯ β {π¦})))) |
12 | 11 | abbidv 2805 |
. . . 4
β’ (π = π½ β {π¦ β£ π¦ β ((clsβπ)β(π₯ β {π¦}))} = {π¦ β£ π¦ β ((clsβπ½)β(π₯ β {π¦}))}) |
13 | 8, 12 | mpteq12dv 5194 |
. . 3
β’ (π = π½ β (π₯ β π« βͺ π
β¦ {π¦ β£ π¦ β ((clsβπ)β(π₯ β {π¦}))}) = (π₯ β π« π β¦ {π¦ β£ π¦ β ((clsβπ½)β(π₯ β {π¦}))})) |
14 | | df-lp 22471 |
. . 3
β’ limPt =
(π β Top β¦
(π₯ β π« βͺ π
β¦ {π¦ β£ π¦ β ((clsβπ)β(π₯ β {π¦}))})) |
15 | 13, 14 | fvmptg 6943 |
. 2
β’ ((π½ β Top β§ (π₯ β π« π β¦ {π¦ β£ π¦ β ((clsβπ½)β(π₯ β {π¦}))}) β V) β (limPtβπ½) = (π₯ β π« π β¦ {π¦ β£ π¦ β ((clsβπ½)β(π₯ β {π¦}))})) |
16 | 5, 15 | mpdan 685 |
1
β’ (π½ β Top β
(limPtβπ½) = (π₯ β π« π β¦ {π¦ β£ π¦ β ((clsβπ½)β(π₯ β {π¦}))})) |