Step | Hyp | Ref
| Expression |
1 | | simprl 770 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β π΄ β ((π½ fLimf πΏ)βπΉ)) |
2 | | flfval 23357 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β ((π½ fLimf πΏ)βπΉ) = (π½ fLim ((π FilMap πΉ)βπΏ))) |
3 | 2 | adantr 482 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β ((π½ fLimf πΏ)βπΉ) = (π½ fLim ((π FilMap πΉ)βπΏ))) |
4 | 1, 3 | eleqtrd 2840 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β π΄ β (π½ fLim ((π FilMap πΉ)βπΏ))) |
5 | | simprr 772 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β πΊ β ((π½ CnP πΎ)βπ΄)) |
6 | | cnpflfi 23366 |
. . 3
β’ ((π΄ β (π½ fLim ((π FilMap πΉ)βπΏ)) β§ πΊ β ((π½ CnP πΎ)βπ΄)) β (πΊβπ΄) β ((πΎ fLimf ((π FilMap πΉ)βπΏ))βπΊ)) |
7 | 4, 5, 6 | syl2anc 585 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β (πΊβπ΄) β ((πΎ fLimf ((π FilMap πΉ)βπΏ))βπΊ)) |
8 | | cnptop2 22610 |
. . . . . . . 8
β’ (πΊ β ((π½ CnP πΎ)βπ΄) β πΎ β Top) |
9 | 8 | ad2antll 728 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β πΎ β Top) |
10 | | toptopon2 22283 |
. . . . . . 7
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
11 | 9, 10 | sylib 217 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β πΎ β (TopOnββͺ πΎ)) |
12 | | toponmax 22291 |
. . . . . 6
β’ (πΎ β (TopOnββͺ πΎ)
β βͺ πΎ β πΎ) |
13 | 11, 12 | syl 17 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β βͺ
πΎ β πΎ) |
14 | | simpl1 1192 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β π½ β (TopOnβπ)) |
15 | | toponmax 22291 |
. . . . . 6
β’ (π½ β (TopOnβπ) β π β π½) |
16 | 14, 15 | syl 17 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β π β π½) |
17 | | simpl2 1193 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β πΏ β (Filβπ)) |
18 | | filfbas 23215 |
. . . . . 6
β’ (πΏ β (Filβπ) β πΏ β (fBasβπ)) |
19 | 17, 18 | syl 17 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β πΏ β (fBasβπ)) |
20 | | cnpf2 22617 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnββͺ πΎ)
β§ πΊ β ((π½ CnP πΎ)βπ΄)) β πΊ:πβΆβͺ πΎ) |
21 | 14, 11, 5, 20 | syl3anc 1372 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β πΊ:πβΆβͺ πΎ) |
22 | | simpl3 1194 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β πΉ:πβΆπ) |
23 | | fmco 23328 |
. . . . 5
β’ (((βͺ πΎ
β πΎ β§ π β π½ β§ πΏ β (fBasβπ)) β§ (πΊ:πβΆβͺ πΎ β§ πΉ:πβΆπ)) β ((βͺ
πΎ FilMap (πΊ β πΉ))βπΏ) = ((βͺ πΎ FilMap πΊ)β((π FilMap πΉ)βπΏ))) |
24 | 13, 16, 19, 21, 22, 23 | syl32anc 1379 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β ((βͺ
πΎ FilMap (πΊ β πΉ))βπΏ) = ((βͺ πΎ FilMap πΊ)β((π FilMap πΉ)βπΏ))) |
25 | 24 | oveq2d 7378 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β (πΎ fLim ((βͺ πΎ FilMap (πΊ β πΉ))βπΏ)) = (πΎ fLim ((βͺ πΎ FilMap πΊ)β((π FilMap πΉ)βπΏ)))) |
26 | | fco 6697 |
. . . . 5
β’ ((πΊ:πβΆβͺ πΎ β§ πΉ:πβΆπ) β (πΊ β πΉ):πβΆβͺ πΎ) |
27 | 21, 22, 26 | syl2anc 585 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β (πΊ β πΉ):πβΆβͺ πΎ) |
28 | | flfval 23357 |
. . . 4
β’ ((πΎ β (TopOnββͺ πΎ)
β§ πΏ β
(Filβπ) β§ (πΊ β πΉ):πβΆβͺ πΎ) β ((πΎ fLimf πΏ)β(πΊ β πΉ)) = (πΎ fLim ((βͺ πΎ FilMap (πΊ β πΉ))βπΏ))) |
29 | 11, 17, 27, 28 | syl3anc 1372 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β ((πΎ fLimf πΏ)β(πΊ β πΉ)) = (πΎ fLim ((βͺ πΎ FilMap (πΊ β πΉ))βπΏ))) |
30 | | fmfil 23311 |
. . . . 5
β’ ((π β π½ β§ πΏ β (fBasβπ) β§ πΉ:πβΆπ) β ((π FilMap πΉ)βπΏ) β (Filβπ)) |
31 | 16, 19, 22, 30 | syl3anc 1372 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β ((π FilMap πΉ)βπΏ) β (Filβπ)) |
32 | | flfval 23357 |
. . . 4
β’ ((πΎ β (TopOnββͺ πΎ)
β§ ((π FilMap πΉ)βπΏ) β (Filβπ) β§ πΊ:πβΆβͺ πΎ) β ((πΎ fLimf ((π FilMap πΉ)βπΏ))βπΊ) = (πΎ fLim ((βͺ πΎ FilMap πΊ)β((π FilMap πΉ)βπΏ)))) |
33 | 11, 31, 21, 32 | syl3anc 1372 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β ((πΎ fLimf ((π FilMap πΉ)βπΏ))βπΊ) = (πΎ fLim ((βͺ πΎ FilMap πΊ)β((π FilMap πΉ)βπΏ)))) |
34 | 25, 29, 33 | 3eqtr4d 2787 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β ((πΎ fLimf πΏ)β(πΊ β πΉ)) = ((πΎ fLimf ((π FilMap πΉ)βπΏ))βπΊ)) |
35 | 7, 34 | eleqtrrd 2841 |
1
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β (πΊβπ΄) β ((πΎ fLimf πΏ)β(πΊ β πΉ))) |