Step | Hyp | Ref
| Expression |
1 | | ssid 3971 |
. 2
β’ {π β£ π:π΄β1-1βπ΅} β {π β£ π:π΄β1-1βπ΅} |
2 | | hashf1lem2.2 |
. . . . 5
β’ (π β π΅ β Fin) |
3 | | hashf1lem2.1 |
. . . . 5
β’ (π β π΄ β Fin) |
4 | | mapfi 9299 |
. . . . 5
β’ ((π΅ β Fin β§ π΄ β Fin) β (π΅ βm π΄) β Fin) |
5 | 2, 3, 4 | syl2anc 585 |
. . . 4
β’ (π β (π΅ βm π΄) β Fin) |
6 | | f1f 6743 |
. . . . . 6
β’ (π:π΄β1-1βπ΅ β π:π΄βΆπ΅) |
7 | 2, 3 | elmapd 8786 |
. . . . . 6
β’ (π β (π β (π΅ βm π΄) β π:π΄βΆπ΅)) |
8 | 6, 7 | syl5ibr 246 |
. . . . 5
β’ (π β (π:π΄β1-1βπ΅ β π β (π΅ βm π΄))) |
9 | 8 | abssdv 4030 |
. . . 4
β’ (π β {π β£ π:π΄β1-1βπ΅} β (π΅ βm π΄)) |
10 | 5, 9 | ssfid 9218 |
. . 3
β’ (π β {π β£ π:π΄β1-1βπ΅} β Fin) |
11 | | sseq1 3974 |
. . . . . 6
β’ (π₯ = β
β (π₯ β {π β£ π:π΄β1-1βπ΅} β β
β {π β£ π:π΄β1-1βπ΅})) |
12 | | eleq2 2827 |
. . . . . . . . . . . . 13
β’ (π₯ = β
β ((π βΎ π΄) β π₯ β (π βΎ π΄) β β
)) |
13 | | noel 4295 |
. . . . . . . . . . . . . 14
β’ Β¬
(π βΎ π΄) β
β
|
14 | 13 | pm2.21i 119 |
. . . . . . . . . . . . 13
β’ ((π βΎ π΄) β β
β π β β
) |
15 | 12, 14 | syl6bi 253 |
. . . . . . . . . . . 12
β’ (π₯ = β
β ((π βΎ π΄) β π₯ β π β β
)) |
16 | 15 | adantrd 493 |
. . . . . . . . . . 11
β’ (π₯ = β
β (((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β π β β
)) |
17 | 16 | abssdv 4030 |
. . . . . . . . . 10
β’ (π₯ = β
β {π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β β
) |
18 | | ss0 4363 |
. . . . . . . . . 10
β’ ({π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β β
β {π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} = β
) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
β’ (π₯ = β
β {π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} = β
) |
20 | 19 | fveq2d 6851 |
. . . . . . . 8
β’ (π₯ = β
β
(β―β{π β£
((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) =
(β―ββ
)) |
21 | | hash0 14274 |
. . . . . . . 8
β’
(β―ββ
) = 0 |
22 | 20, 21 | eqtrdi 2793 |
. . . . . . 7
β’ (π₯ = β
β
(β―β{π β£
((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = 0) |
23 | | fveq2 6847 |
. . . . . . . . 9
β’ (π₯ = β
β
(β―βπ₯) =
(β―ββ
)) |
24 | 23, 21 | eqtrdi 2793 |
. . . . . . . 8
β’ (π₯ = β
β
(β―βπ₯) =
0) |
25 | 24 | oveq2d 7378 |
. . . . . . 7
β’ (π₯ = β
β
(((β―βπ΅) β
(β―βπ΄)) Β·
(β―βπ₯)) =
(((β―βπ΅) β
(β―βπ΄)) Β·
0)) |
26 | 22, 25 | eqeq12d 2753 |
. . . . . 6
β’ (π₯ = β
β
((β―β{π β£
((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ₯)) β 0 =
(((β―βπ΅) β
(β―βπ΄)) Β·
0))) |
27 | 11, 26 | imbi12d 345 |
. . . . 5
β’ (π₯ = β
β ((π₯ β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ₯))) β (β
β
{π β£ π:π΄β1-1βπ΅} β 0 = (((β―βπ΅) β (β―βπ΄)) Β·
0)))) |
28 | 27 | imbi2d 341 |
. . . 4
β’ (π₯ = β
β ((π β (π₯ β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ₯)))) β (π β (β
β {π β£ π:π΄β1-1βπ΅} β 0 = (((β―βπ΅) β (β―βπ΄)) Β·
0))))) |
29 | | sseq1 3974 |
. . . . . 6
β’ (π₯ = π¦ β (π₯ β {π β£ π:π΄β1-1βπ΅} β π¦ β {π β£ π:π΄β1-1βπ΅})) |
30 | | eleq2 2827 |
. . . . . . . . . 10
β’ (π₯ = π¦ β ((π βΎ π΄) β π₯ β (π βΎ π΄) β π¦)) |
31 | 30 | anbi1d 631 |
. . . . . . . . 9
β’ (π₯ = π¦ β (((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅))) |
32 | 31 | abbidv 2806 |
. . . . . . . 8
β’ (π₯ = π¦ β {π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} = {π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) |
33 | 32 | fveq2d 6851 |
. . . . . . 7
β’ (π₯ = π¦ β (β―β{π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)})) |
34 | | fveq2 6847 |
. . . . . . . 8
β’ (π₯ = π¦ β (β―βπ₯) = (β―βπ¦)) |
35 | 34 | oveq2d 7378 |
. . . . . . 7
β’ (π₯ = π¦ β (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ₯)) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ¦))) |
36 | 33, 35 | eqeq12d 2753 |
. . . . . 6
β’ (π₯ = π¦ β ((β―β{π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ₯)) β (β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ¦)))) |
37 | 29, 36 | imbi12d 345 |
. . . . 5
β’ (π₯ = π¦ β ((π₯ β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ₯))) β (π¦ β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ¦))))) |
38 | 37 | imbi2d 341 |
. . . 4
β’ (π₯ = π¦ β ((π β (π₯ β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ₯)))) β (π β (π¦ β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ¦)))))) |
39 | | sseq1 3974 |
. . . . . 6
β’ (π₯ = (π¦ βͺ {π}) β (π₯ β {π β£ π:π΄β1-1βπ΅} β (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) |
40 | | eleq2 2827 |
. . . . . . . . . 10
β’ (π₯ = (π¦ βͺ {π}) β ((π βΎ π΄) β π₯ β (π βΎ π΄) β (π¦ βͺ {π}))) |
41 | 40 | anbi1d 631 |
. . . . . . . . 9
β’ (π₯ = (π¦ βͺ {π}) β (((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅))) |
42 | 41 | abbidv 2806 |
. . . . . . . 8
β’ (π₯ = (π¦ βͺ {π}) β {π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} = {π β£ ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) |
43 | 42 | fveq2d 6851 |
. . . . . . 7
β’ (π₯ = (π¦ βͺ {π}) β (β―β{π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (β―β{π β£ ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅)})) |
44 | | fveq2 6847 |
. . . . . . . 8
β’ (π₯ = (π¦ βͺ {π}) β (β―βπ₯) = (β―β(π¦ βͺ {π}))) |
45 | 44 | oveq2d 7378 |
. . . . . . 7
β’ (π₯ = (π¦ βͺ {π}) β (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ₯)) = (((β―βπ΅) β (β―βπ΄)) Β·
(β―β(π¦ βͺ
{π})))) |
46 | 43, 45 | eqeq12d 2753 |
. . . . . 6
β’ (π₯ = (π¦ βͺ {π}) β ((β―β{π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ₯)) β (β―β{π β£ ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―β(π¦ βͺ {π}))))) |
47 | 39, 46 | imbi12d 345 |
. . . . 5
β’ (π₯ = (π¦ βͺ {π}) β ((π₯ β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ₯))) β ((π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―β(π¦ βͺ {π})))))) |
48 | 47 | imbi2d 341 |
. . . 4
β’ (π₯ = (π¦ βͺ {π}) β ((π β (π₯ β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ₯)))) β (π β ((π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―β(π¦ βͺ {π}))))))) |
49 | | sseq1 3974 |
. . . . . 6
β’ (π₯ = {π β£ π:π΄β1-1βπ΅} β (π₯ β {π β£ π:π΄β1-1βπ΅} β {π β£ π:π΄β1-1βπ΅} β {π β£ π:π΄β1-1βπ΅})) |
50 | | f1eq1 6738 |
. . . . . . . . . . 11
β’ (π = π¦ β (π:π΄β1-1βπ΅ β π¦:π΄β1-1βπ΅)) |
51 | 50 | cbvabv 2810 |
. . . . . . . . . 10
β’ {π β£ π:π΄β1-1βπ΅} = {π¦ β£ π¦:π΄β1-1βπ΅} |
52 | 51 | eqeq2i 2750 |
. . . . . . . . 9
β’ (π₯ = {π β£ π:π΄β1-1βπ΅} β π₯ = {π¦ β£ π¦:π΄β1-1βπ΅}) |
53 | | ssun1 4137 |
. . . . . . . . . . . . . . 15
β’ π΄ β (π΄ βͺ {π§}) |
54 | | f1ssres 6751 |
. . . . . . . . . . . . . . 15
β’ ((π:(π΄ βͺ {π§})β1-1βπ΅ β§ π΄ β (π΄ βͺ {π§})) β (π βΎ π΄):π΄β1-1βπ΅) |
55 | 53, 54 | mpan2 690 |
. . . . . . . . . . . . . 14
β’ (π:(π΄ βͺ {π§})β1-1βπ΅ β (π βΎ π΄):π΄β1-1βπ΅) |
56 | | vex 3452 |
. . . . . . . . . . . . . . . 16
β’ π β V |
57 | 56 | resex 5990 |
. . . . . . . . . . . . . . 15
β’ (π βΎ π΄) β V |
58 | | f1eq1 6738 |
. . . . . . . . . . . . . . 15
β’ (π¦ = (π βΎ π΄) β (π¦:π΄β1-1βπ΅ β (π βΎ π΄):π΄β1-1βπ΅)) |
59 | 57, 58 | elab 3635 |
. . . . . . . . . . . . . 14
β’ ((π βΎ π΄) β {π¦ β£ π¦:π΄β1-1βπ΅} β (π βΎ π΄):π΄β1-1βπ΅) |
60 | 55, 59 | sylibr 233 |
. . . . . . . . . . . . 13
β’ (π:(π΄ βͺ {π§})β1-1βπ΅ β (π βΎ π΄) β {π¦ β£ π¦:π΄β1-1βπ΅}) |
61 | | eleq2 2827 |
. . . . . . . . . . . . 13
β’ (π₯ = {π¦ β£ π¦:π΄β1-1βπ΅} β ((π βΎ π΄) β π₯ β (π βΎ π΄) β {π¦ β£ π¦:π΄β1-1βπ΅})) |
62 | 60, 61 | syl5ibr 246 |
. . . . . . . . . . . 12
β’ (π₯ = {π¦ β£ π¦:π΄β1-1βπ΅} β (π:(π΄ βͺ {π§})β1-1βπ΅ β (π βΎ π΄) β π₯)) |
63 | 62 | pm4.71rd 564 |
. . . . . . . . . . 11
β’ (π₯ = {π¦ β£ π¦:π΄β1-1βπ΅} β (π:(π΄ βͺ {π§})β1-1βπ΅ β ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅))) |
64 | 63 | bicomd 222 |
. . . . . . . . . 10
β’ (π₯ = {π¦ β£ π¦:π΄β1-1βπ΅} β (((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β π:(π΄ βͺ {π§})β1-1βπ΅)) |
65 | 64 | abbidv 2806 |
. . . . . . . . 9
β’ (π₯ = {π¦ β£ π¦:π΄β1-1βπ΅} β {π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} = {π β£ π:(π΄ βͺ {π§})β1-1βπ΅}) |
66 | 52, 65 | sylbi 216 |
. . . . . . . 8
β’ (π₯ = {π β£ π:π΄β1-1βπ΅} β {π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} = {π β£ π:(π΄ βͺ {π§})β1-1βπ΅}) |
67 | 66 | fveq2d 6851 |
. . . . . . 7
β’ (π₯ = {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (β―β{π β£ π:(π΄ βͺ {π§})β1-1βπ΅})) |
68 | | fveq2 6847 |
. . . . . . . 8
β’ (π₯ = {π β£ π:π΄β1-1βπ΅} β (β―βπ₯) = (β―β{π β£ π:π΄β1-1βπ΅})) |
69 | 68 | oveq2d 7378 |
. . . . . . 7
β’ (π₯ = {π β£ π:π΄β1-1βπ΅} β (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ₯)) = (((β―βπ΅) β (β―βπ΄)) Β·
(β―β{π β£
π:π΄β1-1βπ΅}))) |
70 | 67, 69 | eqeq12d 2753 |
. . . . . 6
β’ (π₯ = {π β£ π:π΄β1-1βπ΅} β ((β―β{π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ₯)) β (β―β{π β£ π:(π΄ βͺ {π§})β1-1βπ΅}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―β{π β£ π:π΄β1-1βπ΅})))) |
71 | 49, 70 | imbi12d 345 |
. . . . 5
β’ (π₯ = {π β£ π:π΄β1-1βπ΅} β ((π₯ β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ₯))) β ({π β£ π:π΄β1-1βπ΅} β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ π:(π΄ βͺ {π§})β1-1βπ΅}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―β{π β£ π:π΄β1-1βπ΅}))))) |
72 | 71 | imbi2d 341 |
. . . 4
β’ (π₯ = {π β£ π:π΄β1-1βπ΅} β ((π β (π₯ β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β π₯ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ₯)))) β (π β ({π β£ π:π΄β1-1βπ΅} β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ π:(π΄ βͺ {π§})β1-1βπ΅}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―β{π β£ π:π΄β1-1βπ΅})))))) |
73 | | hashcl 14263 |
. . . . . . . . . 10
β’ (π΅ β Fin β
(β―βπ΅) β
β0) |
74 | 2, 73 | syl 17 |
. . . . . . . . 9
β’ (π β (β―βπ΅) β
β0) |
75 | 74 | nn0cnd 12482 |
. . . . . . . 8
β’ (π β (β―βπ΅) β
β) |
76 | | hashcl 14263 |
. . . . . . . . . 10
β’ (π΄ β Fin β
(β―βπ΄) β
β0) |
77 | 3, 76 | syl 17 |
. . . . . . . . 9
β’ (π β (β―βπ΄) β
β0) |
78 | 77 | nn0cnd 12482 |
. . . . . . . 8
β’ (π β (β―βπ΄) β
β) |
79 | 75, 78 | subcld 11519 |
. . . . . . 7
β’ (π β ((β―βπ΅) β (β―βπ΄)) β
β) |
80 | 79 | mul01d 11361 |
. . . . . 6
β’ (π β (((β―βπ΅) β (β―βπ΄)) Β· 0) =
0) |
81 | 80 | eqcomd 2743 |
. . . . 5
β’ (π β 0 = (((β―βπ΅) β (β―βπ΄)) Β· 0)) |
82 | 81 | a1d 25 |
. . . 4
β’ (π β (β
β {π β£ π:π΄β1-1βπ΅} β 0 = (((β―βπ΅) β (β―βπ΄)) Β·
0))) |
83 | | ssun1 4137 |
. . . . . . . . 9
β’ π¦ β (π¦ βͺ {π}) |
84 | | sstr 3957 |
. . . . . . . . 9
β’ ((π¦ β (π¦ βͺ {π}) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅}) β π¦ β {π β£ π:π΄β1-1βπ΅}) |
85 | 83, 84 | mpan 689 |
. . . . . . . 8
β’ ((π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅} β π¦ β {π β£ π:π΄β1-1βπ΅}) |
86 | 85 | imim1i 63 |
. . . . . . 7
β’ ((π¦ β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ¦))) β ((π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ¦)))) |
87 | | oveq1 7369 |
. . . . . . . . . 10
β’
((β―β{π
β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ¦)) β ((β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) + ((β―βπ΅) β (β―βπ΄))) = ((((β―βπ΅) β (β―βπ΄)) Β· (β―βπ¦)) + ((β―βπ΅) β (β―βπ΄)))) |
88 | | elun 4113 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π βΎ π΄) β (π¦ βͺ {π}) β ((π βΎ π΄) β π¦ β¨ (π βΎ π΄) β {π})) |
89 | 57 | elsn 4606 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π βΎ π΄) β {π} β (π βΎ π΄) = π) |
90 | 89 | orbi2i 912 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π βΎ π΄) β π¦ β¨ (π βΎ π΄) β {π}) β ((π βΎ π΄) β π¦ β¨ (π βΎ π΄) = π)) |
91 | 88, 90 | bitri 275 |
. . . . . . . . . . . . . . . . . 18
β’ ((π βΎ π΄) β (π¦ βͺ {π}) β ((π βΎ π΄) β π¦ β¨ (π βΎ π΄) = π)) |
92 | 91 | anbi1i 625 |
. . . . . . . . . . . . . . . . 17
β’ (((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅) β (((π βΎ π΄) β π¦ β¨ (π βΎ π΄) = π) β§ π:(π΄ βͺ {π§})β1-1βπ΅)) |
93 | | andir 1008 |
. . . . . . . . . . . . . . . . 17
β’ ((((π βΎ π΄) β π¦ β¨ (π βΎ π΄) = π) β§ π:(π΄ βͺ {π§})β1-1βπ΅) β (((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β¨ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅))) |
94 | 92, 93 | bitri 275 |
. . . . . . . . . . . . . . . 16
β’ (((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅) β (((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β¨ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅))) |
95 | 94 | abbii 2807 |
. . . . . . . . . . . . . . 15
β’ {π β£ ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅)} = {π β£ (((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β¨ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅))} |
96 | | unab 4263 |
. . . . . . . . . . . . . . 15
β’ ({π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} βͺ {π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = {π β£ (((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β¨ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅))} |
97 | 95, 96 | eqtr4i 2768 |
. . . . . . . . . . . . . 14
β’ {π β£ ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅)} = ({π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} βͺ {π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) |
98 | 97 | fveq2i 6850 |
. . . . . . . . . . . . 13
β’
(β―β{π
β£ ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (β―β({π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} βͺ {π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)})) |
99 | | snfi 8995 |
. . . . . . . . . . . . . . . . . . 19
β’ {π§} β Fin |
100 | | unfi 9123 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β Fin β§ {π§} β Fin) β (π΄ βͺ {π§}) β Fin) |
101 | 3, 99, 100 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΄ βͺ {π§}) β Fin) |
102 | | mapvalg 8782 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΅ β Fin β§ (π΄ βͺ {π§}) β Fin) β (π΅ βm (π΄ βͺ {π§})) = {π β£ π:(π΄ βͺ {π§})βΆπ΅}) |
103 | 2, 101, 102 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΅ βm (π΄ βͺ {π§})) = {π β£ π:(π΄ βͺ {π§})βΆπ΅}) |
104 | | mapfi 9299 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΅ β Fin β§ (π΄ βͺ {π§}) β Fin) β (π΅ βm (π΄ βͺ {π§})) β Fin) |
105 | 2, 101, 104 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΅ βm (π΄ βͺ {π§})) β Fin) |
106 | 103, 105 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . 16
β’ (π β {π β£ π:(π΄ βͺ {π§})βΆπ΅} β Fin) |
107 | | f1f 6743 |
. . . . . . . . . . . . . . . . . 18
β’ (π:(π΄ βͺ {π§})β1-1βπ΅ β π:(π΄ βͺ {π§})βΆπ΅) |
108 | 107 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β π:(π΄ βͺ {π§})βΆπ΅) |
109 | 108 | ss2abi 4028 |
. . . . . . . . . . . . . . . 16
β’ {π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β {π β£ π:(π΄ βͺ {π§})βΆπ΅} |
110 | | ssfi 9124 |
. . . . . . . . . . . . . . . 16
β’ (({π β£ π:(π΄ βͺ {π§})βΆπ΅} β Fin β§ {π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β {π β£ π:(π΄ βͺ {π§})βΆπ΅}) β {π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β Fin) |
111 | 106, 109,
110 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ (π β {π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β Fin) |
112 | 111 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β {π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β Fin) |
113 | 107 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅) β π:(π΄ βͺ {π§})βΆπ΅) |
114 | 113 | ss2abi 4028 |
. . . . . . . . . . . . . . . 16
β’ {π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β {π β£ π:(π΄ βͺ {π§})βΆπ΅} |
115 | | ssfi 9124 |
. . . . . . . . . . . . . . . 16
β’ (({π β£ π:(π΄ βͺ {π§})βΆπ΅} β Fin β§ {π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β {π β£ π:(π΄ βͺ {π§})βΆπ΅}) β {π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β Fin) |
116 | 106, 114,
115 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ (π β {π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β Fin) |
117 | 116 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β {π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β Fin) |
118 | | inab 4264 |
. . . . . . . . . . . . . . 15
β’ ({π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β© {π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = {π β£ (((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β§ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅))} |
119 | | simprlr 779 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β Β¬ π β π¦) |
120 | | abn0 4345 |
. . . . . . . . . . . . . . . . . 18
β’ ({π β£ (((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β§ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅))} β β
β βπ(((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β§ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅))) |
121 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β§ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)) β (π βΎ π΄) = π) |
122 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β§ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)) β (π βΎ π΄) β π¦) |
123 | 121, 122 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β§ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)) β π β π¦) |
124 | 123 | exlimiv 1934 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ(((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β§ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)) β π β π¦) |
125 | 120, 124 | sylbi 216 |
. . . . . . . . . . . . . . . . 17
β’ ({π β£ (((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β§ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅))} β β
β π β π¦) |
126 | 125 | necon1bi 2973 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π β π¦ β {π β£ (((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β§ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅))} = β
) |
127 | 119, 126 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β {π β£ (((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅) β§ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅))} = β
) |
128 | 118, 127 | eqtrid 2789 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β ({π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β© {π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = β
) |
129 | | hashun 14289 |
. . . . . . . . . . . . . 14
β’ (({π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β Fin β§ {π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β Fin β§ ({π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β© {π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = β
) β (β―β({π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} βͺ {π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)})) = ((β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) + (β―β{π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)}))) |
130 | 112, 117,
128, 129 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β (β―β({π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} βͺ {π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)})) = ((β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) + (β―β{π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)}))) |
131 | 98, 130 | eqtrid 2789 |
. . . . . . . . . . . 12
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β (β―β{π β£ ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = ((β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) + (β―β{π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)}))) |
132 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ (((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅}) β (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅}) |
133 | 132 | unssbd 4153 |
. . . . . . . . . . . . . . . 16
β’ (((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅}) β {π} β {π β£ π:π΄β1-1βπ΅}) |
134 | | vex 3452 |
. . . . . . . . . . . . . . . . 17
β’ π β V |
135 | 134 | snss 4751 |
. . . . . . . . . . . . . . . 16
β’ (π β {π β£ π:π΄β1-1βπ΅} β {π} β {π β£ π:π΄β1-1βπ΅}) |
136 | 133, 135 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ (((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅}) β π β {π β£ π:π΄β1-1βπ΅}) |
137 | | f1eq1 6738 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π:π΄β1-1βπ΅ β π:π΄β1-1βπ΅)) |
138 | 134, 137 | elab 3635 |
. . . . . . . . . . . . . . 15
β’ (π β {π β£ π:π΄β1-1βπ΅} β π:π΄β1-1βπ΅) |
139 | 136, 138 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅}) β π:π΄β1-1βπ΅) |
140 | 78 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π:π΄β1-1βπ΅) β (β―βπ΄) β β) |
141 | 116 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π:π΄β1-1βπ΅) β {π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β Fin) |
142 | | hashcl 14263 |
. . . . . . . . . . . . . . . . . 18
β’ ({π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β Fin β (β―β{π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) β
β0) |
143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π:π΄β1-1βπ΅) β (β―β{π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) β
β0) |
144 | 143 | nn0cnd 12482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π:π΄β1-1βπ΅) β (β―β{π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) β β) |
145 | 140, 144 | pncan2d 11521 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π:π΄β1-1βπ΅) β (((β―βπ΄) + (β―β{π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)})) β (β―βπ΄)) = (β―β{π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)})) |
146 | | f1f1orn 6800 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π:π΄β1-1βπ΅ β π:π΄β1-1-ontoβran
π) |
147 | 146 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π:π΄β1-1βπ΅) β π:π΄β1-1-ontoβran
π) |
148 | | f1oen3g 8913 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β V β§ π:π΄β1-1-ontoβran
π) β π΄ β ran π) |
149 | 134, 147,
148 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π:π΄β1-1βπ΅) β π΄ β ran π) |
150 | | hasheni 14255 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β ran π β (β―βπ΄) = (β―βran π)) |
151 | 149, 150 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π:π΄β1-1βπ΅) β (β―βπ΄) = (β―βran π)) |
152 | 3 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π:π΄β1-1βπ΅) β π΄ β Fin) |
153 | 2 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π:π΄β1-1βπ΅) β π΅ β Fin) |
154 | | hashf1lem2.3 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Β¬ π§ β π΄) |
155 | 154 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π:π΄β1-1βπ΅) β Β¬ π§ β π΄) |
156 | | hashf1lem2.4 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((β―βπ΄) + 1) β€ (β―βπ΅)) |
157 | 156 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π:π΄β1-1βπ΅) β ((β―βπ΄) + 1) β€ (β―βπ΅)) |
158 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π:π΄β1-1βπ΅) β π:π΄β1-1βπ΅) |
159 | 152, 153,
155, 157, 158 | hashf1lem1 14360 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π:π΄β1-1βπ΅) β {π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β (π΅ β ran π)) |
160 | | hasheni 14255 |
. . . . . . . . . . . . . . . . . . 19
β’ ({π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β (π΅ β ran π) β (β―β{π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (β―β(π΅ β ran π))) |
161 | 159, 160 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π:π΄β1-1βπ΅) β (β―β{π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (β―β(π΅ β ran π))) |
162 | 151, 161 | oveq12d 7380 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π:π΄β1-1βπ΅) β ((β―βπ΄) + (β―β{π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)})) = ((β―βran π) + (β―β(π΅ β ran π)))) |
163 | | f1f 6743 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π:π΄β1-1βπ΅ β π:π΄βΆπ΅) |
164 | 163 | frnd 6681 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π:π΄β1-1βπ΅ β ran π β π΅) |
165 | 164 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π:π΄β1-1βπ΅) β ran π β π΅) |
166 | 153, 165 | ssfid 9218 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π:π΄β1-1βπ΅) β ran π β Fin) |
167 | | diffi 9130 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΅ β Fin β (π΅ β ran π) β Fin) |
168 | 153, 167 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π:π΄β1-1βπ΅) β (π΅ β ran π) β Fin) |
169 | | disjdif 4436 |
. . . . . . . . . . . . . . . . . . 19
β’ (ran
π β© (π΅ β ran π)) = β
|
170 | 169 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π:π΄β1-1βπ΅) β (ran π β© (π΅ β ran π)) = β
) |
171 | | hashun 14289 |
. . . . . . . . . . . . . . . . . 18
β’ ((ran
π β Fin β§ (π΅ β ran π) β Fin β§ (ran π β© (π΅ β ran π)) = β
) β (β―β(ran
π βͺ (π΅ β ran π))) = ((β―βran π) + (β―β(π΅ β ran π)))) |
172 | 166, 168,
170, 171 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π:π΄β1-1βπ΅) β (β―β(ran π βͺ (π΅ β ran π))) = ((β―βran π) + (β―β(π΅ β ran π)))) |
173 | | undif 4446 |
. . . . . . . . . . . . . . . . . . 19
β’ (ran
π β π΅ β (ran π βͺ (π΅ β ran π)) = π΅) |
174 | 165, 173 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π:π΄β1-1βπ΅) β (ran π βͺ (π΅ β ran π)) = π΅) |
175 | 174 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π:π΄β1-1βπ΅) β (β―β(ran π βͺ (π΅ β ran π))) = (β―βπ΅)) |
176 | 162, 172,
175 | 3eqtr2d 2783 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π:π΄β1-1βπ΅) β ((β―βπ΄) + (β―β{π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)})) = (β―βπ΅)) |
177 | 176 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π:π΄β1-1βπ΅) β (((β―βπ΄) + (β―β{π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)})) β (β―βπ΄)) = ((β―βπ΅) β (β―βπ΄))) |
178 | 145, 177 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
β’ ((π β§ π:π΄β1-1βπ΅) β (β―β{π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = ((β―βπ΅) β (β―βπ΄))) |
179 | 139, 178 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β (β―β{π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = ((β―βπ΅) β (β―βπ΄))) |
180 | 179 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β ((β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) + (β―β{π β£ ((π βΎ π΄) = π β§ π:(π΄ βͺ {π§})β1-1βπ΅)})) = ((β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) + ((β―βπ΅) β (β―βπ΄)))) |
181 | 131, 180 | eqtrd 2777 |
. . . . . . . . . . 11
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β (β―β{π β£ ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = ((β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) + ((β―βπ΅) β (β―βπ΄)))) |
182 | | hashunsng 14299 |
. . . . . . . . . . . . . . 15
β’ (π β V β ((π¦ β Fin β§ Β¬ π β π¦) β (β―β(π¦ βͺ {π})) = ((β―βπ¦) + 1))) |
183 | 182 | elv 3454 |
. . . . . . . . . . . . . 14
β’ ((π¦ β Fin β§ Β¬ π β π¦) β (β―β(π¦ βͺ {π})) = ((β―βπ¦) + 1)) |
184 | 183 | ad2antrl 727 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β (β―β(π¦ βͺ {π})) = ((β―βπ¦) + 1)) |
185 | 184 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β (((β―βπ΅) β (β―βπ΄)) Β·
(β―β(π¦ βͺ
{π}))) =
(((β―βπ΅) β
(β―βπ΄)) Β·
((β―βπ¦) +
1))) |
186 | 79 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β ((β―βπ΅) β (β―βπ΄)) β β) |
187 | | simprll 778 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β π¦ β Fin) |
188 | | hashcl 14263 |
. . . . . . . . . . . . . . 15
β’ (π¦ β Fin β
(β―βπ¦) β
β0) |
189 | 187, 188 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β (β―βπ¦) β
β0) |
190 | 189 | nn0cnd 12482 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β (β―βπ¦) β β) |
191 | | 1cnd 11157 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β 1 β
β) |
192 | 186, 190,
191 | adddid 11186 |
. . . . . . . . . . . 12
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β (((β―βπ΅) β (β―βπ΄)) Β·
((β―βπ¦) + 1)) =
((((β―βπ΅)
β (β―βπ΄))
Β· (β―βπ¦))
+ (((β―βπ΅)
β (β―βπ΄))
Β· 1))) |
193 | 186 | mulid1d 11179 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β (((β―βπ΅) β (β―βπ΄)) Β· 1) =
((β―βπ΅) β
(β―βπ΄))) |
194 | 193 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β ((((β―βπ΅) β (β―βπ΄)) Β· (β―βπ¦)) + (((β―βπ΅) β (β―βπ΄)) Β· 1)) =
((((β―βπ΅)
β (β―βπ΄))
Β· (β―βπ¦))
+ ((β―βπ΅)
β (β―βπ΄)))) |
195 | 185, 192,
194 | 3eqtrd 2781 |
. . . . . . . . . . 11
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β (((β―βπ΅) β (β―βπ΄)) Β·
(β―β(π¦ βͺ
{π}))) =
((((β―βπ΅)
β (β―βπ΄))
Β· (β―βπ¦))
+ ((β―βπ΅)
β (β―βπ΄)))) |
196 | 181, 195 | eqeq12d 2753 |
. . . . . . . . . 10
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β ((β―β{π β£ ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―β(π¦ βͺ {π}))) β ((β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) + ((β―βπ΅) β (β―βπ΄))) = ((((β―βπ΅) β (β―βπ΄)) Β· (β―βπ¦)) + ((β―βπ΅) β (β―βπ΄))))) |
197 | 87, 196 | syl5ibr 246 |
. . . . . . . . 9
β’ ((π β§ ((π¦ β Fin β§ Β¬ π β π¦) β§ (π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅})) β ((β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ¦)) β (β―β{π β£ ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―β(π¦ βͺ {π}))))) |
198 | 197 | expr 458 |
. . . . . . . 8
β’ ((π β§ (π¦ β Fin β§ Β¬ π β π¦)) β ((π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅} β ((β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ¦)) β (β―β{π β£ ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―β(π¦ βͺ {π})))))) |
199 | 198 | a2d 29 |
. . . . . . 7
β’ ((π β§ (π¦ β Fin β§ Β¬ π β π¦)) β (((π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ¦))) β ((π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―β(π¦ βͺ {π})))))) |
200 | 86, 199 | syl5 34 |
. . . . . 6
β’ ((π β§ (π¦ β Fin β§ Β¬ π β π¦)) β ((π¦ β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ¦))) β ((π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―β(π¦ βͺ {π})))))) |
201 | 200 | expcom 415 |
. . . . 5
β’ ((π¦ β Fin β§ Β¬ π β π¦) β (π β ((π¦ β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ¦))) β ((π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―β(π¦ βͺ {π}))))))) |
202 | 201 | a2d 29 |
. . . 4
β’ ((π¦ β Fin β§ Β¬ π β π¦) β ((π β (π¦ β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β π¦ β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―βπ¦)))) β (π β ((π¦ βͺ {π}) β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ ((π βΎ π΄) β (π¦ βͺ {π}) β§ π:(π΄ βͺ {π§})β1-1βπ΅)}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―β(π¦ βͺ {π}))))))) |
203 | 28, 38, 48, 72, 82, 202 | findcard2s 9116 |
. . 3
β’ ({π β£ π:π΄β1-1βπ΅} β Fin β (π β ({π β£ π:π΄β1-1βπ΅} β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ π:(π΄ βͺ {π§})β1-1βπ΅}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―β{π β£ π:π΄β1-1βπ΅}))))) |
204 | 10, 203 | mpcom 38 |
. 2
β’ (π β ({π β£ π:π΄β1-1βπ΅} β {π β£ π:π΄β1-1βπ΅} β (β―β{π β£ π:(π΄ βͺ {π§})β1-1βπ΅}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―β{π β£ π:π΄β1-1βπ΅})))) |
205 | 1, 204 | mpi 20 |
1
β’ (π β (β―β{π β£ π:(π΄ βͺ {π§})β1-1βπ΅}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―β{π β£ π:π΄β1-1βπ΅}))) |