Step | Hyp | Ref
| Expression |
1 | | topontop 22415 |
. . 3
β’ (π½ β (TopOnβπ) β π½ β Top) |
2 | | fvssunirn 6925 |
. . . 4
β’
(Filβπ)
β βͺ ran Fil |
3 | 2 | sseli 3979 |
. . 3
β’ (πΏ β (Filβπ) β πΏ β βͺ ran
Fil) |
4 | | unieq 4920 |
. . . . . 6
β’ (π₯ = π½ β βͺ π₯ = βͺ
π½) |
5 | | unieq 4920 |
. . . . . 6
β’ (π¦ = πΏ β βͺ π¦ = βͺ
πΏ) |
6 | 4, 5 | oveqan12d 7428 |
. . . . 5
β’ ((π₯ = π½ β§ π¦ = πΏ) β (βͺ π₯ βm βͺ π¦) =
(βͺ π½ βm βͺ πΏ)) |
7 | | simpl 484 |
. . . . . 6
β’ ((π₯ = π½ β§ π¦ = πΏ) β π₯ = π½) |
8 | 4 | adantr 482 |
. . . . . . . 8
β’ ((π₯ = π½ β§ π¦ = πΏ) β βͺ π₯ = βͺ
π½) |
9 | 8 | oveq1d 7424 |
. . . . . . 7
β’ ((π₯ = π½ β§ π¦ = πΏ) β (βͺ π₯ FilMap π) = (βͺ π½ FilMap π)) |
10 | | simpr 486 |
. . . . . . 7
β’ ((π₯ = π½ β§ π¦ = πΏ) β π¦ = πΏ) |
11 | 9, 10 | fveq12d 6899 |
. . . . . 6
β’ ((π₯ = π½ β§ π¦ = πΏ) β ((βͺ
π₯ FilMap π)βπ¦) = ((βͺ π½ FilMap π)βπΏ)) |
12 | 7, 11 | oveq12d 7427 |
. . . . 5
β’ ((π₯ = π½ β§ π¦ = πΏ) β (π₯ fLim ((βͺ π₯ FilMap π)βπ¦)) = (π½ fLim ((βͺ π½ FilMap π)βπΏ))) |
13 | 6, 12 | mpteq12dv 5240 |
. . . 4
β’ ((π₯ = π½ β§ π¦ = πΏ) β (π β (βͺ π₯ βm βͺ π¦)
β¦ (π₯ fLim ((βͺ π₯
FilMap π)βπ¦))) = (π β (βͺ π½ βm βͺ πΏ)
β¦ (π½ fLim ((βͺ π½
FilMap π)βπΏ)))) |
14 | | df-flf 23444 |
. . . 4
β’ fLimf =
(π₯ β Top, π¦ β βͺ ran Fil β¦ (π β (βͺ π₯ βm βͺ π¦)
β¦ (π₯ fLim ((βͺ π₯
FilMap π)βπ¦)))) |
15 | | ovex 7442 |
. . . . 5
β’ (βͺ π½
βm βͺ πΏ) β V |
16 | 15 | mptex 7225 |
. . . 4
β’ (π β (βͺ π½
βm βͺ πΏ) β¦ (π½ fLim ((βͺ π½ FilMap π)βπΏ))) β V |
17 | 13, 14, 16 | ovmpoa 7563 |
. . 3
β’ ((π½ β Top β§ πΏ β βͺ ran Fil) β (π½ fLimf πΏ) = (π β (βͺ π½ βm βͺ πΏ)
β¦ (π½ fLim ((βͺ π½
FilMap π)βπΏ)))) |
18 | 1, 3, 17 | syl2an 597 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ)) β (π½ fLimf πΏ) = (π β (βͺ π½ βm βͺ πΏ)
β¦ (π½ fLim ((βͺ π½
FilMap π)βπΏ)))) |
19 | | toponuni 22416 |
. . . . 5
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
20 | 19 | eqcomd 2739 |
. . . 4
β’ (π½ β (TopOnβπ) β βͺ π½ =
π) |
21 | | filunibas 23385 |
. . . 4
β’ (πΏ β (Filβπ) β βͺ πΏ =
π) |
22 | 20, 21 | oveqan12d 7428 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ)) β (βͺ
π½ βm βͺ πΏ) =
(π βm π)) |
23 | 20 | adantr 482 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ)) β βͺ π½ = π) |
24 | 23 | oveq1d 7424 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ)) β (βͺ
π½ FilMap π) = (π FilMap π)) |
25 | 24 | fveq1d 6894 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ)) β ((βͺ
π½ FilMap π)βπΏ) = ((π FilMap π)βπΏ)) |
26 | 25 | oveq2d 7425 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ)) β (π½ fLim ((βͺ π½ FilMap π)βπΏ)) = (π½ fLim ((π FilMap π)βπΏ))) |
27 | 22, 26 | mpteq12dv 5240 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ)) β (π β (βͺ π½ βm βͺ πΏ)
β¦ (π½ fLim ((βͺ π½
FilMap π)βπΏ))) = (π β (π βm π) β¦ (π½ fLim ((π FilMap π)βπΏ)))) |
28 | 18, 27 | eqtrd 2773 |
1
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ)) β (π½ fLimf πΏ) = (π β (π βm π) β¦ (π½ fLim ((π FilMap π)βπΏ)))) |