Step | Hyp | Ref
| Expression |
1 | | tsmscls.x |
. . . 4
β’ (π β π β (πΊ tsums πΉ)) |
2 | | tsmscls.b |
. . . . . 6
β’ π΅ = (BaseβπΊ) |
3 | | tsmscls.j |
. . . . . 6
β’ π½ = (TopOpenβπΊ) |
4 | | eqid 2733 |
. . . . . 6
β’
(π« π΄ β©
Fin) = (π« π΄ β©
Fin) |
5 | | eqid 2733 |
. . . . . 6
β’ ran
(π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦}) = ran (π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦}) |
6 | | tsmscls.2 |
. . . . . 6
β’ (π β πΊ β TopSp) |
7 | | tsmscls.a |
. . . . . 6
β’ (π β π΄ β π) |
8 | | tsmscls.f |
. . . . . 6
β’ (π β πΉ:π΄βΆπ΅) |
9 | 2, 3, 4, 5, 6, 7, 8 | tsmsval 23498 |
. . . . 5
β’ (π β (πΊ tsums πΉ) = ((π½ fLimf ((π« π΄ β© Fin)filGenran (π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦})))β(π¦ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π¦))))) |
10 | 2, 3 | istps 22299 |
. . . . . . 7
β’ (πΊ β TopSp β π½ β (TopOnβπ΅)) |
11 | 6, 10 | sylib 217 |
. . . . . 6
β’ (π β π½ β (TopOnβπ΅)) |
12 | | eqid 2733 |
. . . . . . . 8
β’ (π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦}) = (π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦}) |
13 | 4, 12, 5, 7 | tsmsfbas 23495 |
. . . . . . 7
β’ (π β ran (π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦}) β (fBasβ(π« π΄ β© Fin))) |
14 | | fgcl 23245 |
. . . . . . 7
β’ (ran
(π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦}) β (fBasβ(π« π΄ β© Fin)) β ((π«
π΄ β© Fin)filGenran
(π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦})) β (Filβ(π« π΄ β© Fin))) |
15 | 13, 14 | syl 17 |
. . . . . 6
β’ (π β ((π« π΄ β© Fin)filGenran (π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦})) β (Filβ(π« π΄ β© Fin))) |
16 | | tsmscls.1 |
. . . . . . . 8
β’ (π β πΊ β CMnd) |
17 | 2, 4, 16, 7, 8 | tsmslem1 23496 |
. . . . . . 7
β’ ((π β§ π¦ β (π« π΄ β© Fin)) β (πΊ Ξ£g (πΉ βΎ π¦)) β π΅) |
18 | 17 | fmpttd 7064 |
. . . . . 6
β’ (π β (π¦ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π¦))):(π« π΄ β© Fin)βΆπ΅) |
19 | | flfval 23357 |
. . . . . 6
β’ ((π½ β (TopOnβπ΅) β§ ((π« π΄ β© Fin)filGenran (π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦})) β (Filβ(π« π΄ β© Fin)) β§ (π¦ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π¦))):(π« π΄ β© Fin)βΆπ΅) β ((π½ fLimf ((π« π΄ β© Fin)filGenran (π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦})))β(π¦ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π¦)))) = (π½ fLim ((π΅ FilMap (π¦ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π¦))))β((π« π΄ β© Fin)filGenran (π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦}))))) |
20 | 11, 15, 18, 19 | syl3anc 1372 |
. . . . 5
β’ (π β ((π½ fLimf ((π« π΄ β© Fin)filGenran (π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦})))β(π¦ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π¦)))) = (π½ fLim ((π΅ FilMap (π¦ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π¦))))β((π« π΄ β© Fin)filGenran (π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦}))))) |
21 | 9, 20 | eqtrd 2773 |
. . . 4
β’ (π β (πΊ tsums πΉ) = (π½ fLim ((π΅ FilMap (π¦ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π¦))))β((π« π΄ β© Fin)filGenran (π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦}))))) |
22 | 1, 21 | eleqtrd 2836 |
. . 3
β’ (π β π β (π½ fLim ((π΅ FilMap (π¦ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π¦))))β((π« π΄ β© Fin)filGenran (π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦}))))) |
23 | | flimsncls 23353 |
. . 3
β’ (π β (π½ fLim ((π΅ FilMap (π¦ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π¦))))β((π« π΄ β© Fin)filGenran (π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦})))) β ((clsβπ½)β{π}) β (π½ fLim ((π΅ FilMap (π¦ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π¦))))β((π« π΄ β© Fin)filGenran (π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦}))))) |
24 | 22, 23 | syl 17 |
. 2
β’ (π β ((clsβπ½)β{π}) β (π½ fLim ((π΅ FilMap (π¦ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π¦))))β((π« π΄ β© Fin)filGenran (π₯ β (π« π΄ β© Fin) β¦ {π¦ β (π« π΄ β© Fin) β£ π₯ β π¦}))))) |
25 | 24, 21 | sseqtrrd 3986 |
1
β’ (π β ((clsβπ½)β{π}) β (πΊ tsums πΉ)) |