Step | Hyp | Ref
| Expression |
1 | | haustsms.h |
. . 3
β’ (π β π½ β Haus) |
2 | | eqid 2733 |
. . . . 5
β’
(π« π΄ β©
Fin) = (π« π΄ β©
Fin) |
3 | | eqid 2733 |
. . . . 5
β’ (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§}) = (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§}) |
4 | | eqid 2733 |
. . . . 5
β’ ran
(π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§}) = ran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§}) |
5 | | tsmscl.a |
. . . . 5
β’ (π β π΄ β π) |
6 | 2, 3, 4, 5 | tsmsfbas 23495 |
. . . 4
β’ (π β ran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§}) β (fBasβ(π« π΄ β© Fin))) |
7 | | fgcl 23245 |
. . . 4
β’ (ran
(π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§}) β (fBasβ(π« π΄ β© Fin)) β ((π«
π΄ β© Fin)filGenran
(π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})) β (Filβ(π« π΄ β© Fin))) |
8 | 6, 7 | syl 17 |
. . 3
β’ (π β ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})) β (Filβ(π« π΄ β© Fin))) |
9 | | tsmscl.b |
. . . . . 6
β’ π΅ = (BaseβπΊ) |
10 | | tsmscl.1 |
. . . . . 6
β’ (π β πΊ β CMnd) |
11 | | tsmscl.f |
. . . . . 6
β’ (π β πΉ:π΄βΆπ΅) |
12 | 9, 2, 10, 5, 11 | tsmslem1 23496 |
. . . . 5
β’ ((π β§ π§ β (π« π΄ β© Fin)) β (πΊ Ξ£g (πΉ βΎ π§)) β π΅) |
13 | | tsmscl.2 |
. . . . . . 7
β’ (π β πΊ β TopSp) |
14 | | haustsms.j |
. . . . . . . 8
β’ π½ = (TopOpenβπΊ) |
15 | 9, 14 | tpsuni 22301 |
. . . . . . 7
β’ (πΊ β TopSp β π΅ = βͺ
π½) |
16 | 13, 15 | syl 17 |
. . . . . 6
β’ (π β π΅ = βͺ π½) |
17 | 16 | adantr 482 |
. . . . 5
β’ ((π β§ π§ β (π« π΄ β© Fin)) β π΅ = βͺ π½) |
18 | 12, 17 | eleqtrd 2836 |
. . . 4
β’ ((π β§ π§ β (π« π΄ β© Fin)) β (πΊ Ξ£g (πΉ βΎ π§)) β βͺ π½) |
19 | 18 | fmpttd 7064 |
. . 3
β’ (π β (π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π§))):(π« π΄ β© Fin)βΆβͺ π½) |
20 | | eqid 2733 |
. . . 4
β’ βͺ π½ =
βͺ π½ |
21 | 20 | hausflf 23364 |
. . 3
β’ ((π½ β Haus β§ ((π«
π΄ β© Fin)filGenran
(π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})) β (Filβ(π« π΄ β© Fin)) β§ (π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π§))):(π« π΄ β© Fin)βΆβͺ π½)
β β*π₯ π₯ β ((π½ fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π§))))) |
22 | 1, 8, 19, 21 | syl3anc 1372 |
. 2
β’ (π β β*π₯ π₯ β ((π½ fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π§))))) |
23 | 9, 14, 2, 4, 10, 5,
11 | tsmsval 23498 |
. . . 4
β’ (π β (πΊ tsums πΉ) = ((π½ fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π§))))) |
24 | 23 | eleq2d 2820 |
. . 3
β’ (π β (π₯ β (πΊ tsums πΉ) β π₯ β ((π½ fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π§)))))) |
25 | 24 | mobidv 2544 |
. 2
β’ (π β (β*π₯ π₯ β (πΊ tsums πΉ) β β*π₯ π₯ β ((π½ fLimf ((π« π΄ β© Fin)filGenran (π¦ β (π« π΄ β© Fin) β¦ {π§ β (π« π΄ β© Fin) β£ π¦ β π§})))β(π§ β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π§)))))) |
26 | 22, 25 | mpbird 257 |
1
β’ (π β β*π₯ π₯ β (πΊ tsums πΉ)) |