| Step | Hyp | Ref
| Expression |
|---|
| 1 | | flimval.1 |
. . . . 5
β’ π = βͺ
π½ |
| 2 | 1 | topopn 22729 |
. . . 4
β’ (π½ β Top β π β π½) |
| 3 | 2 | adantr 480 |
. . 3
β’ ((π½ β Top β§ πΉ β βͺ ran Fil) β π β π½) |
| 4 | | rabexg 5331 |
. . 3
β’ (π β π½ β {π₯ β π β£ (((neiβπ½)β{π₯}) β πΉ β§ πΉ β π« π)} β V) |
| 5 | 3, 4 | syl 17 |
. 2
β’ ((π½ β Top β§ πΉ β βͺ ran Fil) β {π₯ β π β£ (((neiβπ½)β{π₯}) β πΉ β§ πΉ β π« π)} β V) |
| 6 | | simpl 482 |
. . . . . 6
β’ ((π = π½ β§ π = πΉ) β π = π½) |
| 7 | 6 | unieqd 4922 |
. . . . 5
β’ ((π = π½ β§ π = πΉ) β βͺ π = βͺ
π½) |
| 8 | 7, 1 | eqtr4di 2789 |
. . . 4
β’ ((π = π½ β§ π = πΉ) β βͺ π = π) |
| 9 | 6 | fveq2d 6895 |
. . . . . . 7
β’ ((π = π½ β§ π = πΉ) β (neiβπ) = (neiβπ½)) |
| 10 | 9 | fveq1d 6893 |
. . . . . 6
β’ ((π = π½ β§ π = πΉ) β ((neiβπ)β{π₯}) = ((neiβπ½)β{π₯})) |
| 11 | | simpr 484 |
. . . . . 6
β’ ((π = π½ β§ π = πΉ) β π = πΉ) |
| 12 | 10, 11 | sseq12d 4015 |
. . . . 5
β’ ((π = π½ β§ π = πΉ) β (((neiβπ)β{π₯}) β π β ((neiβπ½)β{π₯}) β πΉ)) |
| 13 | 8 | pweqd 4619 |
. . . . . 6
β’ ((π = π½ β§ π = πΉ) β π« βͺ π =
π« π) |
| 14 | 11, 13 | sseq12d 4015 |
. . . . 5
β’ ((π = π½ β§ π = πΉ) β (π β π« βͺ π
β πΉ β π«
π)) |
| 15 | 12, 14 | anbi12d 630 |
. . . 4
β’ ((π = π½ β§ π = πΉ) β ((((neiβπ)β{π₯}) β π β§ π β π« βͺ π)
β (((neiβπ½)β{π₯}) β πΉ β§ πΉ β π« π))) |
| 16 | 8, 15 | rabeqbidv 3448 |
. . 3
β’ ((π = π½ β§ π = πΉ) β {π₯ β βͺ π β£ (((neiβπ)β{π₯}) β π β§ π β π« βͺ π)}
= {π₯ β π β£ (((neiβπ½)β{π₯}) β πΉ β§ πΉ β π« π)}) |
| 17 | | df-flim 23764 |
. . 3
β’ fLim =
(π β Top, π β βͺ ran Fil β¦ {π₯ β βͺ π β£ (((neiβπ)β{π₯}) β π β§ π β π« βͺ π)}) |
| 18 | 16, 17 | ovmpoga 7565 |
. 2
β’ ((π½ β Top β§ πΉ β βͺ ran Fil β§ {π₯ β π β£ (((neiβπ½)β{π₯}) β πΉ β§ πΉ β π« π)} β V) β (π½ fLim πΉ) = {π₯ β π β£ (((neiβπ½)β{π₯}) β πΉ β§ πΉ β π« π)}) |
| 19 | 5, 18 | mpd3an3 1461 |
1
β’ ((π½ β Top β§ πΉ β βͺ ran Fil) β (π½ fLim πΉ) = {π₯ β π β£ (((neiβπ½)β{π₯}) β πΉ β§ πΉ β π« π)}) |
