Step | Hyp | Ref
| Expression |
1 | | cnpf2 22617 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΉ:πβΆπ) |
2 | 1 | 3expa 1119 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΉ:πβΆπ) |
3 | 2 | 3adantl3 1169 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΉ:πβΆπ) |
4 | | topontop 22278 |
. . . . . . 7
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
5 | | cnpfcfi 23407 |
. . . . . . . . 9
β’ ((πΎ β Top β§ π΄ β (π½ fClus π) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)) |
6 | 5 | 3com23 1127 |
. . . . . . . 8
β’ ((πΎ β Top β§ πΉ β ((π½ CnP πΎ)βπ΄) β§ π΄ β (π½ fClus π)) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)) |
7 | 6 | 3expia 1122 |
. . . . . . 7
β’ ((πΎ β Top β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ))) |
8 | 4, 7 | sylan 581 |
. . . . . 6
β’ ((πΎ β (TopOnβπ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ))) |
9 | 8 | ralrimivw 3144 |
. . . . 5
β’ ((πΎ β (TopOnβπ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ))) |
10 | 9 | 3ad2antl2 1187 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ))) |
11 | 3, 10 | jca 513 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (πΉ:πβΆπ β§ βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)))) |
12 | 11 | ex 414 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ))))) |
13 | | simplrl 776 |
. . . . . . . . . . . . . 14
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β π β (Filβπ)) |
14 | | filfbas 23215 |
. . . . . . . . . . . . . 14
β’ (π β (Filβπ) β π β (fBasβπ)) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β π β (fBasβπ)) |
16 | | simprl 770 |
. . . . . . . . . . . . 13
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β β β (Filβπ)) |
17 | | simpllr 775 |
. . . . . . . . . . . . 13
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β πΉ:πβΆπ) |
18 | | simprr 772 |
. . . . . . . . . . . . 13
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β ((π FilMap πΉ)βπ) β β) |
19 | 15, 16, 17, 18 | fmfnfm 23325 |
. . . . . . . . . . . 12
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β βπ β (Filβπ)(π β π β§ β = ((π FilMap πΉ)βπ))) |
20 | | r19.29 3114 |
. . . . . . . . . . . . 13
β’
((βπ β
(Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)) β§ βπ β (Filβπ)(π β π β§ β = ((π FilMap πΉ)βπ))) β βπ β (Filβπ)((π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)) β§ (π β π β§ β = ((π FilMap πΉ)βπ)))) |
21 | | flimfcls 23393 |
. . . . . . . . . . . . . . . . . 18
β’ (π½ fLim π) β (π½ fClus π) |
22 | | simpll1 1213 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β π½ β (TopOnβπ)) |
23 | 22 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ (π β (Filβπ) β§ (π β π β§ β = ((π FilMap πΉ)βπ)))) β π½ β (TopOnβπ)) |
24 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ (π β (Filβπ) β§ (π β π β§ β = ((π FilMap πΉ)βπ)))) β π β (Filβπ)) |
25 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ (π β (Filβπ) β§ (π β π β§ β = ((π FilMap πΉ)βπ)))) β π β π) |
26 | | flimss2 23339 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π½ β (TopOnβπ) β§ π β (Filβπ) β§ π β π) β (π½ fLim π) β (π½ fLim π)) |
27 | 23, 24, 25, 26 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ (π β (Filβπ) β§ (π β π β§ β = ((π FilMap πΉ)βπ)))) β (π½ fLim π) β (π½ fLim π)) |
28 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β π΄ β (π½ fLim π)) |
29 | 28 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ (π β (Filβπ) β§ (π β π β§ β = ((π FilMap πΉ)βπ)))) β π΄ β (π½ fLim π)) |
30 | 27, 29 | sseldd 3946 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ (π β (Filβπ) β§ (π β π β§ β = ((π FilMap πΉ)βπ)))) β π΄ β (π½ fLim π)) |
31 | 21, 30 | sselid 3943 |
. . . . . . . . . . . . . . . . 17
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ (π β (Filβπ) β§ (π β π β§ β = ((π FilMap πΉ)βπ)))) β π΄ β (π½ fClus π)) |
32 | | simpll2 1214 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β πΎ β (TopOnβπ)) |
33 | 32 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ (π β (Filβπ) β§ (π β π β§ β = ((π FilMap πΉ)βπ)))) β πΎ β (TopOnβπ)) |
34 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β πΉ:πβΆπ) |
35 | 34 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ (π β (Filβπ) β§ (π β π β§ β = ((π FilMap πΉ)βπ)))) β πΉ:πβΆπ) |
36 | | fcfval 23400 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΎ β (TopOnβπ) β§ π β (Filβπ) β§ πΉ:πβΆπ) β ((πΎ fClusf π)βπΉ) = (πΎ fClus ((π FilMap πΉ)βπ))) |
37 | 33, 24, 35, 36 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ (π β (Filβπ) β§ (π β π β§ β = ((π FilMap πΉ)βπ)))) β ((πΎ fClusf π)βπΉ) = (πΎ fClus ((π FilMap πΉ)βπ))) |
38 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ (π β (Filβπ) β§ (π β π β§ β = ((π FilMap πΉ)βπ)))) β β = ((π FilMap πΉ)βπ)) |
39 | 38 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ (π β (Filβπ) β§ (π β π β§ β = ((π FilMap πΉ)βπ)))) β (πΎ fClus β) = (πΎ fClus ((π FilMap πΉ)βπ))) |
40 | 37, 39 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ (π β (Filβπ) β§ (π β π β§ β = ((π FilMap πΉ)βπ)))) β ((πΎ fClusf π)βπΉ) = (πΎ fClus β)) |
41 | 40 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ (π β (Filβπ) β§ (π β π β§ β = ((π FilMap πΉ)βπ)))) β ((πΉβπ΄) β ((πΎ fClusf π)βπΉ) β (πΉβπ΄) β (πΎ fClus β))) |
42 | 41 | biimpd 228 |
. . . . . . . . . . . . . . . . 17
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ (π β (Filβπ) β§ (π β π β§ β = ((π FilMap πΉ)βπ)))) β ((πΉβπ΄) β ((πΎ fClusf π)βπΉ) β (πΉβπ΄) β (πΎ fClus β))) |
43 | 31, 42 | embantd 59 |
. . . . . . . . . . . . . . . 16
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ (π β (Filβπ) β§ (π β π β§ β = ((π FilMap πΉ)βπ)))) β ((π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)) β (πΉβπ΄) β (πΎ fClus β))) |
44 | 43 | expr 458 |
. . . . . . . . . . . . . . 15
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ π β (Filβπ)) β ((π β π β§ β = ((π FilMap πΉ)βπ)) β ((π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)) β (πΉβπ΄) β (πΎ fClus β)))) |
45 | 44 | impcomd 413 |
. . . . . . . . . . . . . 14
β’
((((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β§ π β (Filβπ)) β (((π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)) β§ (π β π β§ β = ((π FilMap πΉ)βπ))) β (πΉβπ΄) β (πΎ fClus β))) |
46 | 45 | rexlimdva 3149 |
. . . . . . . . . . . . 13
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β (βπ β (Filβπ)((π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)) β§ (π β π β§ β = ((π FilMap πΉ)βπ))) β (πΉβπ΄) β (πΎ fClus β))) |
47 | 20, 46 | syl5 34 |
. . . . . . . . . . . 12
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β ((βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)) β§ βπ β (Filβπ)(π β π β§ β = ((π FilMap πΉ)βπ))) β (πΉβπ΄) β (πΎ fClus β))) |
48 | 19, 47 | mpan2d 693 |
. . . . . . . . . . 11
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ (β β (Filβπ) β§ ((π FilMap πΉ)βπ) β β)) β (βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)) β (πΉβπ΄) β (πΎ fClus β))) |
49 | 48 | expr 458 |
. . . . . . . . . 10
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ β β (Filβπ)) β (((π FilMap πΉ)βπ) β β β (βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)) β (πΉβπ΄) β (πΎ fClus β)))) |
50 | 49 | com23 86 |
. . . . . . . . 9
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β§ β β (Filβπ)) β (βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)) β (((π FilMap πΉ)βπ) β β β (πΉβπ΄) β (πΎ fClus β)))) |
51 | 50 | ralrimdva 3148 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β (βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)) β ββ β (Filβπ)(((π FilMap πΉ)βπ) β β β (πΉβπ΄) β (πΎ fClus β)))) |
52 | | toponmax 22291 |
. . . . . . . . . . . . 13
β’ (πΎ β (TopOnβπ) β π β πΎ) |
53 | 32, 52 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β π β πΎ) |
54 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β π β (Filβπ)) |
55 | 54, 14 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β π β (fBasβπ)) |
56 | | fmfil 23311 |
. . . . . . . . . . . 12
β’ ((π β πΎ β§ π β (fBasβπ) β§ πΉ:πβΆπ) β ((π FilMap πΉ)βπ) β (Filβπ)) |
57 | 53, 55, 34, 56 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β ((π FilMap πΉ)βπ) β (Filβπ)) |
58 | | toponuni 22279 |
. . . . . . . . . . . . 13
β’ (πΎ β (TopOnβπ) β π = βͺ πΎ) |
59 | 32, 58 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β π = βͺ πΎ) |
60 | 59 | fveq2d 6847 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β (Filβπ) = (Filββͺ
πΎ)) |
61 | 57, 60 | eleqtrd 2836 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β ((π FilMap πΉ)βπ) β (Filββͺ πΎ)) |
62 | | eqid 2733 |
. . . . . . . . . . 11
β’ βͺ πΎ =
βͺ πΎ |
63 | 62 | flimfnfcls 23395 |
. . . . . . . . . 10
β’ (((π FilMap πΉ)βπ) β (Filββͺ πΎ)
β ((πΉβπ΄) β (πΎ fLim ((π FilMap πΉ)βπ)) β ββ β (Filββͺ πΎ)(((π FilMap πΉ)βπ) β β β (πΉβπ΄) β (πΎ fClus β)))) |
64 | 61, 63 | syl 17 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β ((πΉβπ΄) β (πΎ fLim ((π FilMap πΉ)βπ)) β ββ β (Filββͺ πΎ)(((π FilMap πΉ)βπ) β β β (πΉβπ΄) β (πΎ fClus β)))) |
65 | | flfval 23357 |
. . . . . . . . . . 11
β’ ((πΎ β (TopOnβπ) β§ π β (Filβπ) β§ πΉ:πβΆπ) β ((πΎ fLimf π)βπΉ) = (πΎ fLim ((π FilMap πΉ)βπ))) |
66 | 32, 54, 34, 65 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β ((πΎ fLimf π)βπΉ) = (πΎ fLim ((π FilMap πΉ)βπ))) |
67 | 66 | eleq2d 2820 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β ((πΉβπ΄) β ((πΎ fLimf π)βπΉ) β (πΉβπ΄) β (πΎ fLim ((π FilMap πΉ)βπ)))) |
68 | 60 | raleqdv 3312 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β (ββ β (Filβπ)(((π FilMap πΉ)βπ) β β β (πΉβπ΄) β (πΎ fClus β)) β ββ β (Filββͺ πΎ)(((π FilMap πΉ)βπ) β β β (πΉβπ΄) β (πΎ fClus β)))) |
69 | 64, 67, 68 | 3bitr4d 311 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β ((πΉβπ΄) β ((πΎ fLimf π)βπΉ) β ββ β (Filβπ)(((π FilMap πΉ)βπ) β β β (πΉβπ΄) β (πΎ fClus β)))) |
70 | 51, 69 | sylibrd 259 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ (π β (Filβπ) β§ π΄ β (π½ fLim π))) β (βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ))) |
71 | 70 | expr 458 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ π β (Filβπ)) β (π΄ β (π½ fLim π) β (βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ)))) |
72 | 71 | com23 86 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β§ π β (Filβπ)) β (βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)) β (π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ)))) |
73 | 72 | ralrimdva 3148 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β (βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ)) β βπ β (Filβπ)(π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ)))) |
74 | 73 | imdistanda 573 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β ((πΉ:πβΆπ β§ βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ))) β (πΉ:πβΆπ β§ βπ β (Filβπ)(π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ))))) |
75 | | cnpflf 23368 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β (Filβπ)(π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ))))) |
76 | 74, 75 | sylibrd 259 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β ((πΉ:πβΆπ β§ βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ))) β πΉ β ((π½ CnP πΎ)βπ΄))) |
77 | 12, 76 | impbid 211 |
1
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ))))) |