Step | Hyp | Ref
| Expression |
1 | | eltsms.b |
. . . 4
β’ π΅ = (BaseβπΊ) |
2 | | eltsms.j |
. . . 4
β’ π½ = (TopOpenβπΊ) |
3 | | eltsms.s |
. . . 4
β’ π = (π« π΄ β© Fin) |
4 | | eqid 2733 |
. . . 4
β’ ran
(π§ β π β¦ {π¦ β π β£ π§ β π¦}) = ran (π§ β π β¦ {π¦ β π β£ π§ β π¦}) |
5 | | eltsms.1 |
. . . 4
β’ (π β πΊ β CMnd) |
6 | | eltsms.a |
. . . 4
β’ (π β π΄ β π) |
7 | | eltsms.f |
. . . 4
β’ (π β πΉ:π΄βΆπ΅) |
8 | 1, 2, 3, 4, 5, 6, 7 | tsmsval 23498 |
. . 3
β’ (π β (πΊ tsums πΉ) = ((π½ fLimf (πfilGenran (π§ β π β¦ {π¦ β π β£ π§ β π¦})))β(π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))))) |
9 | 8 | eleq2d 2820 |
. 2
β’ (π β (πΆ β (πΊ tsums πΉ) β πΆ β ((π½ fLimf (πfilGenran (π§ β π β¦ {π¦ β π β£ π§ β π¦})))β(π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦)))))) |
10 | | eltsms.2 |
. . . 4
β’ (π β πΊ β TopSp) |
11 | 1, 2 | istps 22299 |
. . . 4
β’ (πΊ β TopSp β π½ β (TopOnβπ΅)) |
12 | 10, 11 | sylib 217 |
. . 3
β’ (π β π½ β (TopOnβπ΅)) |
13 | | eqid 2733 |
. . . 4
β’ (π§ β π β¦ {π¦ β π β£ π§ β π¦}) = (π§ β π β¦ {π¦ β π β£ π§ β π¦}) |
14 | 3, 13, 4, 6 | tsmsfbas 23495 |
. . 3
β’ (π β ran (π§ β π β¦ {π¦ β π β£ π§ β π¦}) β (fBasβπ)) |
15 | 1, 3, 5, 6, 7 | tsmslem1 23496 |
. . . 4
β’ ((π β§ π¦ β π) β (πΊ Ξ£g (πΉ βΎ π¦)) β π΅) |
16 | 15 | fmpttd 7064 |
. . 3
β’ (π β (π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))):πβΆπ΅) |
17 | | eqid 2733 |
. . . 4
β’ (πfilGenran (π§ β π β¦ {π¦ β π β£ π§ β π¦})) = (πfilGenran (π§ β π β¦ {π¦ β π β£ π§ β π¦})) |
18 | 17 | flffbas 23362 |
. . 3
β’ ((π½ β (TopOnβπ΅) β§ ran (π§ β π β¦ {π¦ β π β£ π§ β π¦}) β (fBasβπ) β§ (π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))):πβΆπ΅) β (πΆ β ((π½ fLimf (πfilGenran (π§ β π β¦ {π¦ β π β£ π§ β π¦})))β(π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦)))) β (πΆ β π΅ β§ βπ’ β π½ (πΆ β π’ β βπ€ β ran (π§ β π β¦ {π¦ β π β£ π§ β π¦})((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β π€) β π’)))) |
19 | 12, 14, 16, 18 | syl3anc 1372 |
. 2
β’ (π β (πΆ β ((π½ fLimf (πfilGenran (π§ β π β¦ {π¦ β π β£ π§ β π¦})))β(π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦)))) β (πΆ β π΅ β§ βπ’ β π½ (πΆ β π’ β βπ€ β ran (π§ β π β¦ {π¦ β π β£ π§ β π¦})((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β π€) β π’)))) |
20 | | pwexg 5334 |
. . . . . . . . . . . 12
β’ (π΄ β π β π« π΄ β V) |
21 | | inex1g 5277 |
. . . . . . . . . . . 12
β’
(π« π΄ β
V β (π« π΄ β©
Fin) β V) |
22 | 6, 20, 21 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β (π« π΄ β© Fin) β
V) |
23 | 3, 22 | eqeltrid 2838 |
. . . . . . . . . 10
β’ (π β π β V) |
24 | 23 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π’ β π½) β π β V) |
25 | | rabexg 5289 |
. . . . . . . . 9
β’ (π β V β {π¦ β π β£ π§ β π¦} β V) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
β’ ((π β§ π’ β π½) β {π¦ β π β£ π§ β π¦} β V) |
27 | 26 | ralrimivw 3144 |
. . . . . . 7
β’ ((π β§ π’ β π½) β βπ§ β π {π¦ β π β£ π§ β π¦} β V) |
28 | | imaeq2 6010 |
. . . . . . . . 9
β’ (π€ = {π¦ β π β£ π§ β π¦} β ((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β π€) = ((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β {π¦ β π β£ π§ β π¦})) |
29 | 28 | sseq1d 3976 |
. . . . . . . 8
β’ (π€ = {π¦ β π β£ π§ β π¦} β (((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β π€) β π’ β ((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β {π¦ β π β£ π§ β π¦}) β π’)) |
30 | 13, 29 | rexrnmptw 7046 |
. . . . . . 7
β’
(βπ§ β
π {π¦ β π β£ π§ β π¦} β V β (βπ€ β ran (π§ β π β¦ {π¦ β π β£ π§ β π¦})((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β π€) β π’ β βπ§ β π ((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β {π¦ β π β£ π§ β π¦}) β π’)) |
31 | 27, 30 | syl 17 |
. . . . . 6
β’ ((π β§ π’ β π½) β (βπ€ β ran (π§ β π β¦ {π¦ β π β£ π§ β π¦})((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β π€) β π’ β βπ§ β π ((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β {π¦ β π β£ π§ β π¦}) β π’)) |
32 | | funmpt 6540 |
. . . . . . . . 9
β’ Fun
(π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) |
33 | | ssrab2 4038 |
. . . . . . . . . 10
β’ {π¦ β π β£ π§ β π¦} β π |
34 | | ovex 7391 |
. . . . . . . . . . 11
β’ (πΊ Ξ£g
(πΉ βΎ π¦)) β V |
35 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) = (π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) |
36 | 34, 35 | dmmpti 6646 |
. . . . . . . . . 10
β’ dom
(π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) = π |
37 | 33, 36 | sseqtrri 3982 |
. . . . . . . . 9
β’ {π¦ β π β£ π§ β π¦} β dom (π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) |
38 | | funimass3 7005 |
. . . . . . . . 9
β’ ((Fun
(π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β§ {π¦ β π β£ π§ β π¦} β dom (π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦)))) β (((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β {π¦ β π β£ π§ β π¦}) β π’ β {π¦ β π β£ π§ β π¦} β (β‘(π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β π’))) |
39 | 32, 37, 38 | mp2an 691 |
. . . . . . . 8
β’ (((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β {π¦ β π β£ π§ β π¦}) β π’ β {π¦ β π β£ π§ β π¦} β (β‘(π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β π’)) |
40 | 35 | mptpreima 6191 |
. . . . . . . . 9
β’ (β‘(π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β π’) = {π¦ β π β£ (πΊ Ξ£g (πΉ βΎ π¦)) β π’} |
41 | 40 | sseq2i 3974 |
. . . . . . . 8
β’ ({π¦ β π β£ π§ β π¦} β (β‘(π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β π’) β {π¦ β π β£ π§ β π¦} β {π¦ β π β£ (πΊ Ξ£g (πΉ βΎ π¦)) β π’}) |
42 | | ss2rab 4029 |
. . . . . . . 8
β’ ({π¦ β π β£ π§ β π¦} β {π¦ β π β£ (πΊ Ξ£g (πΉ βΎ π¦)) β π’} β βπ¦ β π (π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’)) |
43 | 39, 41, 42 | 3bitri 297 |
. . . . . . 7
β’ (((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β {π¦ β π β£ π§ β π¦}) β π’ β βπ¦ β π (π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’)) |
44 | 43 | rexbii 3094 |
. . . . . 6
β’
(βπ§ β
π ((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β {π¦ β π β£ π§ β π¦}) β π’ β βπ§ β π βπ¦ β π (π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’)) |
45 | 31, 44 | bitrdi 287 |
. . . . 5
β’ ((π β§ π’ β π½) β (βπ€ β ran (π§ β π β¦ {π¦ β π β£ π§ β π¦})((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β π€) β π’ β βπ§ β π βπ¦ β π (π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’))) |
46 | 45 | imbi2d 341 |
. . . 4
β’ ((π β§ π’ β π½) β ((πΆ β π’ β βπ€ β ran (π§ β π β¦ {π¦ β π β£ π§ β π¦})((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β π€) β π’) β (πΆ β π’ β βπ§ β π βπ¦ β π (π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’)))) |
47 | 46 | ralbidva 3169 |
. . 3
β’ (π β (βπ’ β π½ (πΆ β π’ β βπ€ β ran (π§ β π β¦ {π¦ β π β£ π§ β π¦})((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β π€) β π’) β βπ’ β π½ (πΆ β π’ β βπ§ β π βπ¦ β π (π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’)))) |
48 | 47 | anbi2d 630 |
. 2
β’ (π β ((πΆ β π΅ β§ βπ’ β π½ (πΆ β π’ β βπ€ β ran (π§ β π β¦ {π¦ β π β£ π§ β π¦})((π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))) β π€) β π’)) β (πΆ β π΅ β§ βπ’ β π½ (πΆ β π’ β βπ§ β π βπ¦ β π (π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’))))) |
49 | 9, 19, 48 | 3bitrd 305 |
1
β’ (π β (πΆ β (πΊ tsums πΉ) β (πΆ β π΅ β§ βπ’ β π½ (πΆ β π’ β βπ§ β π βπ¦ β π (π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’))))) |