Step | Hyp | Ref
| Expression |
1 | | cncnp 22654 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯)))) |
2 | | simplr 768 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ π₯ β π) β πΉ:πβΆπ) |
3 | | cnpflf 23375 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π₯ β π) β (πΉ β ((π½ CnP πΎ)βπ₯) β (πΉ:πβΆπ β§ βπ β (Filβπ)(π₯ β (π½ fLim π) β (πΉβπ₯) β ((πΎ fLimf π)βπΉ))))) |
4 | 3 | ad4ant124 1174 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ π₯ β π) β (πΉ β ((π½ CnP πΎ)βπ₯) β (πΉ:πβΆπ β§ βπ β (Filβπ)(π₯ β (π½ fLim π) β (πΉβπ₯) β ((πΎ fLimf π)βπΉ))))) |
5 | 2, 4 | mpbirand 706 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ π₯ β π) β (πΉ β ((π½ CnP πΎ)βπ₯) β βπ β (Filβπ)(π₯ β (π½ fLim π) β (πΉβπ₯) β ((πΎ fLimf π)βπΉ)))) |
6 | 5 | ralbidva 3169 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β (βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯) β βπ₯ β π βπ β (Filβπ)(π₯ β (π½ fLim π) β (πΉβπ₯) β ((πΎ fLimf π)βπΉ)))) |
7 | | eqid 2733 |
. . . . . . . . . . . 12
β’ βͺ π½ =
βͺ π½ |
8 | 7 | flimelbas 23342 |
. . . . . . . . . . 11
β’ (π₯ β (π½ fLim π) β π₯ β βͺ π½) |
9 | | toponuni 22286 |
. . . . . . . . . . . . 13
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
10 | 9 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β π = βͺ π½) |
11 | 10 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β (π₯ β π β π₯ β βͺ π½)) |
12 | 8, 11 | syl5ibr 246 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β (π₯ β (π½ fLim π) β π₯ β π)) |
13 | 12 | pm4.71rd 564 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β (π₯ β (π½ fLim π) β (π₯ β π β§ π₯ β (π½ fLim π)))) |
14 | 13 | imbi1d 342 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β ((π₯ β (π½ fLim π) β (πΉβπ₯) β ((πΎ fLimf π)βπΉ)) β ((π₯ β π β§ π₯ β (π½ fLim π)) β (πΉβπ₯) β ((πΎ fLimf π)βπΉ)))) |
15 | | impexp 452 |
. . . . . . . 8
β’ (((π₯ β π β§ π₯ β (π½ fLim π)) β (πΉβπ₯) β ((πΎ fLimf π)βπΉ)) β (π₯ β π β (π₯ β (π½ fLim π) β (πΉβπ₯) β ((πΎ fLimf π)βπΉ)))) |
16 | 14, 15 | bitrdi 287 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β ((π₯ β (π½ fLim π) β (πΉβπ₯) β ((πΎ fLimf π)βπΉ)) β (π₯ β π β (π₯ β (π½ fLim π) β (πΉβπ₯) β ((πΎ fLimf π)βπΉ))))) |
17 | 16 | ralbidv2 3167 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β (βπ₯ β (π½ fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ) β βπ₯ β π (π₯ β (π½ fLim π) β (πΉβπ₯) β ((πΎ fLimf π)βπΉ)))) |
18 | 17 | ralbidv 3171 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β (βπ β (Filβπ)βπ₯ β (π½ fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ) β βπ β (Filβπ)βπ₯ β π (π₯ β (π½ fLim π) β (πΉβπ₯) β ((πΎ fLimf π)βπΉ)))) |
19 | | ralcom 3271 |
. . . . 5
β’
(βπ β
(Filβπ)βπ₯ β π (π₯ β (π½ fLim π) β (πΉβπ₯) β ((πΎ fLimf π)βπΉ)) β βπ₯ β π βπ β (Filβπ)(π₯ β (π½ fLim π) β (πΉβπ₯) β ((πΎ fLimf π)βπΉ))) |
20 | 18, 19 | bitrdi 287 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β (βπ β (Filβπ)βπ₯ β (π½ fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ) β βπ₯ β π βπ β (Filβπ)(π₯ β (π½ fLim π) β (πΉβπ₯) β ((πΎ fLimf π)βπΉ)))) |
21 | 6, 20 | bitr4d 282 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β (βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯) β βπ β (Filβπ)βπ₯ β (π½ fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ))) |
22 | 21 | pm5.32da 580 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β ((πΉ:πβΆπ β§ βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯)) β (πΉ:πβΆπ β§ βπ β (Filβπ)βπ₯ β (π½ fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ)))) |
23 | 1, 22 | bitrd 279 |
1
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ β (Filβπ)βπ₯ β (π½ fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ)))) |