Step | Hyp | Ref
| Expression |
1 | | bitsf1o 16332 |
. . . . 5
β’ (bits
βΎ β0):β0β1-1-ontoβ(π« β0 β©
Fin) |
2 | | f1of 6789 |
. . . . 5
β’ ((bits
βΎ β0):β0β1-1-ontoβ(π« β0 β© Fin)
β (bits βΎ β0):β0βΆ(π«
β0 β© Fin)) |
3 | 1, 2 | ax-mp 5 |
. . . 4
β’ (bits
βΎ β0):β0βΆ(π«
β0 β© Fin) |
4 | | eulerpart.p |
. . . . . . . . 9
β’ π = {π β (β0
βm β) β£ ((β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π)} |
5 | | eulerpart.o |
. . . . . . . . 9
β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} |
6 | | eulerpart.d |
. . . . . . . . 9
β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} |
7 | | eulerpart.j |
. . . . . . . . 9
β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} |
8 | | eulerpart.f |
. . . . . . . . 9
β’ πΉ = (π₯ β π½, π¦ β β0 β¦
((2βπ¦) Β· π₯)) |
9 | | eulerpart.h |
. . . . . . . . 9
β’ π» = {π β ((π« β0 β©
Fin) βm π½)
β£ (π supp β
)
β Fin} |
10 | | eulerpart.m |
. . . . . . . . 9
β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) |
11 | | eulerpart.r |
. . . . . . . . 9
β’ π
= {π β£ (β‘π β β) β
Fin} |
12 | | eulerpart.t |
. . . . . . . . 9
β’ π = {π β (β0
βm β) β£ (β‘π β β) β π½} |
13 | 4, 5, 6, 7, 8, 9, 10, 11, 12 | eulerpartlemt0 33009 |
. . . . . . . 8
β’ (π΄ β (π β© π
) β (π΄ β (β0
βm β) β§ (β‘π΄ β β) β Fin β§ (β‘π΄ β β) β π½)) |
14 | 13 | biimpi 215 |
. . . . . . 7
β’ (π΄ β (π β© π
) β (π΄ β (β0
βm β) β§ (β‘π΄ β β) β Fin β§ (β‘π΄ β β) β π½)) |
15 | 14 | simp1d 1143 |
. . . . . 6
β’ (π΄ β (π β© π
) β π΄ β (β0
βm β)) |
16 | | nn0ex 12426 |
. . . . . . 7
β’
β0 β V |
17 | | nnex 12166 |
. . . . . . 7
β’ β
β V |
18 | 16, 17 | elmap 8816 |
. . . . . 6
β’ (π΄ β (β0
βm β) β π΄:ββΆβ0) |
19 | 15, 18 | sylib 217 |
. . . . 5
β’ (π΄ β (π β© π
) β π΄:ββΆβ0) |
20 | | ssrab2 4042 |
. . . . . 6
β’ {π§ β β β£ Β¬ 2
β₯ π§} β
β |
21 | 7, 20 | eqsstri 3983 |
. . . . 5
β’ π½ β
β |
22 | | fssres 6713 |
. . . . 5
β’ ((π΄:ββΆβ0 β§
π½ β β) β
(π΄ βΎ π½):π½βΆβ0) |
23 | 19, 21, 22 | sylancl 587 |
. . . 4
β’ (π΄ β (π β© π
) β (π΄ βΎ π½):π½βΆβ0) |
24 | | fco2 6700 |
. . . 4
β’ (((bits
βΎ β0):β0βΆ(π«
β0 β© Fin) β§ (π΄ βΎ π½):π½βΆβ0) β (bits
β (π΄ βΎ π½)):π½βΆ(π« β0 β©
Fin)) |
25 | 3, 23, 24 | sylancr 588 |
. . 3
β’ (π΄ β (π β© π
) β (bits β (π΄ βΎ π½)):π½βΆ(π« β0 β©
Fin)) |
26 | 16 | pwex 5340 |
. . . . 5
β’ π«
β0 β V |
27 | 26 | inex1 5279 |
. . . 4
β’
(π« β0 β© Fin) β V |
28 | 17, 21 | ssexi 5284 |
. . . 4
β’ π½ β V |
29 | 27, 28 | elmap 8816 |
. . 3
β’ ((bits
β (π΄ βΎ π½)) β ((π«
β0 β© Fin) βm π½) β (bits β (π΄ βΎ π½)):π½βΆ(π« β0 β©
Fin)) |
30 | 25, 29 | sylibr 233 |
. 2
β’ (π΄ β (π β© π
) β (bits β (π΄ βΎ π½)) β ((π« β0
β© Fin) βm π½)) |
31 | 14 | simp2d 1144 |
. . . . 5
β’ (π΄ β (π β© π
) β (β‘π΄ β β) β
Fin) |
32 | | 0nn0 12435 |
. . . . . . . . 9
β’ 0 β
β0 |
33 | | suppimacnv 8110 |
. . . . . . . . 9
β’ ((π΄ β (π β© π
) β§ 0 β β0) β
(π΄ supp 0) = (β‘π΄ β (V β {0}))) |
34 | 32, 33 | mpan2 690 |
. . . . . . . 8
β’ (π΄ β (π β© π
) β (π΄ supp 0) = (β‘π΄ β (V β {0}))) |
35 | | fsuppeq 8111 |
. . . . . . . . . 10
β’ ((β
β V β§ 0 β β0) β (π΄:ββΆβ0 β
(π΄ supp 0) = (β‘π΄ β (β0 β
{0})))) |
36 | 17, 32, 35 | mp2an 691 |
. . . . . . . . 9
β’ (π΄:ββΆβ0 β
(π΄ supp 0) = (β‘π΄ β (β0 β
{0}))) |
37 | 19, 36 | syl 17 |
. . . . . . . 8
β’ (π΄ β (π β© π
) β (π΄ supp 0) = (β‘π΄ β (β0 β
{0}))) |
38 | 34, 37 | eqtr3d 2779 |
. . . . . . 7
β’ (π΄ β (π β© π
) β (β‘π΄ β (V β {0})) = (β‘π΄ β (β0 β
{0}))) |
39 | 38 | eleq1d 2823 |
. . . . . 6
β’ (π΄ β (π β© π
) β ((β‘π΄ β (V β {0})) β Fin β
(β‘π΄ β (β0 β {0}))
β Fin)) |
40 | | dfn2 12433 |
. . . . . . . 8
β’ β =
(β0 β {0}) |
41 | 40 | imaeq2i 6016 |
. . . . . . 7
β’ (β‘π΄ β β) = (β‘π΄ β (β0 β
{0})) |
42 | 41 | eleq1i 2829 |
. . . . . 6
β’ ((β‘π΄ β β) β Fin β (β‘π΄ β (β0 β {0}))
β Fin) |
43 | 39, 42 | bitr4di 289 |
. . . . 5
β’ (π΄ β (π β© π
) β ((β‘π΄ β (V β {0})) β Fin β
(β‘π΄ β β) β
Fin)) |
44 | 31, 43 | mpbird 257 |
. . . 4
β’ (π΄ β (π β© π
) β (β‘π΄ β (V β {0})) β
Fin) |
45 | | resss 5967 |
. . . . 5
β’ (π΄ βΎ π½) β π΄ |
46 | | cnvss 5833 |
. . . . 5
β’ ((π΄ βΎ π½) β π΄ β β‘(π΄ βΎ π½) β β‘π΄) |
47 | | imass1 6058 |
. . . . 5
β’ (β‘(π΄ βΎ π½) β β‘π΄ β (β‘(π΄ βΎ π½) β (V β {0})) β (β‘π΄ β (V β {0}))) |
48 | 45, 46, 47 | mp2b 10 |
. . . 4
β’ (β‘(π΄ βΎ π½) β (V β {0})) β (β‘π΄ β (V β {0})) |
49 | | ssfi 9124 |
. . . 4
β’ (((β‘π΄ β (V β {0})) β Fin β§
(β‘(π΄ βΎ π½) β (V β {0})) β (β‘π΄ β (V β {0}))) β (β‘(π΄ βΎ π½) β (V β {0})) β
Fin) |
50 | 44, 48, 49 | sylancl 587 |
. . 3
β’ (π΄ β (π β© π
) β (β‘(π΄ βΎ π½) β (V β {0})) β
Fin) |
51 | | cnvco 5846 |
. . . . . 6
β’ β‘(bits β (π΄ βΎ π½)) = (β‘(π΄ βΎ π½) β β‘bits) |
52 | 51 | imaeq1i 6015 |
. . . . 5
β’ (β‘(bits β (π΄ βΎ π½)) β (V β {β
})) = ((β‘(π΄ βΎ π½) β β‘bits) β (V β
{β
})) |
53 | | imaco 6208 |
. . . . 5
β’ ((β‘(π΄ βΎ π½) β β‘bits) β (V β {β
})) =
(β‘(π΄ βΎ π½) β (β‘bits β (V β
{β
}))) |
54 | 52, 53 | eqtri 2765 |
. . . 4
β’ (β‘(bits β (π΄ βΎ π½)) β (V β {β
})) = (β‘(π΄ βΎ π½) β (β‘bits β (V β
{β
}))) |
55 | | ffun 6676 |
. . . . . 6
β’ (π΄:ββΆβ0 β
Fun π΄) |
56 | | funres 6548 |
. . . . . 6
β’ (Fun
π΄ β Fun (π΄ βΎ π½)) |
57 | 19, 55, 56 | 3syl 18 |
. . . . 5
β’ (π΄ β (π β© π
) β Fun (π΄ βΎ π½)) |
58 | | ssv 3973 |
. . . . . . 7
β’ (β‘bits β V) β V |
59 | | ssdif 4104 |
. . . . . . 7
β’ ((β‘bits β V) β V β ((β‘bits β V) β (β‘bits β {β
})) β (V β
(β‘bits β
{β
}))) |
60 | 58, 59 | ax-mp 5 |
. . . . . 6
β’ ((β‘bits β V) β (β‘bits β {β
})) β (V β
(β‘bits β
{β
})) |
61 | | bitsf 16314 |
. . . . . . 7
β’
bits:β€βΆπ« β0 |
62 | | ffun 6676 |
. . . . . . 7
β’
(bits:β€βΆπ« β0 β Fun
bits) |
63 | | difpreima 7020 |
. . . . . . 7
β’ (Fun bits
β (β‘bits β (V β
{β
})) = ((β‘bits β V)
β (β‘bits β
{β
}))) |
64 | 61, 62, 63 | mp2b 10 |
. . . . . 6
β’ (β‘bits β (V β {β
})) =
((β‘bits β V) β (β‘bits β {β
})) |
65 | | bitsf1 16333 |
. . . . . . . . 9
β’
bits:β€β1-1βπ« β0 |
66 | | 0z 12517 |
. . . . . . . . . 10
β’ 0 β
β€ |
67 | | snssi 4773 |
. . . . . . . . . 10
β’ (0 β
β€ β {0} β β€) |
68 | 66, 67 | ax-mp 5 |
. . . . . . . . 9
β’ {0}
β β€ |
69 | | f1imacnv 6805 |
. . . . . . . . 9
β’
((bits:β€β1-1βπ« β0 β§ {0} β
β€) β (β‘bits β (bits
β {0})) = {0}) |
70 | 65, 68, 69 | mp2an 691 |
. . . . . . . 8
β’ (β‘bits β (bits β {0})) =
{0} |
71 | | ffn 6673 |
. . . . . . . . . . . 12
β’
(bits:β€βΆπ« β0 β bits Fn
β€) |
72 | 61, 71 | ax-mp 5 |
. . . . . . . . . . 11
β’ bits Fn
β€ |
73 | | fnsnfv 6925 |
. . . . . . . . . . 11
β’ ((bits Fn
β€ β§ 0 β β€) β {(bitsβ0)} = (bits β
{0})) |
74 | 72, 66, 73 | mp2an 691 |
. . . . . . . . . 10
β’
{(bitsβ0)} = (bits β {0}) |
75 | | 0bits 16326 |
. . . . . . . . . . 11
β’
(bitsβ0) = β
|
76 | 75 | sneqi 4602 |
. . . . . . . . . 10
β’
{(bitsβ0)} = {β
} |
77 | 74, 76 | eqtr3i 2767 |
. . . . . . . . 9
β’ (bits
β {0}) = {β
} |
78 | 77 | imaeq2i 6016 |
. . . . . . . 8
β’ (β‘bits β (bits β {0})) = (β‘bits β {β
}) |
79 | 70, 78 | eqtr3i 2767 |
. . . . . . 7
β’ {0} =
(β‘bits β
{β
}) |
80 | 79 | difeq2i 4084 |
. . . . . 6
β’ (V
β {0}) = (V β (β‘bits
β {β
})) |
81 | 60, 64, 80 | 3sstr4i 3992 |
. . . . 5
β’ (β‘bits β (V β {β
})) β
(V β {0}) |
82 | | sspreima 7023 |
. . . . 5
β’ ((Fun
(π΄ βΎ π½) β§ (β‘bits β (V β {β
})) β
(V β {0})) β (β‘(π΄ βΎ π½) β (β‘bits β (V β {β
}))) β
(β‘(π΄ βΎ π½) β (V β {0}))) |
83 | 57, 81, 82 | sylancl 587 |
. . . 4
β’ (π΄ β (π β© π
) β (β‘(π΄ βΎ π½) β (β‘bits β (V β {β
}))) β
(β‘(π΄ βΎ π½) β (V β {0}))) |
84 | 54, 83 | eqsstrid 3997 |
. . 3
β’ (π΄ β (π β© π
) β (β‘(bits β (π΄ βΎ π½)) β (V β {β
})) β
(β‘(π΄ βΎ π½) β (V β {0}))) |
85 | | ssfi 9124 |
. . 3
β’ (((β‘(π΄ βΎ π½) β (V β {0})) β Fin β§
(β‘(bits β (π΄ βΎ π½)) β (V β {β
})) β
(β‘(π΄ βΎ π½) β (V β {0}))) β (β‘(bits β (π΄ βΎ π½)) β (V β {β
})) β
Fin) |
86 | 50, 84, 85 | syl2anc 585 |
. 2
β’ (π΄ β (π β© π
) β (β‘(bits β (π΄ βΎ π½)) β (V β {β
})) β
Fin) |
87 | | oveq1 7369 |
. . . . 5
β’ (π = (bits β (π΄ βΎ π½)) β (π supp β
) = ((bits β (π΄ βΎ π½)) supp β
)) |
88 | 87 | eleq1d 2823 |
. . . 4
β’ (π = (bits β (π΄ βΎ π½)) β ((π supp β
) β Fin β ((bits
β (π΄ βΎ π½)) supp β
) β
Fin)) |
89 | 88, 9 | elrab2 3653 |
. . 3
β’ ((bits
β (π΄ βΎ π½)) β π» β ((bits β (π΄ βΎ π½)) β ((π« β0
β© Fin) βm π½) β§ ((bits β (π΄ βΎ π½)) supp β
) β
Fin)) |
90 | | zex 12515 |
. . . . . 6
β’ β€
β V |
91 | | fex 7181 |
. . . . . 6
β’
((bits:β€βΆπ« β0 β§ β€ β
V) β bits β V) |
92 | 61, 90, 91 | mp2an 691 |
. . . . 5
β’ bits
β V |
93 | | resexg 5988 |
. . . . 5
β’ (π΄ β (π β© π
) β (π΄ βΎ π½) β V) |
94 | | coexg 7871 |
. . . . 5
β’ ((bits
β V β§ (π΄ βΎ
π½) β V) β (bits
β (π΄ βΎ π½)) β V) |
95 | 92, 93, 94 | sylancr 588 |
. . . 4
β’ (π΄ β (π β© π
) β (bits β (π΄ βΎ π½)) β V) |
96 | | 0ex 5269 |
. . . . . . 7
β’ β
β V |
97 | | suppimacnv 8110 |
. . . . . . 7
β’ (((bits
β (π΄ βΎ π½)) β V β§ β
β
V) β ((bits β (π΄
βΎ π½)) supp β
) =
(β‘(bits β (π΄ βΎ π½)) β (V β
{β
}))) |
98 | 96, 97 | mpan2 690 |
. . . . . 6
β’ ((bits
β (π΄ βΎ π½)) β V β ((bits
β (π΄ βΎ π½)) supp β
) = (β‘(bits β (π΄ βΎ π½)) β (V β
{β
}))) |
99 | 98 | eleq1d 2823 |
. . . . 5
β’ ((bits
β (π΄ βΎ π½)) β V β (((bits
β (π΄ βΎ π½)) supp β
) β Fin
β (β‘(bits β (π΄ βΎ π½)) β (V β {β
})) β
Fin)) |
100 | 99 | anbi2d 630 |
. . . 4
β’ ((bits
β (π΄ βΎ π½)) β V β (((bits
β (π΄ βΎ π½)) β ((π«
β0 β© Fin) βm π½) β§ ((bits β (π΄ βΎ π½)) supp β
) β Fin) β ((bits
β (π΄ βΎ π½)) β ((π«
β0 β© Fin) βm π½) β§ (β‘(bits β (π΄ βΎ π½)) β (V β {β
})) β
Fin))) |
101 | 95, 100 | syl 17 |
. . 3
β’ (π΄ β (π β© π
) β (((bits β (π΄ βΎ π½)) β ((π« β0
β© Fin) βm π½) β§ ((bits β (π΄ βΎ π½)) supp β
) β Fin) β ((bits
β (π΄ βΎ π½)) β ((π«
β0 β© Fin) βm π½) β§ (β‘(bits β (π΄ βΎ π½)) β (V β {β
})) β
Fin))) |
102 | 89, 101 | bitrid 283 |
. 2
β’ (π΄ β (π β© π
) β ((bits β (π΄ βΎ π½)) β π» β ((bits β (π΄ βΎ π½)) β ((π« β0
β© Fin) βm π½) β§ (β‘(bits β (π΄ βΎ π½)) β (V β {β
})) β
Fin))) |
103 | 30, 86, 102 | mpbir2and 712 |
1
β’ (π΄ β (π β© π
) β (bits β (π΄ βΎ π½)) β π») |