Step | Hyp | Ref
| Expression |
1 | | gsumval3a.n |
. . . . . 6
β’ (π β π β β
) |
2 | 1 | neneqd 2945 |
. . . . 5
β’ (π β Β¬ π = β
) |
3 | | gsumval3a.t |
. . . . . . 7
β’ (π β π β Fin) |
4 | | fz1f1o 15600 |
. . . . . . 7
β’ (π β Fin β (π = β
β¨
((β―βπ) β
β β§ βπ
π:(1...(β―βπ))β1-1-ontoβπ))) |
5 | 3, 4 | syl 17 |
. . . . . 6
β’ (π β (π = β
β¨ ((β―βπ) β β β§
βπ π:(1...(β―βπ))β1-1-ontoβπ))) |
6 | 5 | ord 863 |
. . . . 5
β’ (π β (Β¬ π = β
β ((β―βπ) β β β§
βπ π:(1...(β―βπ))β1-1-ontoβπ))) |
7 | 2, 6 | mpd 15 |
. . . 4
β’ (π β ((β―βπ) β β β§
βπ π:(1...(β―βπ))β1-1-ontoβπ)) |
8 | 7 | simprd 497 |
. . 3
β’ (π β βπ π:(1...(β―βπ))β1-1-ontoβπ) |
9 | | excom 2163 |
. . . 4
β’
(βπ₯βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β βπβπ₯(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ)))) |
10 | | exancom 1865 |
. . . . . 6
β’
(βπ₯(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β βπ₯(π₯ = (seq1( + , (πΉ β π))β(β―βπ)) β§ π:(1...(β―βπ))β1-1-ontoβπ)) |
11 | | fvex 6856 |
. . . . . . 7
β’ (seq1(
+ ,
(πΉ β π))β(β―βπ)) β V |
12 | | biidd 262 |
. . . . . . 7
β’ (π₯ = (seq1( + , (πΉ β π))β(β―βπ)) β (π:(1...(β―βπ))β1-1-ontoβπ β π:(1...(β―βπ))β1-1-ontoβπ)) |
13 | 11, 12 | ceqsexv 3493 |
. . . . . 6
β’
(βπ₯(π₯ = (seq1( + , (πΉ β π))β(β―βπ)) β§ π:(1...(β―βπ))β1-1-ontoβπ) β π:(1...(β―βπ))β1-1-ontoβπ) |
14 | 10, 13 | bitri 275 |
. . . . 5
β’
(βπ₯(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β π:(1...(β―βπ))β1-1-ontoβπ) |
15 | 14 | exbii 1851 |
. . . 4
β’
(βπβπ₯(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β βπ π:(1...(β―βπ))β1-1-ontoβπ) |
16 | 9, 15 | bitri 275 |
. . 3
β’
(βπ₯βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β βπ π:(1...(β―βπ))β1-1-ontoβπ) |
17 | 8, 16 | sylibr 233 |
. 2
β’ (π β βπ₯βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ)))) |
18 | | exdistrv 1960 |
. . . 4
β’
(βπβπ((π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ)))) β (βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β§ βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ))))) |
19 | | an4 655 |
. . . . . 6
β’ (((π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ) β§ (π₯ = (seq1( + , (πΉ β π))β(β―βπ)) β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ)))) β ((π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ))))) |
20 | | gsumval3.g |
. . . . . . . . . . 11
β’ (π β πΊ β Mnd) |
21 | 20 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β πΊ β Mnd) |
22 | | gsumval3.b |
. . . . . . . . . . . 12
β’ π΅ = (BaseβπΊ) |
23 | | gsumval3.p |
. . . . . . . . . . . 12
β’ + =
(+gβπΊ) |
24 | 22, 23 | mndcl 18569 |
. . . . . . . . . . 11
β’ ((πΊ β Mnd β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) β π΅) |
25 | 24 | 3expb 1121 |
. . . . . . . . . 10
β’ ((πΊ β Mnd β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯ + π¦) β π΅) |
26 | 21, 25 | sylan 581 |
. . . . . . . . 9
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯ + π¦) β π΅) |
27 | | gsumval3.c |
. . . . . . . . . . . . 13
β’ (π β ran πΉ β (πβran πΉ)) |
28 | 27 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β ran πΉ β (πβran πΉ)) |
29 | 28 | sselda 3945 |
. . . . . . . . . . 11
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ π₯ β ran πΉ) β π₯ β (πβran πΉ)) |
30 | 29 | adantrr 716 |
. . . . . . . . . 10
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ (π₯ β ran πΉ β§ π¦ β ran πΉ)) β π₯ β (πβran πΉ)) |
31 | | simprr 772 |
. . . . . . . . . 10
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ (π₯ β ran πΉ β§ π¦ β ran πΉ)) β π¦ β ran πΉ) |
32 | | gsumval3.z |
. . . . . . . . . . 11
β’ π = (CntzβπΊ) |
33 | 23, 32 | cntzi 19114 |
. . . . . . . . . 10
β’ ((π₯ β (πβran πΉ) β§ π¦ β ran πΉ) β (π₯ + π¦) = (π¦ + π₯)) |
34 | 30, 31, 33 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ (π₯ β ran πΉ β§ π¦ β ran πΉ)) β (π₯ + π¦) = (π¦ + π₯)) |
35 | 22, 23 | mndass 18570 |
. . . . . . . . . 10
β’ ((πΊ β Mnd β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) |
36 | 21, 35 | sylan 581 |
. . . . . . . . 9
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) |
37 | 7 | simpld 496 |
. . . . . . . . . . 11
β’ (π β (β―βπ) β
β) |
38 | 37 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β (β―βπ) β
β) |
39 | | nnuz 12811 |
. . . . . . . . . 10
β’ β =
(β€β₯β1) |
40 | 38, 39 | eleqtrdi 2844 |
. . . . . . . . 9
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β (β―βπ) β
(β€β₯β1)) |
41 | | gsumval3.f |
. . . . . . . . . . 11
β’ (π β πΉ:π΄βΆπ΅) |
42 | 41 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β πΉ:π΄βΆπ΅) |
43 | 42 | frnd 6677 |
. . . . . . . . 9
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β ran πΉ β π΅) |
44 | | simprr 772 |
. . . . . . . . . . 11
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β π:(1...(β―βπ))β1-1-ontoβπ) |
45 | | f1ocnv 6797 |
. . . . . . . . . . 11
β’ (π:(1...(β―βπ))β1-1-ontoβπ β β‘π:πβ1-1-ontoβ(1...(β―βπ))) |
46 | 44, 45 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β β‘π:πβ1-1-ontoβ(1...(β―βπ))) |
47 | | simprl 770 |
. . . . . . . . . 10
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β π:(1...(β―βπ))β1-1-ontoβπ) |
48 | | f1oco 6808 |
. . . . . . . . . 10
β’ ((β‘π:πβ1-1-ontoβ(1...(β―βπ)) β§ π:(1...(β―βπ))β1-1-ontoβπ) β (β‘π β π):(1...(β―βπ))β1-1-ontoβ(1...(β―βπ))) |
49 | 46, 47, 48 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β (β‘π β π):(1...(β―βπ))β1-1-ontoβ(1...(β―βπ))) |
50 | | f1of 6785 |
. . . . . . . . . . . 12
β’ (π:(1...(β―βπ))β1-1-ontoβπ β π:(1...(β―βπ))βΆπ) |
51 | 44, 50 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β π:(1...(β―βπ))βΆπ) |
52 | | fvco3 6941 |
. . . . . . . . . . 11
β’ ((π:(1...(β―βπ))βΆπ β§ π₯ β (1...(β―βπ))) β ((πΉ β π)βπ₯) = (πΉβ(πβπ₯))) |
53 | 51, 52 | sylan 581 |
. . . . . . . . . 10
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ π₯ β (1...(β―βπ))) β ((πΉ β π)βπ₯) = (πΉβ(πβπ₯))) |
54 | 42 | ffnd 6670 |
. . . . . . . . . . 11
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β πΉ Fn π΄) |
55 | | gsumval3a.s |
. . . . . . . . . . . . . 14
β’ (π β π β π΄) |
56 | 55 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β π β π΄) |
57 | 51, 56 | fssd 6687 |
. . . . . . . . . . . 12
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β π:(1...(β―βπ))βΆπ΄) |
58 | 57 | ffvelcdmda 7036 |
. . . . . . . . . . 11
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ π₯ β (1...(β―βπ))) β (πβπ₯) β π΄) |
59 | | fnfvelrn 7032 |
. . . . . . . . . . 11
β’ ((πΉ Fn π΄ β§ (πβπ₯) β π΄) β (πΉβ(πβπ₯)) β ran πΉ) |
60 | 54, 58, 59 | syl2an2r 684 |
. . . . . . . . . 10
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ π₯ β (1...(β―βπ))) β (πΉβ(πβπ₯)) β ran πΉ) |
61 | 53, 60 | eqeltrd 2834 |
. . . . . . . . 9
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ π₯ β (1...(β―βπ))) β ((πΉ β π)βπ₯) β ran πΉ) |
62 | | f1of 6785 |
. . . . . . . . . . . . . . 15
β’ (π:(1...(β―βπ))β1-1-ontoβπ β π:(1...(β―βπ))βΆπ) |
63 | 47, 62 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β π:(1...(β―βπ))βΆπ) |
64 | | fvco3 6941 |
. . . . . . . . . . . . . 14
β’ ((π:(1...(β―βπ))βΆπ β§ π β (1...(β―βπ))) β ((β‘π β π)βπ) = (β‘πβ(πβπ))) |
65 | 63, 64 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ π β (1...(β―βπ))) β ((β‘π β π)βπ) = (β‘πβ(πβπ))) |
66 | 65 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ π β (1...(β―βπ))) β (πβ((β‘π β π)βπ)) = (πβ(β‘πβ(πβπ)))) |
67 | 63 | ffvelcdmda 7036 |
. . . . . . . . . . . . 13
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ π β (1...(β―βπ))) β (πβπ) β π) |
68 | | f1ocnvfv2 7224 |
. . . . . . . . . . . . 13
β’ ((π:(1...(β―βπ))β1-1-ontoβπ β§ (πβπ) β π) β (πβ(β‘πβ(πβπ))) = (πβπ)) |
69 | 44, 67, 68 | syl2an2r 684 |
. . . . . . . . . . . 12
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ π β (1...(β―βπ))) β (πβ(β‘πβ(πβπ))) = (πβπ)) |
70 | 66, 69 | eqtr2d 2774 |
. . . . . . . . . . 11
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ π β (1...(β―βπ))) β (πβπ) = (πβ((β‘π β π)βπ))) |
71 | 70 | fveq2d 6847 |
. . . . . . . . . 10
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ π β (1...(β―βπ))) β (πΉβ(πβπ)) = (πΉβ(πβ((β‘π β π)βπ)))) |
72 | | fvco3 6941 |
. . . . . . . . . . 11
β’ ((π:(1...(β―βπ))βΆπ β§ π β (1...(β―βπ))) β ((πΉ β π)βπ) = (πΉβ(πβπ))) |
73 | 63, 72 | sylan 581 |
. . . . . . . . . 10
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ π β (1...(β―βπ))) β ((πΉ β π)βπ) = (πΉβ(πβπ))) |
74 | | f1of 6785 |
. . . . . . . . . . . . 13
β’ ((β‘π β π):(1...(β―βπ))β1-1-ontoβ(1...(β―βπ)) β (β‘π β π):(1...(β―βπ))βΆ(1...(β―βπ))) |
75 | 49, 74 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β (β‘π β π):(1...(β―βπ))βΆ(1...(β―βπ))) |
76 | 75 | ffvelcdmda 7036 |
. . . . . . . . . . 11
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ π β (1...(β―βπ))) β ((β‘π β π)βπ) β (1...(β―βπ))) |
77 | | fvco3 6941 |
. . . . . . . . . . 11
β’ ((π:(1...(β―βπ))βΆπ΄ β§ ((β‘π β π)βπ) β (1...(β―βπ))) β ((πΉ β π)β((β‘π β π)βπ)) = (πΉβ(πβ((β‘π β π)βπ)))) |
78 | 57, 76, 77 | syl2an2r 684 |
. . . . . . . . . 10
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ π β (1...(β―βπ))) β ((πΉ β π)β((β‘π β π)βπ)) = (πΉβ(πβ((β‘π β π)βπ)))) |
79 | 71, 73, 78 | 3eqtr4d 2783 |
. . . . . . . . 9
β’ (((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β§ π β (1...(β―βπ))) β ((πΉ β π)βπ) = ((πΉ β π)β((β‘π β π)βπ))) |
80 | 26, 34, 36, 40, 43, 49, 61, 79 | seqf1o 13955 |
. . . . . . . 8
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β (seq1( + , (πΉ β π))β(β―βπ)) = (seq1( + , (πΉ β π))β(β―βπ))) |
81 | | eqeq12 2750 |
. . . . . . . 8
β’ ((π₯ = (seq1( + , (πΉ β π))β(β―βπ)) β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ))) β (π₯ = π¦ β (seq1( + , (πΉ β π))β(β―βπ)) = (seq1( + , (πΉ β π))β(β―βπ)))) |
82 | 80, 81 | syl5ibrcom 247 |
. . . . . . 7
β’ ((π β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ)) β ((π₯ = (seq1( + , (πΉ β π))β(β―βπ)) β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ))) β π₯ = π¦)) |
83 | 82 | expimpd 455 |
. . . . . 6
β’ (π β (((π:(1...(β―βπ))β1-1-ontoβπ β§ π:(1...(β―βπ))β1-1-ontoβπ) β§ (π₯ = (seq1( + , (πΉ β π))β(β―βπ)) β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ)))) β π₯ = π¦)) |
84 | 19, 83 | biimtrrid 242 |
. . . . 5
β’ (π β (((π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ)))) β π₯ = π¦)) |
85 | 84 | exlimdvv 1938 |
. . . 4
β’ (π β (βπβπ((π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β§ (π:(1...(β―βπ))β1-1-ontoβπ β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ)))) β π₯ = π¦)) |
86 | 18, 85 | biimtrrid 242 |
. . 3
β’ (π β ((βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β§ βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ)))) β π₯ = π¦)) |
87 | 86 | alrimivv 1932 |
. 2
β’ (π β βπ₯βπ¦((βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β§ βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ)))) β π₯ = π¦)) |
88 | | eqeq1 2737 |
. . . . . 6
β’ (π₯ = π¦ β (π₯ = (seq1( + , (πΉ β π))β(β―βπ)) β π¦ = (seq1( + , (πΉ β π))β(β―βπ)))) |
89 | 88 | anbi2d 630 |
. . . . 5
β’ (π₯ = π¦ β ((π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β (π:(1...(β―βπ))β1-1-ontoβπ β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ))))) |
90 | 89 | exbidv 1925 |
. . . 4
β’ (π₯ = π¦ β (βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ))))) |
91 | | f1oeq1 6773 |
. . . . . 6
β’ (π = π β (π:(1...(β―βπ))β1-1-ontoβπ β π:(1...(β―βπ))β1-1-ontoβπ)) |
92 | | coeq2 5815 |
. . . . . . . . 9
β’ (π = π β (πΉ β π) = (πΉ β π)) |
93 | 92 | seqeq3d 13920 |
. . . . . . . 8
β’ (π = π β seq1( + , (πΉ β π)) = seq1( + , (πΉ β π))) |
94 | 93 | fveq1d 6845 |
. . . . . . 7
β’ (π = π β (seq1( + , (πΉ β π))β(β―βπ)) = (seq1( + , (πΉ β π))β(β―βπ))) |
95 | 94 | eqeq2d 2744 |
. . . . . 6
β’ (π = π β (π¦ = (seq1( + , (πΉ β π))β(β―βπ)) β π¦ = (seq1( + , (πΉ β π))β(β―βπ)))) |
96 | 91, 95 | anbi12d 632 |
. . . . 5
β’ (π = π β ((π:(1...(β―βπ))β1-1-ontoβπ β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ))) β (π:(1...(β―βπ))β1-1-ontoβπ β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ))))) |
97 | 96 | cbvexvw 2041 |
. . . 4
β’
(βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ))) β βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ)))) |
98 | 90, 97 | bitrdi 287 |
. . 3
β’ (π₯ = π¦ β (βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ))))) |
99 | 98 | eu4 2612 |
. 2
β’
(β!π₯βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β (βπ₯βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β§ βπ₯βπ¦((βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))) β§ βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π¦ = (seq1( + , (πΉ β π))β(β―βπ)))) β π₯ = π¦))) |
100 | 17, 87, 99 | sylanbrc 584 |
1
β’ (π β β!π₯βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ)))) |