| Step | Hyp | Ref
| Expression |
|---|
| 1 | | lpfval.1 |
. . . . 5
β’ π = βͺ
π½ |
| 2 | 1 | lpfval 22862 |
. . . 4
β’ (π½ β Top β
(limPtβπ½) = (π¦ β π« π β¦ {π₯ β£ π₯ β ((clsβπ½)β(π¦ β {π₯}))})) |
| 3 | 2 | fveq1d 6893 |
. . 3
β’ (π½ β Top β
((limPtβπ½)βπ) = ((π¦ β π« π β¦ {π₯ β£ π₯ β ((clsβπ½)β(π¦ β {π₯}))})βπ)) |
| 4 | 3 | adantr 481 |
. 2
β’ ((π½ β Top β§ π β π) β ((limPtβπ½)βπ) = ((π¦ β π« π β¦ {π₯ β£ π₯ β ((clsβπ½)β(π¦ β {π₯}))})βπ)) |
| 5 | | eqid 2732 |
. . 3
β’ (π¦ β π« π β¦ {π₯ β£ π₯ β ((clsβπ½)β(π¦ β {π₯}))}) = (π¦ β π« π β¦ {π₯ β£ π₯ β ((clsβπ½)β(π¦ β {π₯}))}) |
| 6 | | difeq1 4115 |
. . . . . 6
β’ (π¦ = π β (π¦ β {π₯}) = (π β {π₯})) |
| 7 | 6 | fveq2d 6895 |
. . . . 5
β’ (π¦ = π β ((clsβπ½)β(π¦ β {π₯})) = ((clsβπ½)β(π β {π₯}))) |
| 8 | 7 | eleq2d 2819 |
. . . 4
β’ (π¦ = π β (π₯ β ((clsβπ½)β(π¦ β {π₯})) β π₯ β ((clsβπ½)β(π β {π₯})))) |
| 9 | 8 | abbidv 2801 |
. . 3
β’ (π¦ = π β {π₯ β£ π₯ β ((clsβπ½)β(π¦ β {π₯}))} = {π₯ β£ π₯ β ((clsβπ½)β(π β {π₯}))}) |
| 10 | 1 | topopn 22628 |
. . . . 5
β’ (π½ β Top β π β π½) |
| 11 | | elpw2g 5344 |
. . . . 5
β’ (π β π½ β (π β π« π β π β π)) |
| 12 | 10, 11 | syl 17 |
. . . 4
β’ (π½ β Top β (π β π« π β π β π)) |
| 13 | 12 | biimpar 478 |
. . 3
β’ ((π½ β Top β§ π β π) β π β π« π) |
| 14 | 10 | adantr 481 |
. . . 4
β’ ((π½ β Top β§ π β π) β π β π½) |
| 15 | | ssdifss 4135 |
. . . . . 6
β’ (π β π β (π β {π₯}) β π) |
| 16 | 1 | clsss3 22783 |
. . . . . . 7
β’ ((π½ β Top β§ (π β {π₯}) β π) β ((clsβπ½)β(π β {π₯})) β π) |
| 17 | 16 | sseld 3981 |
. . . . . 6
β’ ((π½ β Top β§ (π β {π₯}) β π) β (π₯ β ((clsβπ½)β(π β {π₯})) β π₯ β π)) |
| 18 | 15, 17 | sylan2 593 |
. . . . 5
β’ ((π½ β Top β§ π β π) β (π₯ β ((clsβπ½)β(π β {π₯})) β π₯ β π)) |
| 19 | 18 | abssdv 4065 |
. . . 4
β’ ((π½ β Top β§ π β π) β {π₯ β£ π₯ β ((clsβπ½)β(π β {π₯}))} β π) |
| 20 | 14, 19 | ssexd 5324 |
. . 3
β’ ((π½ β Top β§ π β π) β {π₯ β£ π₯ β ((clsβπ½)β(π β {π₯}))} β V) |
| 21 | 5, 9, 13, 20 | fvmptd3 7021 |
. 2
β’ ((π½ β Top β§ π β π) β ((π¦ β π« π β¦ {π₯ β£ π₯ β ((clsβπ½)β(π¦ β {π₯}))})βπ) = {π₯ β£ π₯ β ((clsβπ½)β(π β {π₯}))}) |
| 22 | 4, 21 | eqtrd 2772 |
1
β’ ((π½ β Top β§ π β π) β ((limPtβπ½)βπ) = {π₯ β£ π₯ β ((clsβπ½)β(π β {π₯}))}) |
