Step | Hyp | Ref
| Expression |
1 | | tsmsf1o.s |
. . . . . . . . . . 11
β’ (π β π»:πΆβ1-1-ontoβπ΄) |
2 | | f1opwfi 9303 |
. . . . . . . . . . 11
β’ (π»:πΆβ1-1-ontoβπ΄ β (π β (π« πΆ β© Fin) β¦ (π» β π)):(π« πΆ β© Fin)β1-1-ontoβ(π« π΄ β© Fin)) |
3 | 1, 2 | syl 17 |
. . . . . . . . . 10
β’ (π β (π β (π« πΆ β© Fin) β¦ (π» β π)):(π« πΆ β© Fin)β1-1-ontoβ(π« π΄ β© Fin)) |
4 | | f1of 6785 |
. . . . . . . . . 10
β’ ((π β (π« πΆ β© Fin) β¦ (π» β π)):(π« πΆ β© Fin)β1-1-ontoβ(π« π΄ β© Fin) β (π β (π« πΆ β© Fin) β¦ (π» β π)):(π« πΆ β© Fin)βΆ(π« π΄ β© Fin)) |
5 | 3, 4 | syl 17 |
. . . . . . . . 9
β’ (π β (π β (π« πΆ β© Fin) β¦ (π» β π)):(π« πΆ β© Fin)βΆ(π« π΄ β© Fin)) |
6 | | eqid 2733 |
. . . . . . . . . 10
β’ (π β (π« πΆ β© Fin) β¦ (π» β π)) = (π β (π« πΆ β© Fin) β¦ (π» β π)) |
7 | 6 | fmpt 7059 |
. . . . . . . . 9
β’
(βπ β
(π« πΆ β©
Fin)(π» β π) β (π« π΄ β© Fin) β (π β (π« πΆ β© Fin) β¦ (π» β π)):(π« πΆ β© Fin)βΆ(π« π΄ β© Fin)) |
8 | 5, 7 | sylibr 233 |
. . . . . . . 8
β’ (π β βπ β (π« πΆ β© Fin)(π» β π) β (π« π΄ β© Fin)) |
9 | | sseq1 3970 |
. . . . . . . . . . 11
β’ (π¦ = (π» β π) β (π¦ β π§ β (π» β π) β π§)) |
10 | 9 | imbi1d 342 |
. . . . . . . . . 10
β’ (π¦ = (π» β π) β ((π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β ((π» β π) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) |
11 | 10 | ralbidv 3171 |
. . . . . . . . 9
β’ (π¦ = (π» β π) β (βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β βπ§ β (π« π΄ β© Fin)((π» β π) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) |
12 | 6, 11 | rexrnmptw 7046 |
. . . . . . . 8
β’
(βπ β
(π« πΆ β©
Fin)(π» β π) β (π« π΄ β© Fin) β (βπ¦ β ran (π β (π« πΆ β© Fin) β¦ (π» β π))βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β βπ β (π« πΆ β© Fin)βπ§ β (π« π΄ β© Fin)((π» β π) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) |
13 | 8, 12 | syl 17 |
. . . . . . 7
β’ (π β (βπ¦ β ran (π β (π« πΆ β© Fin) β¦ (π» β π))βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β βπ β (π« πΆ β© Fin)βπ§ β (π« π΄ β© Fin)((π» β π) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) |
14 | | f1ofo 6792 |
. . . . . . . . 9
β’ ((π β (π« πΆ β© Fin) β¦ (π» β π)):(π« πΆ β© Fin)β1-1-ontoβ(π« π΄ β© Fin) β (π β (π« πΆ β© Fin) β¦ (π» β π)):(π« πΆ β© Fin)βontoβ(π« π΄ β© Fin)) |
15 | | forn 6760 |
. . . . . . . . 9
β’ ((π β (π« πΆ β© Fin) β¦ (π» β π)):(π« πΆ β© Fin)βontoβ(π« π΄ β© Fin) β ran (π β (π« πΆ β© Fin) β¦ (π» β π)) = (π« π΄ β© Fin)) |
16 | 3, 14, 15 | 3syl 18 |
. . . . . . . 8
β’ (π β ran (π β (π« πΆ β© Fin) β¦ (π» β π)) = (π« π΄ β© Fin)) |
17 | 16 | rexeqdv 3313 |
. . . . . . 7
β’ (π β (βπ¦ β ran (π β (π« πΆ β© Fin) β¦ (π» β π))βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) |
18 | | imaeq2 6010 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π» β π) = (π» β π)) |
19 | 18 | cbvmptv 5219 |
. . . . . . . . . . . . . 14
β’ (π β (π« πΆ β© Fin) β¦ (π» β π)) = (π β (π« πΆ β© Fin) β¦ (π» β π)) |
20 | 19 | fmpt 7059 |
. . . . . . . . . . . . 13
β’
(βπ β
(π« πΆ β©
Fin)(π» β π) β (π« π΄ β© Fin) β (π β (π« πΆ β© Fin) β¦ (π» β π)):(π« πΆ β© Fin)βΆ(π« π΄ β© Fin)) |
21 | 5, 20 | sylibr 233 |
. . . . . . . . . . . 12
β’ (π β βπ β (π« πΆ β© Fin)(π» β π) β (π« π΄ β© Fin)) |
22 | | sseq2 3971 |
. . . . . . . . . . . . . 14
β’ (π§ = (π» β π) β ((π» β π) β π§ β (π» β π) β (π» β π))) |
23 | | reseq2 5933 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (π» β π) β (πΉ βΎ π§) = (πΉ βΎ (π» β π))) |
24 | 23 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π» β π) β (πΊ Ξ£g (πΉ βΎ π§)) = (πΊ Ξ£g (πΉ βΎ (π» β π)))) |
25 | 24 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π§ = (π» β π) β ((πΊ Ξ£g (πΉ βΎ π§)) β π’ β (πΊ Ξ£g (πΉ βΎ (π» β π))) β π’)) |
26 | 22, 25 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π§ = (π» β π) β (((π» β π) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β ((π» β π) β (π» β π) β (πΊ Ξ£g (πΉ βΎ (π» β π))) β π’))) |
27 | 19, 26 | ralrnmptw 7045 |
. . . . . . . . . . . 12
β’
(βπ β
(π« πΆ β©
Fin)(π» β π) β (π« π΄ β© Fin) β
(βπ§ β ran
(π β (π« πΆ β© Fin) β¦ (π» β π))((π» β π) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β βπ β (π« πΆ β© Fin)((π» β π) β (π» β π) β (πΊ Ξ£g (πΉ βΎ (π» β π))) β π’))) |
28 | 21, 27 | syl 17 |
. . . . . . . . . . 11
β’ (π β (βπ§ β ran (π β (π« πΆ β© Fin) β¦ (π» β π))((π» β π) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β βπ β (π« πΆ β© Fin)((π» β π) β (π» β π) β (πΊ Ξ£g (πΉ βΎ (π» β π))) β π’))) |
29 | 16 | raleqdv 3312 |
. . . . . . . . . . 11
β’ (π β (βπ§ β ran (π β (π« πΆ β© Fin) β¦ (π» β π))((π» β π) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β βπ§ β (π« π΄ β© Fin)((π» β π) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) |
30 | 28, 29 | bitr3d 281 |
. . . . . . . . . 10
β’ (π β (βπ β (π« πΆ β© Fin)((π» β π) β (π» β π) β (πΊ Ξ£g (πΉ βΎ (π» β π))) β π’) β βπ§ β (π« π΄ β© Fin)((π» β π) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) |
31 | 30 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (π« πΆ β© Fin)) β (βπ β (π« πΆ β© Fin)((π» β π) β (π» β π) β (πΊ Ξ£g (πΉ βΎ (π» β π))) β π’) β βπ§ β (π« π΄ β© Fin)((π» β π) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) |
32 | | f1of1 6784 |
. . . . . . . . . . . . . 14
β’ (π»:πΆβ1-1-ontoβπ΄ β π»:πΆβ1-1βπ΄) |
33 | 1, 32 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π»:πΆβ1-1βπ΄) |
34 | 33 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β π»:πΆβ1-1βπ΄) |
35 | | elfpw 9301 |
. . . . . . . . . . . . . 14
β’ (π β (π« πΆ β© Fin) β (π β πΆ β§ π β Fin)) |
36 | 35 | simplbi 499 |
. . . . . . . . . . . . 13
β’ (π β (π« πΆ β© Fin) β π β πΆ) |
37 | 36 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β π β πΆ) |
38 | | elfpw 9301 |
. . . . . . . . . . . . . 14
β’ (π β (π« πΆ β© Fin) β (π β πΆ β§ π β Fin)) |
39 | 38 | simplbi 499 |
. . . . . . . . . . . . 13
β’ (π β (π« πΆ β© Fin) β π β πΆ) |
40 | 39 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β π β πΆ) |
41 | | f1imass 7212 |
. . . . . . . . . . . 12
β’ ((π»:πΆβ1-1βπ΄ β§ (π β πΆ β§ π β πΆ)) β ((π» β π) β (π» β π) β π β π)) |
42 | 34, 37, 40, 41 | syl12anc 836 |
. . . . . . . . . . 11
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β ((π» β π) β (π» β π) β π β π)) |
43 | | tsmsf1o.b |
. . . . . . . . . . . . . 14
β’ π΅ = (BaseβπΊ) |
44 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(0gβπΊ) = (0gβπΊ) |
45 | | tsmsf1o.1 |
. . . . . . . . . . . . . . 15
β’ (π β πΊ β CMnd) |
46 | 45 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β πΊ β CMnd) |
47 | | elinel2 4157 |
. . . . . . . . . . . . . . . 16
β’ (π β (π« πΆ β© Fin) β π β Fin) |
48 | 47 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β π β Fin) |
49 | | f1ores 6799 |
. . . . . . . . . . . . . . . . 17
β’ ((π»:πΆβ1-1βπ΄ β§ π β πΆ) β (π» βΎ π):πβ1-1-ontoβ(π» β π)) |
50 | 34, 40, 49 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β (π» βΎ π):πβ1-1-ontoβ(π» β π)) |
51 | | f1ofo 6792 |
. . . . . . . . . . . . . . . 16
β’ ((π» βΎ π):πβ1-1-ontoβ(π» β π) β (π» βΎ π):πβontoβ(π» β π)) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β (π» βΎ π):πβontoβ(π» β π)) |
53 | | fofi 9285 |
. . . . . . . . . . . . . . 15
β’ ((π β Fin β§ (π» βΎ π):πβontoβ(π» β π)) β (π» β π) β Fin) |
54 | 48, 52, 53 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β (π» β π) β Fin) |
55 | | tsmsf1o.f |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ:π΄βΆπ΅) |
56 | 55 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β πΉ:π΄βΆπ΅) |
57 | | imassrn 6025 |
. . . . . . . . . . . . . . . 16
β’ (π» β π) β ran π» |
58 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β π»:πΆβ1-1-ontoβπ΄) |
59 | | f1ofo 6792 |
. . . . . . . . . . . . . . . . 17
β’ (π»:πΆβ1-1-ontoβπ΄ β π»:πΆβontoβπ΄) |
60 | | forn 6760 |
. . . . . . . . . . . . . . . . 17
β’ (π»:πΆβontoβπ΄ β ran π» = π΄) |
61 | 58, 59, 60 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β ran π» = π΄) |
62 | 57, 61 | sseqtrid 3997 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β (π» β π) β π΄) |
63 | 56, 62 | fssresd 6710 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β (πΉ βΎ (π» β π)):(π» β π)βΆπ΅) |
64 | | fvexd 6858 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β
(0gβπΊ)
β V) |
65 | 63, 54, 64 | fdmfifsupp 9320 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β (πΉ βΎ (π» β π)) finSupp (0gβπΊ)) |
66 | 43, 44, 46, 54, 63, 65, 50 | gsumf1o 19698 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β (πΊ Ξ£g (πΉ βΎ (π» β π))) = (πΊ Ξ£g ((πΉ βΎ (π» β π)) β (π» βΎ π)))) |
67 | | df-ima 5647 |
. . . . . . . . . . . . . . . . 17
β’ (π» β π) = ran (π» βΎ π) |
68 | 67 | eqimss2i 4004 |
. . . . . . . . . . . . . . . 16
β’ ran
(π» βΎ π) β (π» β π) |
69 | | cores 6202 |
. . . . . . . . . . . . . . . 16
β’ (ran
(π» βΎ π) β (π» β π) β ((πΉ βΎ (π» β π)) β (π» βΎ π)) = (πΉ β (π» βΎ π))) |
70 | 68, 69 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ ((πΉ βΎ (π» β π)) β (π» βΎ π)) = (πΉ β (π» βΎ π)) |
71 | | resco 6203 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β π») βΎ π) = (πΉ β (π» βΎ π)) |
72 | 70, 71 | eqtr4i 2764 |
. . . . . . . . . . . . . 14
β’ ((πΉ βΎ (π» β π)) β (π» βΎ π)) = ((πΉ β π») βΎ π) |
73 | 72 | oveq2i 7369 |
. . . . . . . . . . . . 13
β’ (πΊ Ξ£g
((πΉ βΎ (π» β π)) β (π» βΎ π))) = (πΊ Ξ£g ((πΉ β π») βΎ π)) |
74 | 66, 73 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β (πΊ Ξ£g (πΉ βΎ (π» β π))) = (πΊ Ξ£g ((πΉ β π») βΎ π))) |
75 | 74 | eleq1d 2819 |
. . . . . . . . . . 11
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β ((πΊ Ξ£g (πΉ βΎ (π» β π))) β π’ β (πΊ Ξ£g ((πΉ β π») βΎ π)) β π’)) |
76 | 42, 75 | imbi12d 345 |
. . . . . . . . . 10
β’ (((π β§ π β (π« πΆ β© Fin)) β§ π β (π« πΆ β© Fin)) β (((π» β π) β (π» β π) β (πΊ Ξ£g (πΉ βΎ (π» β π))) β π’) β (π β π β (πΊ Ξ£g ((πΉ β π») βΎ π)) β π’))) |
77 | 76 | ralbidva 3169 |
. . . . . . . . 9
β’ ((π β§ π β (π« πΆ β© Fin)) β (βπ β (π« πΆ β© Fin)((π» β π) β (π» β π) β (πΊ Ξ£g (πΉ βΎ (π» β π))) β π’) β βπ β (π« πΆ β© Fin)(π β π β (πΊ Ξ£g ((πΉ β π») βΎ π)) β π’))) |
78 | 31, 77 | bitr3d 281 |
. . . . . . . 8
β’ ((π β§ π β (π« πΆ β© Fin)) β (βπ§ β (π« π΄ β© Fin)((π» β π) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β βπ β (π« πΆ β© Fin)(π β π β (πΊ Ξ£g ((πΉ β π») βΎ π)) β π’))) |
79 | 78 | rexbidva 3170 |
. . . . . . 7
β’ (π β (βπ β (π« πΆ β© Fin)βπ§ β (π« π΄ β© Fin)((π» β π) β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β βπ β (π« πΆ β© Fin)βπ β (π« πΆ β© Fin)(π β π β (πΊ Ξ£g ((πΉ β π») βΎ π)) β π’))) |
80 | 13, 17, 79 | 3bitr3d 309 |
. . . . . 6
β’ (π β (βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β βπ β (π« πΆ β© Fin)βπ β (π« πΆ β© Fin)(π β π β (πΊ Ξ£g ((πΉ β π») βΎ π)) β π’))) |
81 | 80 | imbi2d 341 |
. . . . 5
β’ (π β ((π₯ β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) β (π₯ β π’ β βπ β (π« πΆ β© Fin)βπ β (π« πΆ β© Fin)(π β π β (πΊ Ξ£g ((πΉ β π») βΎ π)) β π’)))) |
82 | 81 | ralbidv 3171 |
. . . 4
β’ (π β (βπ’ β (TopOpenβπΊ)(π₯ β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) β βπ’ β (TopOpenβπΊ)(π₯ β π’ β βπ β (π« πΆ β© Fin)βπ β (π« πΆ β© Fin)(π β π β (πΊ Ξ£g ((πΉ β π») βΎ π)) β π’)))) |
83 | 82 | anbi2d 630 |
. . 3
β’ (π β ((π₯ β π΅ β§ βπ’ β (TopOpenβπΊ)(π₯ β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) β (π₯ β π΅ β§ βπ’ β (TopOpenβπΊ)(π₯ β π’ β βπ β (π« πΆ β© Fin)βπ β (π« πΆ β© Fin)(π β π β (πΊ Ξ£g ((πΉ β π») βΎ π)) β π’))))) |
84 | | eqid 2733 |
. . . 4
β’
(TopOpenβπΊ) =
(TopOpenβπΊ) |
85 | | eqid 2733 |
. . . 4
β’
(π« π΄ β©
Fin) = (π« π΄ β©
Fin) |
86 | | tsmsf1o.2 |
. . . 4
β’ (π β πΊ β TopSp) |
87 | | tsmsf1o.a |
. . . 4
β’ (π β π΄ β π) |
88 | 43, 84, 85, 45, 86, 87, 55 | eltsms 23500 |
. . 3
β’ (π β (π₯ β (πΊ tsums πΉ) β (π₯ β π΅ β§ βπ’ β (TopOpenβπΊ)(π₯ β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))))) |
89 | | eqid 2733 |
. . . 4
β’
(π« πΆ β©
Fin) = (π« πΆ β©
Fin) |
90 | | f1dmex 7890 |
. . . . 5
β’ ((π»:πΆβ1-1βπ΄ β§ π΄ β π) β πΆ β V) |
91 | 33, 87, 90 | syl2anc 585 |
. . . 4
β’ (π β πΆ β V) |
92 | | f1of 6785 |
. . . . . 6
β’ (π»:πΆβ1-1-ontoβπ΄ β π»:πΆβΆπ΄) |
93 | 1, 92 | syl 17 |
. . . . 5
β’ (π β π»:πΆβΆπ΄) |
94 | | fco 6693 |
. . . . 5
β’ ((πΉ:π΄βΆπ΅ β§ π»:πΆβΆπ΄) β (πΉ β π»):πΆβΆπ΅) |
95 | 55, 93, 94 | syl2anc 585 |
. . . 4
β’ (π β (πΉ β π»):πΆβΆπ΅) |
96 | 43, 84, 89, 45, 86, 91, 95 | eltsms 23500 |
. . 3
β’ (π β (π₯ β (πΊ tsums (πΉ β π»)) β (π₯ β π΅ β§ βπ’ β (TopOpenβπΊ)(π₯ β π’ β βπ β (π« πΆ β© Fin)βπ β (π« πΆ β© Fin)(π β π β (πΊ Ξ£g ((πΉ β π») βΎ π)) β π’))))) |
97 | 83, 88, 96 | 3bitr4d 311 |
. 2
β’ (π β (π₯ β (πΊ tsums πΉ) β π₯ β (πΊ tsums (πΉ β π»)))) |
98 | 97 | eqrdv 2731 |
1
β’ (π β (πΊ tsums πΉ) = (πΊ tsums (πΉ β π»))) |