Step | Hyp | Ref
| Expression |
1 | | toponmax 22428 |
. . . . 5
β’ (π½ β (TopOnβπ) β π β π½) |
2 | | filtop 23359 |
. . . . 5
β’ (πΏ β (Filβπ) β π β πΏ) |
3 | | elmapg 8833 |
. . . . 5
β’ ((π β π½ β§ π β πΏ) β (πΉ β (π βm π) β πΉ:πβΆπ)) |
4 | 1, 2, 3 | syl2an 597 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ)) β (πΉ β (π βm π) β πΉ:πβΆπ)) |
5 | 4 | biimpar 479 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ)) β§ πΉ:πβΆπ) β πΉ β (π βm π)) |
6 | | flffval 23493 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ)) β (π½ fLimf πΏ) = (π β (π βm π) β¦ (π½ fLim ((π FilMap π)βπΏ)))) |
7 | 6 | fveq1d 6894 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ)) β ((π½ fLimf πΏ)βπΉ) = ((π β (π βm π) β¦ (π½ fLim ((π FilMap π)βπΏ)))βπΉ)) |
8 | | oveq2 7417 |
. . . . . . 7
β’ (π = πΉ β (π FilMap π) = (π FilMap πΉ)) |
9 | 8 | fveq1d 6894 |
. . . . . 6
β’ (π = πΉ β ((π FilMap π)βπΏ) = ((π FilMap πΉ)βπΏ)) |
10 | 9 | oveq2d 7425 |
. . . . 5
β’ (π = πΉ β (π½ fLim ((π FilMap π)βπΏ)) = (π½ fLim ((π FilMap πΉ)βπΏ))) |
11 | | eqid 2733 |
. . . . 5
β’ (π β (π βm π) β¦ (π½ fLim ((π FilMap π)βπΏ))) = (π β (π βm π) β¦ (π½ fLim ((π FilMap π)βπΏ))) |
12 | | ovex 7442 |
. . . . 5
β’ (π½ fLim ((π FilMap πΉ)βπΏ)) β V |
13 | 10, 11, 12 | fvmpt 6999 |
. . . 4
β’ (πΉ β (π βm π) β ((π β (π βm π) β¦ (π½ fLim ((π FilMap π)βπΏ)))βπΉ) = (π½ fLim ((π FilMap πΉ)βπΏ))) |
14 | 7, 13 | sylan9eq 2793 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ)) β§ πΉ β (π βm π)) β ((π½ fLimf πΏ)βπΉ) = (π½ fLim ((π FilMap πΉ)βπΏ))) |
15 | 5, 14 | syldan 592 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ)) β§ πΉ:πβΆπ) β ((π½ fLimf πΏ)βπΉ) = (π½ fLim ((π FilMap πΉ)βπΏ))) |
16 | 15 | 3impa 1111 |
1
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β ((π½ fLimf πΏ)βπΉ) = (π½ fLim ((π FilMap πΉ)βπΏ))) |