Step | Hyp | Ref
| Expression |
1 | | sticksstones18.3 |
. . . . . . . . . . . . . 14
β’ π΄ = {π β£ (π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π)} |
2 | 1 | eqimssi 4003 |
. . . . . . . . . . . . 13
β’ π΄ β {π β£ (π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π)} |
3 | 2 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β π΄ β {π β£ (π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π)}) |
4 | 3 | sseld 3944 |
. . . . . . . . . . 11
β’ (π β (π β π΄ β π β {π β£ (π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π)})) |
5 | 4 | imp 408 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β π β {π β£ (π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π)}) |
6 | | vex 3448 |
. . . . . . . . . . 11
β’ π β V |
7 | | feq1 6650 |
. . . . . . . . . . . 12
β’ (π = π β (π:(1...πΎ)βΆβ0 β π:(1...πΎ)βΆβ0)) |
8 | | simpl 484 |
. . . . . . . . . . . . . . 15
β’ ((π = π β§ π β (1...πΎ)) β π = π) |
9 | 8 | fveq1d 6845 |
. . . . . . . . . . . . . 14
β’ ((π = π β§ π β (1...πΎ)) β (πβπ) = (πβπ)) |
10 | 9 | sumeq2dv 15593 |
. . . . . . . . . . . . 13
β’ (π = π β Ξ£π β (1...πΎ)(πβπ) = Ξ£π β (1...πΎ)(πβπ)) |
11 | 10 | eqeq1d 2735 |
. . . . . . . . . . . 12
β’ (π = π β (Ξ£π β (1...πΎ)(πβπ) = π β Ξ£π β (1...πΎ)(πβπ) = π)) |
12 | 7, 11 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π = π β ((π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π) β (π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π))) |
13 | 6, 12 | elab 3631 |
. . . . . . . . . 10
β’ (π β {π β£ (π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π)} β (π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π)) |
14 | 5, 13 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β (π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π)) |
15 | 14 | simpld 496 |
. . . . . . . 8
β’ ((π β§ π β π΄) β π:(1...πΎ)βΆβ0) |
16 | 15 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β π΄) β§ π₯ β π) β π:(1...πΎ)βΆβ0) |
17 | | sticksstones18.5 |
. . . . . . . . . . 11
β’ (π β π:(1...πΎ)β1-1-ontoβπ) |
18 | | f1ocnv 6797 |
. . . . . . . . . . 11
β’ (π:(1...πΎ)β1-1-ontoβπ β β‘π:πβ1-1-ontoβ(1...πΎ)) |
19 | 17, 18 | syl 17 |
. . . . . . . . . 10
β’ (π β β‘π:πβ1-1-ontoβ(1...πΎ)) |
20 | | f1of 6785 |
. . . . . . . . . 10
β’ (β‘π:πβ1-1-ontoβ(1...πΎ) β β‘π:πβΆ(1...πΎ)) |
21 | 19, 20 | syl 17 |
. . . . . . . . 9
β’ (π β β‘π:πβΆ(1...πΎ)) |
22 | 21 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π΄) β β‘π:πβΆ(1...πΎ)) |
23 | 22 | ffvelcdmda 7036 |
. . . . . . 7
β’ (((π β§ π β π΄) β§ π₯ β π) β (β‘πβπ₯) β (1...πΎ)) |
24 | 16, 23 | ffvelcdmd 7037 |
. . . . . 6
β’ (((π β§ π β π΄) β§ π₯ β π) β (πβ(β‘πβπ₯)) β
β0) |
25 | 24 | fmpttd 7064 |
. . . . 5
β’ ((π β§ π β π΄) β (π₯ β π β¦ (πβ(β‘πβπ₯))):πβΆβ0) |
26 | | eqidd 2734 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ π β π) β (π₯ β π β¦ (πβ(β‘πβπ₯))) = (π₯ β π β¦ (πβ(β‘πβπ₯)))) |
27 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π β π) β§ π₯ = π) β π₯ = π) |
28 | 27 | fveq2d 6847 |
. . . . . . . . 9
β’ ((((π β§ π β π΄) β§ π β π) β§ π₯ = π) β (β‘πβπ₯) = (β‘πβπ)) |
29 | 28 | fveq2d 6847 |
. . . . . . . 8
β’ ((((π β§ π β π΄) β§ π β π) β§ π₯ = π) β (πβ(β‘πβπ₯)) = (πβ(β‘πβπ))) |
30 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ π β π) β π β π) |
31 | | fvexd 6858 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ π β π) β (πβ(β‘πβπ)) β V) |
32 | 26, 29, 30, 31 | fvmptd 6956 |
. . . . . . 7
β’ (((π β§ π β π΄) β§ π β π) β ((π₯ β π β¦ (πβ(β‘πβπ₯)))βπ) = (πβ(β‘πβπ))) |
33 | 32 | sumeq2dv 15593 |
. . . . . 6
β’ ((π β§ π β π΄) β Ξ£π β π ((π₯ β π β¦ (πβ(β‘πβπ₯)))βπ) = Ξ£π β π (πβ(β‘πβπ))) |
34 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = (β‘πβπ) β (πβπ) = (πβ(β‘πβπ))) |
35 | | fzfid 13884 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β (1...πΎ) β Fin) |
36 | 17 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β π:(1...πΎ)β1-1-ontoβπ) |
37 | | f1oenfi 9129 |
. . . . . . . . . . . 12
β’
(((1...πΎ) β Fin
β§ π:(1...πΎ)β1-1-ontoβπ) β (1...πΎ) β π) |
38 | 35, 36, 37 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β (1...πΎ) β π) |
39 | 38 | ensymd 8948 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β π β (1...πΎ)) |
40 | | enfii 9136 |
. . . . . . . . . 10
β’
(((1...πΎ) β Fin
β§ π β (1...πΎ)) β π β Fin) |
41 | 35, 39, 40 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β π β Fin) |
42 | 19 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β β‘π:πβ1-1-ontoβ(1...πΎ)) |
43 | | eqidd 2734 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ π β π) β (β‘πβπ) = (β‘πβπ)) |
44 | | nn0sscn 12423 |
. . . . . . . . . . . 12
β’
β0 β β |
45 | 44 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β β0 β
β) |
46 | | fss 6686 |
. . . . . . . . . . 11
β’ ((π:(1...πΎ)βΆβ0 β§
β0 β β) β π:(1...πΎ)βΆβ) |
47 | 15, 45, 46 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β π:(1...πΎ)βΆβ) |
48 | 47 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ π β (1...πΎ)) β (πβπ) β β) |
49 | 34, 41, 42, 43, 48 | fsumf1o 15613 |
. . . . . . . 8
β’ ((π β§ π β π΄) β Ξ£π β (1...πΎ)(πβπ) = Ξ£π β π (πβ(β‘πβπ))) |
50 | 49 | eqcomd 2739 |
. . . . . . 7
β’ ((π β§ π β π΄) β Ξ£π β π (πβ(β‘πβπ)) = Ξ£π β (1...πΎ)(πβπ)) |
51 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = π β (πβπ) = (πβπ)) |
52 | 51 | cbvsumv 15586 |
. . . . . . . . 9
β’
Ξ£π β
(1...πΎ)(πβπ) = Ξ£π β (1...πΎ)(πβπ) |
53 | 52 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β π΄) β Ξ£π β (1...πΎ)(πβπ) = Ξ£π β (1...πΎ)(πβπ)) |
54 | 14 | simprd 497 |
. . . . . . . 8
β’ ((π β§ π β π΄) β Ξ£π β (1...πΎ)(πβπ) = π) |
55 | 53, 54 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ π β π΄) β Ξ£π β (1...πΎ)(πβπ) = π) |
56 | 50, 55 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π β π΄) β Ξ£π β π (πβ(β‘πβπ)) = π) |
57 | 33, 56 | eqtrd 2773 |
. . . . 5
β’ ((π β§ π β π΄) β Ξ£π β π ((π₯ β π β¦ (πβ(β‘πβπ₯)))βπ) = π) |
58 | 25, 57 | jca 513 |
. . . 4
β’ ((π β§ π β π΄) β ((π₯ β π β¦ (πβ(β‘πβπ₯))):πβΆβ0 β§
Ξ£π β π ((π₯ β π β¦ (πβ(β‘πβπ₯)))βπ) = π)) |
59 | | fzfid 13884 |
. . . . . . . 8
β’ (π β (1...πΎ) β Fin) |
60 | 59 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π΄) β (1...πΎ) β Fin) |
61 | 59, 17, 37 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (1...πΎ) β π) |
62 | 61 | ensymd 8948 |
. . . . . . . 8
β’ (π β π β (1...πΎ)) |
63 | 62 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π΄) β π β (1...πΎ)) |
64 | 60, 63, 40 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β π΄) β π β Fin) |
65 | 64 | mptexd 7175 |
. . . . 5
β’ ((π β§ π β π΄) β (π₯ β π β¦ (πβ(β‘πβπ₯))) β V) |
66 | | feq1 6650 |
. . . . . . 7
β’ (β = (π₯ β π β¦ (πβ(β‘πβπ₯))) β (β:πβΆβ0 β (π₯ β π β¦ (πβ(β‘πβπ₯))):πβΆβ0)) |
67 | | simpl 484 |
. . . . . . . . . 10
β’ ((β = (π₯ β π β¦ (πβ(β‘πβπ₯))) β§ π β π) β β = (π₯ β π β¦ (πβ(β‘πβπ₯)))) |
68 | 67 | fveq1d 6845 |
. . . . . . . . 9
β’ ((β = (π₯ β π β¦ (πβ(β‘πβπ₯))) β§ π β π) β (ββπ) = ((π₯ β π β¦ (πβ(β‘πβπ₯)))βπ)) |
69 | 68 | sumeq2dv 15593 |
. . . . . . . 8
β’ (β = (π₯ β π β¦ (πβ(β‘πβπ₯))) β Ξ£π β π (ββπ) = Ξ£π β π ((π₯ β π β¦ (πβ(β‘πβπ₯)))βπ)) |
70 | 69 | eqeq1d 2735 |
. . . . . . 7
β’ (β = (π₯ β π β¦ (πβ(β‘πβπ₯))) β (Ξ£π β π (ββπ) = π β Ξ£π β π ((π₯ β π β¦ (πβ(β‘πβπ₯)))βπ) = π)) |
71 | 66, 70 | anbi12d 632 |
. . . . . 6
β’ (β = (π₯ β π β¦ (πβ(β‘πβπ₯))) β ((β:πβΆβ0 β§
Ξ£π β π (ββπ) = π) β ((π₯ β π β¦ (πβ(β‘πβπ₯))):πβΆβ0 β§
Ξ£π β π ((π₯ β π β¦ (πβ(β‘πβπ₯)))βπ) = π))) |
72 | 71 | elabg 3629 |
. . . . 5
β’ ((π₯ β π β¦ (πβ(β‘πβπ₯))) β V β ((π₯ β π β¦ (πβ(β‘πβπ₯))) β {β β£ (β:πβΆβ0 β§
Ξ£π β π (ββπ) = π)} β ((π₯ β π β¦ (πβ(β‘πβπ₯))):πβΆβ0 β§
Ξ£π β π ((π₯ β π β¦ (πβ(β‘πβπ₯)))βπ) = π))) |
73 | 65, 72 | syl 17 |
. . . 4
β’ ((π β§ π β π΄) β ((π₯ β π β¦ (πβ(β‘πβπ₯))) β {β β£ (β:πβΆβ0 β§
Ξ£π β π (ββπ) = π)} β ((π₯ β π β¦ (πβ(β‘πβπ₯))):πβΆβ0 β§
Ξ£π β π ((π₯ β π β¦ (πβ(β‘πβπ₯)))βπ) = π))) |
74 | 58, 73 | mpbird 257 |
. . 3
β’ ((π β§ π β π΄) β (π₯ β π β¦ (πβ(β‘πβπ₯))) β {β β£ (β:πβΆβ0 β§
Ξ£π β π (ββπ) = π)}) |
75 | | sticksstones18.4 |
. . . 4
β’ π΅ = {β β£ (β:πβΆβ0 β§
Ξ£π β π (ββπ) = π)} |
76 | 75 | a1i 11 |
. . 3
β’ ((π β§ π β π΄) β π΅ = {β β£ (β:πβΆβ0 β§
Ξ£π β π (ββπ) = π)}) |
77 | 74, 76 | eleqtrrd 2837 |
. 2
β’ ((π β§ π β π΄) β (π₯ β π β¦ (πβ(β‘πβπ₯))) β π΅) |
78 | | sticksstones18.6 |
. 2
β’ πΉ = (π β π΄ β¦ (π₯ β π β¦ (πβ(β‘πβπ₯)))) |
79 | 77, 78 | fmptd 7063 |
1
β’ (π β πΉ:π΄βΆπ΅) |