Step | Hyp | Ref
| Expression |
1 | | hashgval2 14285 |
. . . 4
β’ (β―
βΎ Ο) = (rec((π₯
β V β¦ (π₯ + 1)),
0) βΎ Ο) |
2 | 1 | hashgf1o 13883 |
. . 3
β’ (β―
βΎ Ο):Οβ1-1-ontoββ0 |
3 | | sneq 4601 |
. . . . . . . . . 10
β’ (π€ = π¦ β {π€} = {π¦}) |
4 | | pweq 4579 |
. . . . . . . . . 10
β’ (π€ = π¦ β π« π€ = π« π¦) |
5 | 3, 4 | xpeq12d 5669 |
. . . . . . . . 9
β’ (π€ = π¦ β ({π€} Γ π« π€) = ({π¦} Γ π« π¦)) |
6 | 5 | cbviunv 5005 |
. . . . . . . 8
β’ βͺ π€ β π§ ({π€} Γ π« π€) = βͺ π¦ β π§ ({π¦} Γ π« π¦) |
7 | | iuneq1 4975 |
. . . . . . . 8
β’ (π§ = π₯ β βͺ
π¦ β π§ ({π¦} Γ π« π¦) = βͺ π¦ β π₯ ({π¦} Γ π« π¦)) |
8 | 6, 7 | eqtrid 2789 |
. . . . . . 7
β’ (π§ = π₯ β βͺ
π€ β π§ ({π€} Γ π« π€) = βͺ π¦ β π₯ ({π¦} Γ π« π¦)) |
9 | 8 | fveq2d 6851 |
. . . . . 6
β’ (π§ = π₯ β (cardββͺ π€ β π§ ({π€} Γ π« π€)) = (cardββͺ π¦ β π₯ ({π¦} Γ π« π¦))) |
10 | 9 | cbvmptv 5223 |
. . . . 5
β’ (π§ β (π« Ο β©
Fin) β¦ (cardββͺ π€ β π§ ({π€} Γ π« π€))) = (π₯ β (π« Ο β© Fin) β¦
(cardββͺ π¦ β π₯ ({π¦} Γ π« π¦))) |
11 | 10 | ackbij1 10181 |
. . . 4
β’ (π§ β (π« Ο β©
Fin) β¦ (cardββͺ π€ β π§ ({π€} Γ π« π€))):(π« Ο β© Fin)β1-1-ontoβΟ |
12 | | f1ocnv 6801 |
. . . . . 6
β’ ((β―
βΎ Ο):Οβ1-1-ontoββ0 β β‘(β― βΎ
Ο):β0β1-1-ontoβΟ) |
13 | 2, 12 | ax-mp 5 |
. . . . 5
β’ β‘(β― βΎ
Ο):β0β1-1-ontoβΟ |
14 | | f1opwfi 9307 |
. . . . 5
β’ (β‘(β― βΎ
Ο):β0β1-1-ontoβΟ β (π₯ β (π« β0 β©
Fin) β¦ (β‘(β― βΎ
Ο) β π₯)):(π« β0 β©
Fin)β1-1-ontoβ(π« Ο β©
Fin)) |
15 | 13, 14 | ax-mp 5 |
. . . 4
β’ (π₯ β (π«
β0 β© Fin) β¦ (β‘(β― βΎ Ο) β π₯)):(π«
β0 β© Fin)β1-1-ontoβ(π« Ο β© Fin) |
16 | | f1oco 6812 |
. . . 4
β’ (((π§ β (π« Ο β©
Fin) β¦ (cardββͺ π€ β π§ ({π€} Γ π« π€))):(π« Ο β© Fin)β1-1-ontoβΟ β§ (π₯ β (π« β0 β©
Fin) β¦ (β‘(β― βΎ
Ο) β π₯)):(π« β0 β©
Fin)β1-1-ontoβ(π« Ο β© Fin)) β ((π§ β (π« Ο β©
Fin) β¦ (cardββͺ π€ β π§ ({π€} Γ π« π€))) β (π₯ β (π« β0 β©
Fin) β¦ (β‘(β― βΎ
Ο) β π₯))):(π« β0 β©
Fin)β1-1-ontoβΟ) |
17 | 11, 15, 16 | mp2an 691 |
. . 3
β’ ((π§ β (π« Ο β©
Fin) β¦ (cardββͺ π€ β π§ ({π€} Γ π« π€))) β (π₯ β (π« β0 β©
Fin) β¦ (β‘(β― βΎ
Ο) β π₯))):(π« β0 β©
Fin)β1-1-ontoβΟ |
18 | | f1oco 6812 |
. . 3
β’
(((β― βΎ Ο):Οβ1-1-ontoββ0 β§ ((π§ β (π« Ο β© Fin) β¦
(cardββͺ π€ β π§ ({π€} Γ π« π€))) β (π₯ β (π« β0 β©
Fin) β¦ (β‘(β― βΎ
Ο) β π₯))):(π« β0 β©
Fin)β1-1-ontoβΟ) β ((β― βΎ Ο)
β ((π§ β
(π« Ο β© Fin) β¦ (cardββͺ π€ β π§ ({π€} Γ π« π€))) β (π₯ β (π« β0 β©
Fin) β¦ (β‘(β― βΎ
Ο) β π₯)))):(π« β0 β©
Fin)β1-1-ontoββ0) |
19 | 2, 17, 18 | mp2an 691 |
. 2
β’ ((β―
βΎ Ο) β ((π§ β (π« Ο β© Fin) β¦
(cardββͺ π€ β π§ ({π€} Γ π« π€))) β (π₯ β (π« β0 β©
Fin) β¦ (β‘(β― βΎ
Ο) β π₯)))):(π« β0 β©
Fin)β1-1-ontoββ0 |
20 | | inss2 4194 |
. . . . . . . . . 10
β’
(π« Ο β© Fin) β Fin |
21 | | f1of 6789 |
. . . . . . . . . . . . 13
β’ ((π₯ β (π«
β0 β© Fin) β¦ (β‘(β― βΎ Ο) β π₯)):(π«
β0 β© Fin)β1-1-ontoβ(π« Ο β© Fin) β (π₯ β (π«
β0 β© Fin) β¦ (β‘(β― βΎ Ο) β π₯)):(π«
β0 β© Fin)βΆ(π« Ο β©
Fin)) |
22 | 15, 21 | ax-mp 5 |
. . . . . . . . . . . 12
β’ (π₯ β (π«
β0 β© Fin) β¦ (β‘(β― βΎ Ο) β π₯)):(π«
β0 β© Fin)βΆ(π« Ο β©
Fin) |
23 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π₯ β (π«
β0 β© Fin) β¦ (β‘(β― βΎ Ο) β π₯)) = (π₯ β (π« β0 β©
Fin) β¦ (β‘(β― βΎ
Ο) β π₯)) |
24 | 23 | fmpt 7063 |
. . . . . . . . . . . 12
β’
(βπ₯ β
(π« β0 β© Fin)(β‘(β― βΎ Ο) β π₯) β (π« Ο
β© Fin) β (π₯ β
(π« β0 β© Fin) β¦ (β‘(β― βΎ Ο) β π₯)):(π«
β0 β© Fin)βΆ(π« Ο β©
Fin)) |
25 | 22, 24 | mpbir 230 |
. . . . . . . . . . 11
β’
βπ₯ β
(π« β0 β© Fin)(β‘(β― βΎ Ο) β π₯) β (π« Ο
β© Fin) |
26 | 25 | rspec 3236 |
. . . . . . . . . 10
β’ (π₯ β (π«
β0 β© Fin) β (β‘(β― βΎ Ο) β π₯) β (π« Ο
β© Fin)) |
27 | 20, 26 | sselid 3947 |
. . . . . . . . 9
β’ (π₯ β (π«
β0 β© Fin) β (β‘(β― βΎ Ο) β π₯) β Fin) |
28 | | snfi 8995 |
. . . . . . . . . . 11
β’ {π€} β Fin |
29 | | cnvimass 6038 |
. . . . . . . . . . . . . . 15
β’ (β‘(β― βΎ Ο) β π₯) β dom (β― βΎ
Ο) |
30 | | dmhashres 14248 |
. . . . . . . . . . . . . . 15
β’ dom
(β― βΎ Ο) = Ο |
31 | 29, 30 | sseqtri 3985 |
. . . . . . . . . . . . . 14
β’ (β‘(β― βΎ Ο) β π₯) β
Ο |
32 | | onfin2 9182 |
. . . . . . . . . . . . . . 15
β’ Ο =
(On β© Fin) |
33 | | inss2 4194 |
. . . . . . . . . . . . . . 15
β’ (On β©
Fin) β Fin |
34 | 32, 33 | eqsstri 3983 |
. . . . . . . . . . . . . 14
β’ Ο
β Fin |
35 | 31, 34 | sstri 3958 |
. . . . . . . . . . . . 13
β’ (β‘(β― βΎ Ο) β π₯) β Fin |
36 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π₯ β (π«
β0 β© Fin) β§ π€ β (β‘(β― βΎ Ο) β π₯)) β π€ β (β‘(β― βΎ Ο) β π₯)) |
37 | 35, 36 | sselid 3947 |
. . . . . . . . . . . 12
β’ ((π₯ β (π«
β0 β© Fin) β§ π€ β (β‘(β― βΎ Ο) β π₯)) β π€ β Fin) |
38 | | pwfi 9129 |
. . . . . . . . . . . 12
β’ (π€ β Fin β π«
π€ β
Fin) |
39 | 37, 38 | sylib 217 |
. . . . . . . . . . 11
β’ ((π₯ β (π«
β0 β© Fin) β§ π€ β (β‘(β― βΎ Ο) β π₯)) β π« π€ β Fin) |
40 | | xpfi 9268 |
. . . . . . . . . . 11
β’ (({π€} β Fin β§ π«
π€ β Fin) β
({π€} Γ π«
π€) β
Fin) |
41 | 28, 39, 40 | sylancr 588 |
. . . . . . . . . 10
β’ ((π₯ β (π«
β0 β© Fin) β§ π€ β (β‘(β― βΎ Ο) β π₯)) β ({π€} Γ π« π€) β Fin) |
42 | 41 | ralrimiva 3144 |
. . . . . . . . 9
β’ (π₯ β (π«
β0 β© Fin) β βπ€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€) β Fin) |
43 | | iunfi 9291 |
. . . . . . . . 9
β’ (((β‘(β― βΎ Ο) β π₯) β Fin β§ βπ€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€) β Fin) β βͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€) β Fin) |
44 | 27, 42, 43 | syl2anc 585 |
. . . . . . . 8
β’ (π₯ β (π«
β0 β© Fin) β βͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€) β Fin) |
45 | | ficardom 9904 |
. . . . . . . 8
β’ (βͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€) β Fin β (cardββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€)) β Ο) |
46 | 44, 45 | syl 17 |
. . . . . . 7
β’ (π₯ β (π«
β0 β© Fin) β (cardββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€)) β Ο) |
47 | 46 | fvresd 6867 |
. . . . . 6
β’ (π₯ β (π«
β0 β© Fin) β ((β― βΎ
Ο)β(cardββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€))) = (β―β(cardββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€)))) |
48 | | hashcard 14262 |
. . . . . . 7
β’ (βͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€) β Fin β
(β―β(cardββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€))) = (β―ββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€))) |
49 | 44, 48 | syl 17 |
. . . . . 6
β’ (π₯ β (π«
β0 β© Fin) β (β―β(cardββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€))) = (β―ββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€))) |
50 | | xp1st 7958 |
. . . . . . . . . . . 12
β’ (π§ β ({π€} Γ π« π€) β (1st βπ§) β {π€}) |
51 | | elsni 4608 |
. . . . . . . . . . . 12
β’
((1st βπ§) β {π€} β (1st βπ§) = π€) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . 11
β’ (π§ β ({π€} Γ π« π€) β (1st βπ§) = π€) |
53 | 52 | rgen 3067 |
. . . . . . . . . 10
β’
βπ§ β
({π€} Γ π«
π€)(1st
βπ§) = π€ |
54 | 53 | rgenw 3069 |
. . . . . . . . 9
β’
βπ€ β
(β‘(β― βΎ Ο) β
π₯)βπ§ β ({π€} Γ π« π€)(1st βπ§) = π€ |
55 | | invdisj 5094 |
. . . . . . . . 9
β’
(βπ€ β
(β‘(β― βΎ Ο) β
π₯)βπ§ β ({π€} Γ π« π€)(1st βπ§) = π€ β Disj π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€)) |
56 | 54, 55 | mp1i 13 |
. . . . . . . 8
β’ (π₯ β (π«
β0 β© Fin) β Disj π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€)) |
57 | 27, 41, 56 | hashiun 15714 |
. . . . . . 7
β’ (π₯ β (π«
β0 β© Fin) β (β―ββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€)) = Ξ£π€ β (β‘(β― βΎ Ο) β π₯)(β―β({π€} Γ π« π€))) |
58 | | sneq 4601 |
. . . . . . . . . 10
β’ (π€ = (β‘(β― βΎ Ο)βπ¦) β {π€} = {(β‘(β― βΎ Ο)βπ¦)}) |
59 | | pweq 4579 |
. . . . . . . . . 10
β’ (π€ = (β‘(β― βΎ Ο)βπ¦) β π« π€ = π« (β‘(β― βΎ Ο)βπ¦)) |
60 | 58, 59 | xpeq12d 5669 |
. . . . . . . . 9
β’ (π€ = (β‘(β― βΎ Ο)βπ¦) β ({π€} Γ π« π€) = ({(β‘(β― βΎ Ο)βπ¦)} Γ π« (β‘(β― βΎ Ο)βπ¦))) |
61 | 60 | fveq2d 6851 |
. . . . . . . 8
β’ (π€ = (β‘(β― βΎ Ο)βπ¦) β (β―β({π€} Γ π« π€)) = (β―β({(β‘(β― βΎ Ο)βπ¦)} Γ π« (β‘(β― βΎ Ο)βπ¦)))) |
62 | | elinel2 4161 |
. . . . . . . 8
β’ (π₯ β (π«
β0 β© Fin) β π₯ β Fin) |
63 | | f1of1 6788 |
. . . . . . . . . 10
β’ (β‘(β― βΎ
Ο):β0β1-1-ontoβΟ β β‘(β― βΎ
Ο):β0β1-1βΟ) |
64 | 13, 63 | ax-mp 5 |
. . . . . . . . 9
β’ β‘(β― βΎ
Ο):β0β1-1βΟ |
65 | | elinel1 4160 |
. . . . . . . . . 10
β’ (π₯ β (π«
β0 β© Fin) β π₯ β π«
β0) |
66 | 65 | elpwid 4574 |
. . . . . . . . 9
β’ (π₯ β (π«
β0 β© Fin) β π₯ β
β0) |
67 | | f1ores 6803 |
. . . . . . . . 9
β’ ((β‘(β― βΎ
Ο):β0β1-1βΟ β§ π₯ β β0) β (β‘(β― βΎ Ο) βΎ π₯):π₯β1-1-ontoβ(β‘(β― βΎ Ο) β π₯)) |
68 | 64, 66, 67 | sylancr 588 |
. . . . . . . 8
β’ (π₯ β (π«
β0 β© Fin) β (β‘(β― βΎ Ο) βΎ π₯):π₯β1-1-ontoβ(β‘(β― βΎ Ο) β π₯)) |
69 | | fvres 6866 |
. . . . . . . . 9
β’ (π¦ β π₯ β ((β‘(β― βΎ Ο) βΎ π₯)βπ¦) = (β‘(β― βΎ Ο)βπ¦)) |
70 | 69 | adantl 483 |
. . . . . . . 8
β’ ((π₯ β (π«
β0 β© Fin) β§ π¦ β π₯) β ((β‘(β― βΎ Ο) βΎ π₯)βπ¦) = (β‘(β― βΎ Ο)βπ¦)) |
71 | | hashcl 14263 |
. . . . . . . . 9
β’ (({π€} Γ π« π€) β Fin β
(β―β({π€} Γ
π« π€)) β
β0) |
72 | | nn0cn 12430 |
. . . . . . . . 9
β’
((β―β({π€}
Γ π« π€))
β β0 β (β―β({π€} Γ π« π€)) β β) |
73 | 41, 71, 72 | 3syl 18 |
. . . . . . . 8
β’ ((π₯ β (π«
β0 β© Fin) β§ π€ β (β‘(β― βΎ Ο) β π₯)) β (β―β({π€} Γ π« π€)) β
β) |
74 | 61, 62, 68, 70, 73 | fsumf1o 15615 |
. . . . . . 7
β’ (π₯ β (π«
β0 β© Fin) β Ξ£π€ β (β‘(β― βΎ Ο) β π₯)(β―β({π€} Γ π« π€)) = Ξ£π¦ β π₯ (β―β({(β‘(β― βΎ Ο)βπ¦)} Γ π« (β‘(β― βΎ Ο)βπ¦)))) |
75 | | snfi 8995 |
. . . . . . . . . 10
β’ {(β‘(β― βΎ Ο)βπ¦)} β Fin |
76 | 66 | sselda 3949 |
. . . . . . . . . . . . 13
β’ ((π₯ β (π«
β0 β© Fin) β§ π¦ β π₯) β π¦ β β0) |
77 | | f1of 6789 |
. . . . . . . . . . . . . . 15
β’ (β‘(β― βΎ
Ο):β0β1-1-ontoβΟ β β‘(β― βΎ
Ο):β0βΆΟ) |
78 | 13, 77 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ β‘(β― βΎ
Ο):β0βΆΟ |
79 | 78 | ffvelcdmi 7039 |
. . . . . . . . . . . . 13
β’ (π¦ β β0
β (β‘(β― βΎ
Ο)βπ¦) β
Ο) |
80 | 76, 79 | syl 17 |
. . . . . . . . . . . 12
β’ ((π₯ β (π«
β0 β© Fin) β§ π¦ β π₯) β (β‘(β― βΎ Ο)βπ¦) β
Ο) |
81 | 34, 80 | sselid 3947 |
. . . . . . . . . . 11
β’ ((π₯ β (π«
β0 β© Fin) β§ π¦ β π₯) β (β‘(β― βΎ Ο)βπ¦) β Fin) |
82 | | pwfi 9129 |
. . . . . . . . . . 11
β’ ((β‘(β― βΎ Ο)βπ¦) β Fin β π«
(β‘(β― βΎ Ο)βπ¦) β Fin) |
83 | 81, 82 | sylib 217 |
. . . . . . . . . 10
β’ ((π₯ β (π«
β0 β© Fin) β§ π¦ β π₯) β π« (β‘(β― βΎ Ο)βπ¦) β Fin) |
84 | | hashxp 14341 |
. . . . . . . . . 10
β’ (({(β‘(β― βΎ Ο)βπ¦)} β Fin β§ π«
(β‘(β― βΎ Ο)βπ¦) β Fin) β
(β―β({(β‘(β― βΎ
Ο)βπ¦)} Γ
π« (β‘(β― βΎ
Ο)βπ¦))) =
((β―β{(β‘(β― βΎ
Ο)βπ¦)})
Β· (β―βπ« (β‘(β― βΎ Ο)βπ¦)))) |
85 | 75, 83, 84 | sylancr 588 |
. . . . . . . . 9
β’ ((π₯ β (π«
β0 β© Fin) β§ π¦ β π₯) β (β―β({(β‘(β― βΎ Ο)βπ¦)} Γ π« (β‘(β― βΎ Ο)βπ¦))) = ((β―β{(β‘(β― βΎ Ο)βπ¦)}) Β·
(β―βπ« (β‘(β―
βΎ Ο)βπ¦)))) |
86 | | hashsng 14276 |
. . . . . . . . . . 11
β’ ((β‘(β― βΎ Ο)βπ¦) β Ο β
(β―β{(β‘(β― βΎ
Ο)βπ¦)}) =
1) |
87 | 80, 86 | syl 17 |
. . . . . . . . . 10
β’ ((π₯ β (π«
β0 β© Fin) β§ π¦ β π₯) β (β―β{(β‘(β― βΎ Ο)βπ¦)}) = 1) |
88 | | hashpw 14343 |
. . . . . . . . . . . 12
β’ ((β‘(β― βΎ Ο)βπ¦) β Fin β
(β―βπ« (β‘(β―
βΎ Ο)βπ¦))
= (2β(β―β(β‘(β―
βΎ Ο)βπ¦)))) |
89 | 81, 88 | syl 17 |
. . . . . . . . . . 11
β’ ((π₯ β (π«
β0 β© Fin) β§ π¦ β π₯) β (β―βπ« (β‘(β― βΎ Ο)βπ¦)) =
(2β(β―β(β‘(β―
βΎ Ο)βπ¦)))) |
90 | 80 | fvresd 6867 |
. . . . . . . . . . . . 13
β’ ((π₯ β (π«
β0 β© Fin) β§ π¦ β π₯) β ((β― βΎ
Ο)β(β‘(β― βΎ
Ο)βπ¦)) =
(β―β(β‘(β― βΎ
Ο)βπ¦))) |
91 | | f1ocnvfv2 7228 |
. . . . . . . . . . . . . 14
β’
(((β― βΎ Ο):Οβ1-1-ontoββ0 β§ π¦ β β0) β ((β―
βΎ Ο)β(β‘(β―
βΎ Ο)βπ¦))
= π¦) |
92 | 2, 76, 91 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π₯ β (π«
β0 β© Fin) β§ π¦ β π₯) β ((β― βΎ
Ο)β(β‘(β― βΎ
Ο)βπ¦)) = π¦) |
93 | 90, 92 | eqtr3d 2779 |
. . . . . . . . . . . 12
β’ ((π₯ β (π«
β0 β© Fin) β§ π¦ β π₯) β (β―β(β‘(β― βΎ Ο)βπ¦)) = π¦) |
94 | 93 | oveq2d 7378 |
. . . . . . . . . . 11
β’ ((π₯ β (π«
β0 β© Fin) β§ π¦ β π₯) β (2β(β―β(β‘(β― βΎ Ο)βπ¦))) = (2βπ¦)) |
95 | 89, 94 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π₯ β (π«
β0 β© Fin) β§ π¦ β π₯) β (β―βπ« (β‘(β― βΎ Ο)βπ¦)) = (2βπ¦)) |
96 | 87, 95 | oveq12d 7380 |
. . . . . . . . 9
β’ ((π₯ β (π«
β0 β© Fin) β§ π¦ β π₯) β ((β―β{(β‘(β― βΎ Ο)βπ¦)}) Β·
(β―βπ« (β‘(β―
βΎ Ο)βπ¦)))
= (1 Β· (2βπ¦))) |
97 | | 2cn 12235 |
. . . . . . . . . . 11
β’ 2 β
β |
98 | | expcl 13992 |
. . . . . . . . . . 11
β’ ((2
β β β§ π¦
β β0) β (2βπ¦) β β) |
99 | 97, 76, 98 | sylancr 588 |
. . . . . . . . . 10
β’ ((π₯ β (π«
β0 β© Fin) β§ π¦ β π₯) β (2βπ¦) β β) |
100 | 99 | mulid2d 11180 |
. . . . . . . . 9
β’ ((π₯ β (π«
β0 β© Fin) β§ π¦ β π₯) β (1 Β· (2βπ¦)) = (2βπ¦)) |
101 | 85, 96, 100 | 3eqtrd 2781 |
. . . . . . . 8
β’ ((π₯ β (π«
β0 β© Fin) β§ π¦ β π₯) β (β―β({(β‘(β― βΎ Ο)βπ¦)} Γ π« (β‘(β― βΎ Ο)βπ¦))) = (2βπ¦)) |
102 | 101 | sumeq2dv 15595 |
. . . . . . 7
β’ (π₯ β (π«
β0 β© Fin) β Ξ£π¦ β π₯ (β―β({(β‘(β― βΎ Ο)βπ¦)} Γ π« (β‘(β― βΎ Ο)βπ¦))) = Ξ£π¦ β π₯ (2βπ¦)) |
103 | 57, 74, 102 | 3eqtrd 2781 |
. . . . . 6
β’ (π₯ β (π«
β0 β© Fin) β (β―ββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€)) = Ξ£π¦ β π₯ (2βπ¦)) |
104 | 47, 49, 103 | 3eqtrd 2781 |
. . . . 5
β’ (π₯ β (π«
β0 β© Fin) β ((β― βΎ
Ο)β(cardββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€))) = Ξ£π¦ β π₯ (2βπ¦)) |
105 | 104 | mpteq2ia 5213 |
. . . 4
β’ (π₯ β (π«
β0 β© Fin) β¦ ((β― βΎ
Ο)β(cardββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€)))) = (π₯ β (π« β0 β©
Fin) β¦ Ξ£π¦
β π₯ (2βπ¦)) |
106 | 46 | adantl 483 |
. . . . . 6
β’
((β€ β§ π₯
β (π« β0 β© Fin)) β (cardββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€)) β Ο) |
107 | 26 | adantl 483 |
. . . . . . 7
β’
((β€ β§ π₯
β (π« β0 β© Fin)) β (β‘(β― βΎ Ο) β π₯) β (π« Ο
β© Fin)) |
108 | | eqidd 2738 |
. . . . . . 7
β’ (β€
β (π₯ β (π«
β0 β© Fin) β¦ (β‘(β― βΎ Ο) β π₯)) = (π₯ β (π« β0 β©
Fin) β¦ (β‘(β― βΎ
Ο) β π₯))) |
109 | | eqidd 2738 |
. . . . . . 7
β’ (β€
β (π§ β (π«
Ο β© Fin) β¦ (cardββͺ
π€ β π§ ({π€} Γ π« π€))) = (π§ β (π« Ο β© Fin) β¦
(cardββͺ π€ β π§ ({π€} Γ π« π€)))) |
110 | | iuneq1 4975 |
. . . . . . . 8
β’ (π§ = (β‘(β― βΎ Ο) β π₯) β βͺ π€ β π§ ({π€} Γ π« π€) = βͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€)) |
111 | 110 | fveq2d 6851 |
. . . . . . 7
β’ (π§ = (β‘(β― βΎ Ο) β π₯) β (cardββͺ π€ β π§ ({π€} Γ π« π€)) = (cardββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€))) |
112 | 107, 108,
109, 111 | fmptco 7080 |
. . . . . 6
β’ (β€
β ((π§ β
(π« Ο β© Fin) β¦ (cardββͺ π€ β π§ ({π€} Γ π« π€))) β (π₯ β (π« β0 β©
Fin) β¦ (β‘(β― βΎ
Ο) β π₯))) =
(π₯ β (π«
β0 β© Fin) β¦ (cardββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€)))) |
113 | | f1of 6789 |
. . . . . . . 8
β’ ((β―
βΎ Ο):Οβ1-1-ontoββ0 β (β―
βΎ Ο):ΟβΆβ0) |
114 | 2, 113 | mp1i 13 |
. . . . . . 7
β’ (β€
β (β― βΎ
Ο):ΟβΆβ0) |
115 | 114 | feqmptd 6915 |
. . . . . 6
β’ (β€
β (β― βΎ Ο) = (π¦ β Ο β¦ ((β― βΎ
Ο)βπ¦))) |
116 | | fveq2 6847 |
. . . . . 6
β’ (π¦ = (cardββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€)) β ((β― βΎ
Ο)βπ¦) =
((β― βΎ Ο)β(cardββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€)))) |
117 | 106, 112,
115, 116 | fmptco 7080 |
. . . . 5
β’ (β€
β ((β― βΎ Ο) β ((π§ β (π« Ο β© Fin) β¦
(cardββͺ π€ β π§ ({π€} Γ π« π€))) β (π₯ β (π« β0 β©
Fin) β¦ (β‘(β― βΎ
Ο) β π₯)))) =
(π₯ β (π«
β0 β© Fin) β¦ ((β― βΎ
Ο)β(cardββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€))))) |
118 | 117 | mptru 1549 |
. . . 4
β’ ((β―
βΎ Ο) β ((π§ β (π« Ο β© Fin) β¦
(cardββͺ π€ β π§ ({π€} Γ π« π€))) β (π₯ β (π« β0 β©
Fin) β¦ (β‘(β― βΎ
Ο) β π₯)))) =
(π₯ β (π«
β0 β© Fin) β¦ ((β― βΎ
Ο)β(cardββͺ π€ β (β‘(β― βΎ Ο) β π₯)({π€} Γ π« π€)))) |
119 | | ackbijnn.1 |
. . . 4
β’ πΉ = (π₯ β (π« β0 β©
Fin) β¦ Ξ£π¦
β π₯ (2βπ¦)) |
120 | 105, 118,
119 | 3eqtr4i 2775 |
. . 3
β’ ((β―
βΎ Ο) β ((π§ β (π« Ο β© Fin) β¦
(cardββͺ π€ β π§ ({π€} Γ π« π€))) β (π₯ β (π« β0 β©
Fin) β¦ (β‘(β― βΎ
Ο) β π₯)))) =
πΉ |
121 | | f1oeq1 6777 |
. . 3
β’
(((β― βΎ Ο) β ((π§ β (π« Ο β© Fin) β¦
(cardββͺ π€ β π§ ({π€} Γ π« π€))) β (π₯ β (π« β0 β©
Fin) β¦ (β‘(β― βΎ
Ο) β π₯)))) =
πΉ β (((β― βΎ
Ο) β ((π§ β
(π« Ο β© Fin) β¦ (cardββͺ π€ β π§ ({π€} Γ π« π€))) β (π₯ β (π« β0 β©
Fin) β¦ (β‘(β― βΎ
Ο) β π₯)))):(π« β0 β©
Fin)β1-1-ontoββ0 β πΉ:(π« β0 β©
Fin)β1-1-ontoββ0)) |
122 | 120, 121 | ax-mp 5 |
. 2
β’
(((β― βΎ Ο) β ((π§ β (π« Ο β© Fin) β¦
(cardββͺ π€ β π§ ({π€} Γ π« π€))) β (π₯ β (π« β0 β©
Fin) β¦ (β‘(β― βΎ
Ο) β π₯)))):(π« β0 β©
Fin)β1-1-ontoββ0 β πΉ:(π« β0 β©
Fin)β1-1-ontoββ0) |
123 | 19, 122 | mpbi 229 |
1
β’ πΉ:(π« β0
β© Fin)β1-1-ontoββ0 |