Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  eulerpartgbij Structured version   Visualization version   GIF version
Theorem eulerpartgbij 33670
Description: Lemma for eulerpart 33680: The 𝐺 function is a bijection. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
Hypotheses
Ref Expression
eulerpart.p 𝑃 = {𝑓 ∈ (β„•0 ↑m β„•) ∣ ((◑𝑓 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘“β€˜π‘˜) Β· π‘˜) = 𝑁)}
eulerpart.o 𝑂 = {𝑔 ∈ 𝑃 ∣ βˆ€π‘› ∈ (◑𝑔 β€œ β„•) Β¬ 2 βˆ₯ 𝑛}
eulerpart.d 𝐷 = {𝑔 ∈ 𝑃 ∣ βˆ€π‘› ∈ β„• (π‘”β€˜π‘›) ≀ 1}
eulerpart.j 𝐽 = {𝑧 ∈ β„• ∣ Β¬ 2 βˆ₯ 𝑧}
eulerpart.f 𝐹 = (π‘₯ ∈ 𝐽, 𝑦 ∈ β„•0 ↦ ((2↑𝑦) Β· π‘₯))
eulerpart.h 𝐻 = {π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin}
eulerpart.m 𝑀 = (π‘Ÿ ∈ 𝐻 ↦ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐽 ∧ 𝑦 ∈ (π‘Ÿβ€˜π‘₯))})
eulerpart.r 𝑅 = {𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin}
eulerpart.t 𝑇 = {𝑓 ∈ (β„•0 ↑m β„•) ∣ (◑𝑓 β€œ β„•) βŠ† 𝐽}
eulerpart.g 𝐺 = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ ((πŸ­β€˜β„•)β€˜(𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))))
Assertion
Ref Expression
eulerpartgbij 𝐺:(𝑇 ∩ 𝑅)–1-1-ontoβ†’(({0, 1} ↑m β„•) ∩ 𝑅)
Distinct variable groups:   𝑓,𝑔,π‘˜,𝑛,π‘œ,π‘₯,𝑦,𝑧   π‘œ,𝐹   𝑓,π‘Ÿ,𝐽,π‘œ,π‘₯,𝑦   π‘œ,𝑀,π‘Ÿ   𝑓,𝑁,𝑔,π‘₯   𝑃,𝑔   𝑅,𝑓,π‘œ   π‘œ,𝐻,π‘Ÿ   𝑇,𝑓,π‘œ
Allowed substitution hints:   𝐷(π‘₯,𝑦,𝑧,𝑓,𝑔,π‘˜,𝑛,π‘œ,π‘Ÿ)   𝑃(π‘₯,𝑦,𝑧,𝑓,π‘˜,𝑛,π‘œ,π‘Ÿ)   𝑅(π‘₯,𝑦,𝑧,𝑔,π‘˜,𝑛,π‘Ÿ)   𝑇(π‘₯,𝑦,𝑧,𝑔,π‘˜,𝑛,π‘Ÿ)   𝐹(π‘₯,𝑦,𝑧,𝑓,𝑔,π‘˜,𝑛,π‘Ÿ)   𝐺(π‘₯,𝑦,𝑧,𝑓,𝑔,π‘˜,𝑛,π‘œ,π‘Ÿ)   𝐻(π‘₯,𝑦,𝑧,𝑓,𝑔,π‘˜,𝑛)   𝐽(𝑧,𝑔,π‘˜,𝑛)   𝑀(π‘₯,𝑦,𝑧,𝑓,𝑔,π‘˜,𝑛)   𝑁(𝑦,𝑧,π‘˜,𝑛,π‘œ,π‘Ÿ)   𝑂(π‘₯,𝑦,𝑧,𝑓,𝑔,π‘˜,𝑛,π‘œ,π‘Ÿ)
Proof of Theorem eulerpartgbij
Dummy variables π‘Ž π‘š 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnex 12223 . . . . 5 β„• ∈ V
2 indf1ofs 33323 . . . . 5 (β„• ∈ V β†’ ((πŸ­β€˜β„•) β†Ύ Fin):(𝒫 β„• ∩ Fin)–1-1-ontoβ†’{𝑓 ∈ ({0, 1} ↑m β„•) ∣ (◑𝑓 β€œ {1}) ∈ Fin})
31, 2ax-mp 5 . . . 4 ((πŸ­β€˜β„•) β†Ύ Fin):(𝒫 β„• ∩ Fin)–1-1-ontoβ†’{𝑓 ∈ ({0, 1} ↑m β„•) ∣ (◑𝑓 β€œ {1}) ∈ Fin}
4 incom 4201 . . . . . . 7 (({0, 1} ↑m β„•) ∩ {𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin}) = ({𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin} ∩ ({0, 1} ↑m β„•))
5 eulerpart.r . . . . . . . 8 𝑅 = {𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin}
65ineq2i 4209 . . . . . . 7 (({0, 1} ↑m β„•) ∩ 𝑅) = (({0, 1} ↑m β„•) ∩ {𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin})
7 dfrab2 4310 . . . . . . 7 {𝑓 ∈ ({0, 1} ↑m β„•) ∣ (◑𝑓 β€œ β„•) ∈ Fin} = ({𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin} ∩ ({0, 1} ↑m β„•))
84, 6, 73eqtr4i 2769 . . . . . 6 (({0, 1} ↑m β„•) ∩ 𝑅) = {𝑓 ∈ ({0, 1} ↑m β„•) ∣ (◑𝑓 β€œ β„•) ∈ Fin}
9 elmapfun 8864 . . . . . . . . 9 (𝑓 ∈ ({0, 1} ↑m β„•) β†’ Fun 𝑓)
10 elmapi 8847 . . . . . . . . . 10 (𝑓 ∈ ({0, 1} ↑m β„•) β†’ 𝑓:β„•βŸΆ{0, 1})
1110frnd 6725 . . . . . . . . 9 (𝑓 ∈ ({0, 1} ↑m β„•) β†’ ran 𝑓 βŠ† {0, 1})
12 fimacnvinrn2 7074 . . . . . . . . . 10 ((Fun 𝑓 ∧ ran 𝑓 βŠ† {0, 1}) β†’ (◑𝑓 β€œ β„•) = (◑𝑓 β€œ (β„• ∩ {0, 1})))
13 df-pr 4631 . . . . . . . . . . . . . 14 {0, 1} = ({0} βˆͺ {1})
1413ineq2i 4209 . . . . . . . . . . . . 13 (β„• ∩ {0, 1}) = (β„• ∩ ({0} βˆͺ {1}))
15 indi 4273 . . . . . . . . . . . . 13 (β„• ∩ ({0} βˆͺ {1})) = ((β„• ∩ {0}) βˆͺ (β„• ∩ {1}))
16 0nnn 12253 . . . . . . . . . . . . . . 15 Β¬ 0 ∈ β„•
17 disjsn 4715 . . . . . . . . . . . . . . 15 ((β„• ∩ {0}) = βˆ… ↔ Β¬ 0 ∈ β„•)
1816, 17mpbir 230 . . . . . . . . . . . . . 14 (β„• ∩ {0}) = βˆ…
19 1nn 12228 . . . . . . . . . . . . . . . . 17 1 ∈ β„•
20 1ex 11215 . . . . . . . . . . . . . . . . . 18 1 ∈ V
2120snss 4789 . . . . . . . . . . . . . . . . 17 (1 ∈ β„• ↔ {1} βŠ† β„•)
2219, 21mpbi 229 . . . . . . . . . . . . . . . 16 {1} βŠ† β„•
23 dfss 3966 . . . . . . . . . . . . . . . 16 ({1} βŠ† β„• ↔ {1} = ({1} ∩ β„•))
2422, 23mpbi 229 . . . . . . . . . . . . . . 15 {1} = ({1} ∩ β„•)
25 incom 4201 . . . . . . . . . . . . . . 15 ({1} ∩ β„•) = (β„• ∩ {1})
2624, 25eqtr2i 2760 . . . . . . . . . . . . . 14 (β„• ∩ {1}) = {1}
2718, 26uneq12i 4161 . . . . . . . . . . . . 13 ((β„• ∩ {0}) βˆͺ (β„• ∩ {1})) = (βˆ… βˆͺ {1})
2814, 15, 273eqtri 2763 . . . . . . . . . . . 12 (β„• ∩ {0, 1}) = (βˆ… βˆͺ {1})
29 uncom 4153 . . . . . . . . . . . 12 (βˆ… βˆͺ {1}) = ({1} βˆͺ βˆ…)
30 un0 4390 . . . . . . . . . . . 12 ({1} βˆͺ βˆ…) = {1}
3128, 29, 303eqtri 2763 . . . . . . . . . . 11 (β„• ∩ {0, 1}) = {1}
3231imaeq2i 6057 . . . . . . . . . 10 (◑𝑓 β€œ (β„• ∩ {0, 1})) = (◑𝑓 β€œ {1})
3312, 32eqtrdi 2787 . . . . . . . . 9 ((Fun 𝑓 ∧ ran 𝑓 βŠ† {0, 1}) β†’ (◑𝑓 β€œ β„•) = (◑𝑓 β€œ {1}))
349, 11, 33syl2anc 583 . . . . . . . 8 (𝑓 ∈ ({0, 1} ↑m β„•) β†’ (◑𝑓 β€œ β„•) = (◑𝑓 β€œ {1}))
3534eleq1d 2817 . . . . . . 7 (𝑓 ∈ ({0, 1} ↑m β„•) β†’ ((◑𝑓 β€œ β„•) ∈ Fin ↔ (◑𝑓 β€œ {1}) ∈ Fin))
3635rabbiia 3435 . . . . . 6 {𝑓 ∈ ({0, 1} ↑m β„•) ∣ (◑𝑓 β€œ β„•) ∈ Fin} = {𝑓 ∈ ({0, 1} ↑m β„•) ∣ (◑𝑓 β€œ {1}) ∈ Fin}
378, 36eqtr2i 2760 . . . . 5 {𝑓 ∈ ({0, 1} ↑m β„•) ∣ (◑𝑓 β€œ {1}) ∈ Fin} = (({0, 1} ↑m β„•) ∩ 𝑅)
38 f1oeq3 6823 . . . . 5 ({𝑓 ∈ ({0, 1} ↑m β„•) ∣ (◑𝑓 β€œ {1}) ∈ Fin} = (({0, 1} ↑m β„•) ∩ 𝑅) β†’ (((πŸ­β€˜β„•) β†Ύ Fin):(𝒫 β„• ∩ Fin)–1-1-ontoβ†’{𝑓 ∈ ({0, 1} ↑m β„•) ∣ (◑𝑓 β€œ {1}) ∈ Fin} ↔ ((πŸ­β€˜β„•) β†Ύ Fin):(𝒫 β„• ∩ Fin)–1-1-ontoβ†’(({0, 1} ↑m β„•) ∩ 𝑅)))
3937, 38ax-mp 5 . . . 4 (((πŸ­β€˜β„•) β†Ύ Fin):(𝒫 β„• ∩ Fin)–1-1-ontoβ†’{𝑓 ∈ ({0, 1} ↑m β„•) ∣ (◑𝑓 β€œ {1}) ∈ Fin} ↔ ((πŸ­β€˜β„•) β†Ύ Fin):(𝒫 β„• ∩ Fin)–1-1-ontoβ†’(({0, 1} ↑m β„•) ∩ 𝑅))
403, 39mpbi 229 . . 3 ((πŸ­β€˜β„•) β†Ύ Fin):(𝒫 β„• ∩ Fin)–1-1-ontoβ†’(({0, 1} ↑m β„•) ∩ 𝑅)
41 eulerpart.j . . . . . . 7 𝐽 = {𝑧 ∈ β„• ∣ Β¬ 2 βˆ₯ 𝑧}
42 eulerpart.f . . . . . . 7 𝐹 = (π‘₯ ∈ 𝐽, 𝑦 ∈ β„•0 ↦ ((2↑𝑦) Β· π‘₯))
4341, 42oddpwdc 33652 . . . . . 6 𝐹:(𝐽 Γ— β„•0)–1-1-ontoβ†’β„•
44 f1opwfi 9360 . . . . . 6 (𝐹:(𝐽 Γ— β„•0)–1-1-ontoβ†’β„• β†’ (π‘Ž ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↦ (𝐹 β€œ π‘Ž)):(𝒫 (𝐽 Γ— β„•0) ∩ Fin)–1-1-ontoβ†’(𝒫 β„• ∩ Fin))
4543, 44ax-mp 5 . . . . 5 (π‘Ž ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↦ (𝐹 β€œ π‘Ž)):(𝒫 (𝐽 Γ— β„•0) ∩ Fin)–1-1-ontoβ†’(𝒫 β„• ∩ Fin)
46 eulerpart.p . . . . . . . 8 𝑃 = {𝑓 ∈ (β„•0 ↑m β„•) ∣ ((◑𝑓 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘“β€˜π‘˜) Β· π‘˜) = 𝑁)}
47 eulerpart.o . . . . . . . 8 𝑂 = {𝑔 ∈ 𝑃 ∣ βˆ€π‘› ∈ (◑𝑔 β€œ β„•) Β¬ 2 βˆ₯ 𝑛}
48 eulerpart.d . . . . . . . 8 𝐷 = {𝑔 ∈ 𝑃 ∣ βˆ€π‘› ∈ β„• (π‘”β€˜π‘›) ≀ 1}
49 eulerpart.h . . . . . . . 8 𝐻 = {π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin}
50 eulerpart.m . . . . . . . 8 𝑀 = (π‘Ÿ ∈ 𝐻 ↦ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐽 ∧ 𝑦 ∈ (π‘Ÿβ€˜π‘₯))})
5146, 47, 48, 41, 42, 49, 50eulerpartlem1 33665 . . . . . . 7 𝑀:𝐻–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin)
52 bitsf1o 16391 . . . . . . . . . . . . . 14 (bits β†Ύ β„•0):β„•0–1-1-ontoβ†’(𝒫 β„•0 ∩ Fin)
5352a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ (bits β†Ύ β„•0):β„•0–1-1-ontoβ†’(𝒫 β„•0 ∩ Fin))
5441, 1rabex2 5334 . . . . . . . . . . . . . 14 𝐽 ∈ V
5554a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ 𝐽 ∈ V)
56 nn0ex 12483 . . . . . . . . . . . . . 14 β„•0 ∈ V
5756a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ β„•0 ∈ V)
5856pwex 5378 . . . . . . . . . . . . . . 15 𝒫 β„•0 ∈ V
5958inex1 5317 . . . . . . . . . . . . . 14 (𝒫 β„•0 ∩ Fin) ∈ V
6059a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ (𝒫 β„•0 ∩ Fin) ∈ V)
61 0nn0 12492 . . . . . . . . . . . . . 14 0 ∈ β„•0
6261a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ 0 ∈ β„•0)
63 fvres 6910 . . . . . . . . . . . . . . 15 (0 ∈ β„•0 β†’ ((bits β†Ύ β„•0)β€˜0) = (bitsβ€˜0))
6461, 63ax-mp 5 . . . . . . . . . . . . . 14 ((bits β†Ύ β„•0)β€˜0) = (bitsβ€˜0)
65 0bits 16385 . . . . . . . . . . . . . 14 (bitsβ€˜0) = βˆ…
6664, 65eqtr2i 2760 . . . . . . . . . . . . 13 βˆ… = ((bits β†Ύ β„•0)β€˜0)
67 elmapi 8847 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (β„•0 ↑m 𝐽) β†’ 𝑓:π½βŸΆβ„•0)
68 fcdmnn0supp 12533 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ V ∧ 𝑓:π½βŸΆβ„•0) β†’ (𝑓 supp 0) = (◑𝑓 β€œ β„•))
6954, 67, 68sylancr 586 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (β„•0 ↑m 𝐽) β†’ (𝑓 supp 0) = (◑𝑓 β€œ β„•))
7069eleq1d 2817 . . . . . . . . . . . . . . 15 (𝑓 ∈ (β„•0 ↑m 𝐽) β†’ ((𝑓 supp 0) ∈ Fin ↔ (◑𝑓 β€œ β„•) ∈ Fin))
7170rabbiia 3435 . . . . . . . . . . . . . 14 {𝑓 ∈ (β„•0 ↑m 𝐽) ∣ (𝑓 supp 0) ∈ Fin} = {𝑓 ∈ (β„•0 ↑m 𝐽) ∣ (◑𝑓 β€œ β„•) ∈ Fin}
72 elmapfun 8864 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (β„•0 ↑m 𝐽) β†’ Fun 𝑓)
73 vex 3477 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
74 funisfsupp 9371 . . . . . . . . . . . . . . . . 17 ((Fun 𝑓 ∧ 𝑓 ∈ V ∧ 0 ∈ β„•0) β†’ (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7573, 61, 74mp3an23 1452 . . . . . . . . . . . . . . . 16 (Fun 𝑓 β†’ (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7672, 75syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ (β„•0 ↑m 𝐽) β†’ (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7776rabbiia 3435 . . . . . . . . . . . . . 14 {𝑓 ∈ (β„•0 ↑m 𝐽) ∣ 𝑓 finSupp 0} = {𝑓 ∈ (β„•0 ↑m 𝐽) ∣ (𝑓 supp 0) ∈ Fin}
78 incom 4201 . . . . . . . . . . . . . . 15 ({𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin} ∩ (β„•0 ↑m 𝐽)) = ((β„•0 ↑m 𝐽) ∩ {𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin})
79 dfrab2 4310 . . . . . . . . . . . . . . 15 {𝑓 ∈ (β„•0 ↑m 𝐽) ∣ (◑𝑓 β€œ β„•) ∈ Fin} = ({𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin} ∩ (β„•0 ↑m 𝐽))
805ineq2i 4209 . . . . . . . . . . . . . . 15 ((β„•0 ↑m 𝐽) ∩ 𝑅) = ((β„•0 ↑m 𝐽) ∩ {𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin})
8178, 79, 803eqtr4ri 2770 . . . . . . . . . . . . . 14 ((β„•0 ↑m 𝐽) ∩ 𝑅) = {𝑓 ∈ (β„•0 ↑m 𝐽) ∣ (◑𝑓 β€œ β„•) ∈ Fin}
8271, 77, 813eqtr4ri 2770 . . . . . . . . . . . . 13 ((β„•0 ↑m 𝐽) ∩ 𝑅) = {𝑓 ∈ (β„•0 ↑m 𝐽) ∣ 𝑓 finSupp 0}
83 elmapfun 8864 . . . . . . . . . . . . . . 15 (π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) β†’ Fun π‘Ÿ)
84 vex 3477 . . . . . . . . . . . . . . . . 17 π‘Ÿ ∈ V
85 0ex 5307 . . . . . . . . . . . . . . . . 17 βˆ… ∈ V
86 funisfsupp 9371 . . . . . . . . . . . . . . . . 17 ((Fun π‘Ÿ ∧ π‘Ÿ ∈ V ∧ βˆ… ∈ V) β†’ (π‘Ÿ finSupp βˆ… ↔ (π‘Ÿ supp βˆ…) ∈ Fin))
8784, 85, 86mp3an23 1452 . . . . . . . . . . . . . . . 16 (Fun π‘Ÿ β†’ (π‘Ÿ finSupp βˆ… ↔ (π‘Ÿ supp βˆ…) ∈ Fin))
8887bicomd 222 . . . . . . . . . . . . . . 15 (Fun π‘Ÿ β†’ ((π‘Ÿ supp βˆ…) ∈ Fin ↔ π‘Ÿ finSupp βˆ…))
8983, 88syl 17 . . . . . . . . . . . . . 14 (π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) β†’ ((π‘Ÿ supp βˆ…) ∈ Fin ↔ π‘Ÿ finSupp βˆ…))
9089rabbiia 3435 . . . . . . . . . . . . 13 {π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin} = {π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ π‘Ÿ finSupp βˆ…}
9153, 55, 57, 60, 62, 66, 82, 90fcobijfs 32216 . . . . . . . . . . . 12 (⊀ β†’ (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits β†Ύ β„•0) ∘ 𝑓)):((β„•0 ↑m 𝐽) ∩ 𝑅)–1-1-ontoβ†’{π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin})
92 elinel1 4195 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) β†’ 𝑓 ∈ (β„•0 ↑m 𝐽))
93 frn 6724 . . . . . . . . . . . . . . . . 17 (𝑓:π½βŸΆβ„•0 β†’ ran 𝑓 βŠ† β„•0)
94 cores 6248 . . . . . . . . . . . . . . . . 17 (ran 𝑓 βŠ† β„•0 β†’ ((bits β†Ύ β„•0) ∘ 𝑓) = (bits ∘ 𝑓))
9567, 93, 943syl 18 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (β„•0 ↑m 𝐽) β†’ ((bits β†Ύ β„•0) ∘ 𝑓) = (bits ∘ 𝑓))
9692, 95syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) β†’ ((bits β†Ύ β„•0) ∘ 𝑓) = (bits ∘ 𝑓))
9796mpteq2ia 5251 . . . . . . . . . . . . . 14 (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits β†Ύ β„•0) ∘ 𝑓)) = (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓))
9897eqcomi 2740 . . . . . . . . . . . . 13 (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits β†Ύ β„•0) ∘ 𝑓))
99 f1oeq1 6821 . . . . . . . . . . . . 13 ((𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits β†Ύ β„•0) ∘ 𝑓)) β†’ ((𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((β„•0 ↑m 𝐽) ∩ 𝑅)–1-1-ontoβ†’{π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin} ↔ (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits β†Ύ β„•0) ∘ 𝑓)):((β„•0 ↑m 𝐽) ∩ 𝑅)–1-1-ontoβ†’{π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin}))
10098, 99mp1i 13 . . . . . . . . . . . 12 (⊀ β†’ ((𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((β„•0 ↑m 𝐽) ∩ 𝑅)–1-1-ontoβ†’{π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin} ↔ (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits β†Ύ β„•0) ∘ 𝑓)):((β„•0 ↑m 𝐽) ∩ 𝑅)–1-1-ontoβ†’{π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin}))
10191, 100mpbird 257 . . . . . . . . . . 11 (⊀ β†’ (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((β„•0 ↑m 𝐽) ∩ 𝑅)–1-1-ontoβ†’{π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin})
102101mptru 1547 . . . . . . . . . 10 (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((β„•0 ↑m 𝐽) ∩ 𝑅)–1-1-ontoβ†’{π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin}
103 ssrab2 4077 . . . . . . . . . . . . . . . 16 {𝑧 ∈ β„• ∣ Β¬ 2 βˆ₯ 𝑧} βŠ† β„•
10441, 103eqsstri 4016 . . . . . . . . . . . . . . 15 𝐽 βŠ† β„•
1051, 56, 1043pm3.2i 1338 . . . . . . . . . . . . . 14 (β„• ∈ V ∧ β„•0 ∈ V ∧ 𝐽 βŠ† β„•)
106 eulerpart.t . . . . . . . . . . . . . . . 16 𝑇 = {𝑓 ∈ (β„•0 ↑m β„•) ∣ (◑𝑓 β€œ β„•) βŠ† 𝐽}
107 cnveq 5873 . . . . . . . . . . . . . . . . . . 19 (𝑓 = π‘œ β†’ ◑𝑓 = β—‘π‘œ)
108 dfn2 12490 . . . . . . . . . . . . . . . . . . . 20 β„• = (β„•0 βˆ– {0})
109108a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑓 = π‘œ β†’ β„• = (β„•0 βˆ– {0}))
110107, 109imaeq12d 6060 . . . . . . . . . . . . . . . . . 18 (𝑓 = π‘œ β†’ (◑𝑓 β€œ β„•) = (β—‘π‘œ β€œ (β„•0 βˆ– {0})))
111110sseq1d 4013 . . . . . . . . . . . . . . . . 17 (𝑓 = π‘œ β†’ ((◑𝑓 β€œ β„•) βŠ† 𝐽 ↔ (β—‘π‘œ β€œ (β„•0 βˆ– {0})) βŠ† 𝐽))
112111cbvrabv 3441 . . . . . . . . . . . . . . . 16 {𝑓 ∈ (β„•0 ↑m β„•) ∣ (◑𝑓 β€œ β„•) βŠ† 𝐽} = {π‘œ ∈ (β„•0 ↑m β„•) ∣ (β—‘π‘œ β€œ (β„•0 βˆ– {0})) βŠ† 𝐽}
113106, 112eqtri 2759 . . . . . . . . . . . . . . 15 𝑇 = {π‘œ ∈ (β„•0 ↑m β„•) ∣ (β—‘π‘œ β€œ (β„•0 βˆ– {0})) βŠ† 𝐽}
114 eqid 2731 . . . . . . . . . . . . . . 15 (π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) = (π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))
115113, 114resf1o 32223 . . . . . . . . . . . . . 14 (((β„• ∈ V ∧ β„•0 ∈ V ∧ 𝐽 βŠ† β„•) ∧ 0 ∈ β„•0) β†’ (π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)):𝑇–1-1-ontoβ†’(β„•0 ↑m 𝐽))
116105, 61, 115mp2an 689 . . . . . . . . . . . . 13 (π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)):𝑇–1-1-ontoβ†’(β„•0 ↑m 𝐽)
117 f1of1 6832 . . . . . . . . . . . . 13 ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)):𝑇–1-1-ontoβ†’(β„•0 ↑m 𝐽) β†’ (π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)):𝑇–1-1β†’(β„•0 ↑m 𝐽))
118116, 117ax-mp 5 . . . . . . . . . . . 12 (π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)):𝑇–1-1β†’(β„•0 ↑m 𝐽)
119 inss1 4228 . . . . . . . . . . . 12 (𝑇 ∩ 𝑅) βŠ† 𝑇
120 f1ores 6847 . . . . . . . . . . . 12 (((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)):𝑇–1-1β†’(β„•0 ↑m 𝐽) ∧ (𝑇 ∩ 𝑅) βŠ† 𝑇) β†’ ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β†Ύ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β€œ (𝑇 ∩ 𝑅)))
121118, 119, 120mp2an 689 . . . . . . . . . . 11 ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β†Ύ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β€œ (𝑇 ∩ 𝑅))
122 vex 3477 . . . . . . . . . . . . . . . . . 18 π‘œ ∈ V
123122resex 6029 . . . . . . . . . . . . . . . . 17 (π‘œ β†Ύ 𝐽) ∈ V
124123, 114fnmpti 6693 . . . . . . . . . . . . . . . 16 (π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) Fn 𝑇
125 fvelimab 6964 . . . . . . . . . . . . . . . 16 (((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) Fn 𝑇 ∧ (𝑇 ∩ 𝑅) βŠ† 𝑇) β†’ (𝑓 ∈ ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β€œ (𝑇 ∩ 𝑅)) ↔ βˆƒπ‘š ∈ (𝑇 ∩ 𝑅)((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))β€˜π‘š) = 𝑓))
126124, 119, 125mp2an 689 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β€œ (𝑇 ∩ 𝑅)) ↔ βˆƒπ‘š ∈ (𝑇 ∩ 𝑅)((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))β€˜π‘š) = 𝑓)
127 eqid 2731 . . . . . . . . . . . . . . . . 17 (π‘š ∈ (𝑇 ∩ 𝑅) ↦ (π‘š β†Ύ 𝐽)) = (π‘š ∈ (𝑇 ∩ 𝑅) ↦ (π‘š β†Ύ 𝐽))
128 vex 3477 . . . . . . . . . . . . . . . . . 18 π‘š ∈ V
129128resex 6029 . . . . . . . . . . . . . . . . 17 (π‘š β†Ύ 𝐽) ∈ V
130127, 129elrnmpti 5959 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ran (π‘š ∈ (𝑇 ∩ 𝑅) ↦ (π‘š β†Ύ 𝐽)) ↔ βˆƒπ‘š ∈ (𝑇 ∩ 𝑅)𝑓 = (π‘š β†Ύ 𝐽))
13146, 47, 48, 41, 42, 49, 50, 5, 106eulerpartlemt 33669 . . . . . . . . . . . . . . . . 17 ((β„•0 ↑m 𝐽) ∩ 𝑅) = ran (π‘š ∈ (𝑇 ∩ 𝑅) ↦ (π‘š β†Ύ 𝐽))
132131eleq2i 2824 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↔ 𝑓 ∈ ran (π‘š ∈ (𝑇 ∩ 𝑅) ↦ (π‘š β†Ύ 𝐽)))
133 elinel1 4195 . . . . . . . . . . . . . . . . . . 19 (π‘š ∈ (𝑇 ∩ 𝑅) β†’ π‘š ∈ 𝑇)
134114fvtresfn 7000 . . . . . . . . . . . . . . . . . . . 20 (π‘š ∈ 𝑇 β†’ ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))β€˜π‘š) = (π‘š β†Ύ 𝐽))
135134eqeq1d 2733 . . . . . . . . . . . . . . . . . . 19 (π‘š ∈ 𝑇 β†’ (((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))β€˜π‘š) = 𝑓 ↔ (π‘š β†Ύ 𝐽) = 𝑓))
136133, 135syl 17 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ (𝑇 ∩ 𝑅) β†’ (((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))β€˜π‘š) = 𝑓 ↔ (π‘š β†Ύ 𝐽) = 𝑓))
137 eqcom 2738 . . . . . . . . . . . . . . . . . 18 ((π‘š β†Ύ 𝐽) = 𝑓 ↔ 𝑓 = (π‘š β†Ύ 𝐽))
138136, 137bitrdi 287 . . . . . . . . . . . . . . . . 17 (π‘š ∈ (𝑇 ∩ 𝑅) β†’ (((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))β€˜π‘š) = 𝑓 ↔ 𝑓 = (π‘š β†Ύ 𝐽)))
139138rexbiia 3091 . . . . . . . . . . . . . . . 16 (βˆƒπ‘š ∈ (𝑇 ∩ 𝑅)((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))β€˜π‘š) = 𝑓 ↔ βˆƒπ‘š ∈ (𝑇 ∩ 𝑅)𝑓 = (π‘š β†Ύ 𝐽))
140130, 132, 1393bitr4ri 304 . . . . . . . . . . . . . . 15 (βˆƒπ‘š ∈ (𝑇 ∩ 𝑅)((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))β€˜π‘š) = 𝑓 ↔ 𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅))
141126, 140bitri 275 . . . . . . . . . . . . . 14 (𝑓 ∈ ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β€œ (𝑇 ∩ 𝑅)) ↔ 𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅))
142141eqriv 2728 . . . . . . . . . . . . 13 ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β€œ (𝑇 ∩ 𝑅)) = ((β„•0 ↑m 𝐽) ∩ 𝑅)
143 f1oeq3 6823 . . . . . . . . . . . . 13 (((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β€œ (𝑇 ∩ 𝑅)) = ((β„•0 ↑m 𝐽) ∩ 𝑅) β†’ (((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β†Ύ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β€œ (𝑇 ∩ 𝑅)) ↔ ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β†Ύ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((β„•0 ↑m 𝐽) ∩ 𝑅)))
144142, 143ax-mp 5 . . . . . . . . . . . 12 (((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β†Ύ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β€œ (𝑇 ∩ 𝑅)) ↔ ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β†Ύ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((β„•0 ↑m 𝐽) ∩ 𝑅))
145 resmpt 6037 . . . . . . . . . . . . 13 ((𝑇 ∩ 𝑅) βŠ† 𝑇 β†’ ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β†Ύ (𝑇 ∩ 𝑅)) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)))
146 f1oeq1 6821 . . . . . . . . . . . . 13 (((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β†Ύ (𝑇 ∩ 𝑅)) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)) β†’ (((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β†Ύ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((β„•0 ↑m 𝐽) ∩ 𝑅) ↔ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((β„•0 ↑m 𝐽) ∩ 𝑅)))
147119, 145, 146mp2b 10 . . . . . . . . . . . 12 (((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β†Ύ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((β„•0 ↑m 𝐽) ∩ 𝑅) ↔ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((β„•0 ↑m 𝐽) ∩ 𝑅))
148144, 147bitri 275 . . . . . . . . . . 11 (((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β†Ύ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β€œ (𝑇 ∩ 𝑅)) ↔ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((β„•0 ↑m 𝐽) ∩ 𝑅))
149121, 148mpbi 229 . . . . . . . . . 10 (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((β„•0 ↑m 𝐽) ∩ 𝑅)
150 f1oco 6856 . . . . . . . . . 10 (((𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((β„•0 ↑m 𝐽) ∩ 𝑅)–1-1-ontoβ†’{π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin} ∧ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((β„•0 ↑m 𝐽) ∩ 𝑅)) β†’ ((𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’{π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin})
151102, 149, 150mp2an 689 . . . . . . . . 9 ((𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’{π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin}
152 f1of 6833 . . . . . . . . . . . . . 14 ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((β„•0 ↑m 𝐽) ∩ 𝑅) β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)):(𝑇 ∩ 𝑅)⟢((β„•0 ↑m 𝐽) ∩ 𝑅))
153 eqid 2731 . . . . . . . . . . . . . . . 16 (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽))
154153fmpt 7111 . . . . . . . . . . . . . . 15 (βˆ€π‘œ ∈ (𝑇 ∩ 𝑅)(π‘œ β†Ύ 𝐽) ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↔ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)):(𝑇 ∩ 𝑅)⟢((β„•0 ↑m 𝐽) ∩ 𝑅))
155154biimpri 227 . . . . . . . . . . . . . 14 ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)):(𝑇 ∩ 𝑅)⟢((β„•0 ↑m 𝐽) ∩ 𝑅) β†’ βˆ€π‘œ ∈ (𝑇 ∩ 𝑅)(π‘œ β†Ύ 𝐽) ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅))
156149, 152, 155mp2b 10 . . . . . . . . . . . . 13 βˆ€π‘œ ∈ (𝑇 ∩ 𝑅)(π‘œ β†Ύ 𝐽) ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅)
157156a1i 11 . . . . . . . . . . . 12 (⊀ β†’ βˆ€π‘œ ∈ (𝑇 ∩ 𝑅)(π‘œ β†Ύ 𝐽) ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅))
158 eqidd 2732 . . . . . . . . . . . 12 (⊀ β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)))
159 eqidd 2732 . . . . . . . . . . . 12 (⊀ β†’ (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)))
160 coeq2 5858 . . . . . . . . . . . 12 (𝑓 = (π‘œ β†Ύ 𝐽) β†’ (bits ∘ 𝑓) = (bits ∘ (π‘œ β†Ύ 𝐽)))
161157, 158, 159, 160fmptcof 7130 . . . . . . . . . . 11 (⊀ β†’ ((𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))))
162161eqcomd 2737 . . . . . . . . . 10 (⊀ β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))) = ((𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽))))
163 eqidd 2732 . . . . . . . . . 10 (⊀ β†’ (𝑇 ∩ 𝑅) = (𝑇 ∩ 𝑅))
16449a1i 11 . . . . . . . . . 10 (⊀ β†’ 𝐻 = {π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin})
165162, 163, 164f1oeq123d 6827 . . . . . . . . 9 (⊀ β†’ ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻 ↔ ((𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’{π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin}))
166151, 165mpbiri 258 . . . . . . . 8 (⊀ β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻)
167166mptru 1547 . . . . . . 7 (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻
168 f1oco 6856 . . . . . . 7 ((𝑀:𝐻–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin) ∧ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻) β†’ (𝑀 ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin))
16951, 167, 168mp2an 689 . . . . . 6 (𝑀 ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin)
170 eqidd 2732 . . . . . . . . . . 11 (⊀ β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))))
171 bitsf 16373 . . . . . . . . . . . . . 14 bits:β„€βŸΆπ’« β„•0
172 zex 12572 . . . . . . . . . . . . . 14 β„€ ∈ V
173 fex 7230 . . . . . . . . . . . . . 14 ((bits:β„€βŸΆπ’« β„•0 ∧ β„€ ∈ V) β†’ bits ∈ V)
174171, 172, 173mp2an 689 . . . . . . . . . . . . 13 bits ∈ V
175174, 123coex 7925 . . . . . . . . . . . 12 (bits ∘ (π‘œ β†Ύ 𝐽)) ∈ V
176175a1i 11 . . . . . . . . . . 11 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ (bits ∘ (π‘œ β†Ύ 𝐽)) ∈ V)
177170, 176fvmpt2d 7011 . . . . . . . . . 10 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽)))β€˜π‘œ) = (bits ∘ (π‘œ β†Ύ 𝐽)))
178 f1of 6833 . . . . . . . . . . . 12 ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻 β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))):(𝑇 ∩ 𝑅)⟢𝐻)
179166, 178syl 17 . . . . . . . . . . 11 (⊀ β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))):(𝑇 ∩ 𝑅)⟢𝐻)
180179ffvelcdmda 7086 . . . . . . . . . 10 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽)))β€˜π‘œ) ∈ 𝐻)
181177, 180eqeltrrd 2833 . . . . . . . . 9 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ (bits ∘ (π‘œ β†Ύ 𝐽)) ∈ 𝐻)
182 f1ofn 6834 . . . . . . . . . . . 12 (𝑀:𝐻–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin) β†’ 𝑀 Fn 𝐻)
18351, 182ax-mp 5 . . . . . . . . . . 11 𝑀 Fn 𝐻
184 dffn5 6950 . . . . . . . . . . 11 (𝑀 Fn 𝐻 ↔ 𝑀 = (π‘Ÿ ∈ 𝐻 ↦ (π‘€β€˜π‘Ÿ)))
185183, 184mpbi 229 . . . . . . . . . 10 𝑀 = (π‘Ÿ ∈ 𝐻 ↦ (π‘€β€˜π‘Ÿ))
186185a1i 11 . . . . . . . . 9 (⊀ β†’ 𝑀 = (π‘Ÿ ∈ 𝐻 ↦ (π‘€β€˜π‘Ÿ)))
187 fveq2 6891 . . . . . . . . 9 (π‘Ÿ = (bits ∘ (π‘œ β†Ύ 𝐽)) β†’ (π‘€β€˜π‘Ÿ) = (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))
188181, 170, 186, 187fmptco 7129 . . . . . . . 8 (⊀ β†’ (𝑀 ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽)))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))
189188mptru 1547 . . . . . . 7 (𝑀 ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽)))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))
190 f1oeq1 6821 . . . . . . 7 ((𝑀 ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽)))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))) β†’ ((𝑀 ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↔ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin)))
191189, 190ax-mp 5 . . . . . 6 ((𝑀 ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↔ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin))
192169, 191mpbi 229 . . . . 5 (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin)
193 f1oco 6856 . . . . 5 (((π‘Ž ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↦ (𝐹 β€œ π‘Ž)):(𝒫 (𝐽 Γ— β„•0) ∩ Fin)–1-1-ontoβ†’(𝒫 β„• ∩ Fin) ∧ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin)) β†’ ((π‘Ž ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↦ (𝐹 β€œ π‘Ž)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 β„• ∩ Fin))
19445, 192, 193mp2an 689 . . . 4 ((π‘Ž ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↦ (𝐹 β€œ π‘Ž)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 β„• ∩ Fin)
195 simpr 484 . . . . . . . . 9 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ π‘œ ∈ (𝑇 ∩ 𝑅))
196 fvex 6904 . . . . . . . . 9 (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))) ∈ V
197 eqid 2731 . . . . . . . . . 10 (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))
198197fvmpt2 7009 . . . . . . . . 9 ((π‘œ ∈ (𝑇 ∩ 𝑅) ∧ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))) ∈ V) β†’ ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))β€˜π‘œ) = (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))
199195, 196, 198sylancl 585 . . . . . . . 8 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))β€˜π‘œ) = (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))
200 f1of 6833 . . . . . . . . . 10 ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin) β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))):(𝑇 ∩ 𝑅)⟢(𝒫 (𝐽 Γ— β„•0) ∩ Fin))
201192, 200mp1i 13 . . . . . . . . 9 (⊀ β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))):(𝑇 ∩ 𝑅)⟢(𝒫 (𝐽 Γ— β„•0) ∩ Fin))
202201ffvelcdmda 7086 . . . . . . . 8 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))β€˜π‘œ) ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin))
203199, 202eqeltrrd 2833 . . . . . . 7 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))) ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin))
204 eqidd 2732 . . . . . . 7 (⊀ β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))
205 eqidd 2732 . . . . . . 7 (⊀ β†’ (π‘Ž ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↦ (𝐹 β€œ π‘Ž)) = (π‘Ž ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↦ (𝐹 β€œ π‘Ž)))
206 imaeq2 6055 . . . . . . 7 (π‘Ž = (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))) β†’ (𝐹 β€œ π‘Ž) = (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))
207203, 204, 205, 206fmptco 7129 . . . . . 6 (⊀ β†’ ((π‘Ž ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↦ (𝐹 β€œ π‘Ž)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))))
208207mptru 1547 . . . . 5 ((π‘Ž ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↦ (𝐹 β€œ π‘Ž)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))
209 f1oeq1 6821 . . . . 5 (((π‘Ž ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↦ (𝐹 β€œ π‘Ž)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))) β†’ (((π‘Ž ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↦ (𝐹 β€œ π‘Ž)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 β„• ∩ Fin) ↔ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 β„• ∩ Fin)))
210208, 209ax-mp 5 . . . 4 (((π‘Ž ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↦ (𝐹 β€œ π‘Ž)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 β„• ∩ Fin) ↔ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 β„• ∩ Fin))
211194, 210mpbi 229 . . 3 (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 β„• ∩ Fin)
212 f1oco 6856 . . 3 ((((πŸ­β€˜β„•) β†Ύ Fin):(𝒫 β„• ∩ Fin)–1-1-ontoβ†’(({0, 1} ↑m β„•) ∩ 𝑅) ∧ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 β„• ∩ Fin)) β†’ (((πŸ­β€˜β„•) β†Ύ Fin) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(({0, 1} ↑m β„•) ∩ 𝑅))
21340, 211, 212mp2an 689 . 2 (((πŸ­β€˜β„•) β†Ύ Fin) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(({0, 1} ↑m β„•) ∩ 𝑅)
214 eulerpart.g . . . 4 𝐺 = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ ((πŸ­β€˜β„•)β€˜(𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))))
21542mpoexg 8067 . . . . . . . . . 10 ((𝐽 ∈ V ∧ β„•0 ∈ V) β†’ 𝐹 ∈ V)
21654, 56, 215mp2an 689 . . . . . . . . 9 𝐹 ∈ V
217 imaexg 7910 . . . . . . . . 9 (𝐹 ∈ V β†’ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))) ∈ V)
218216, 217ax-mp 5 . . . . . . . 8 (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))) ∈ V
219 eqid 2731 . . . . . . . . 9 (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))
220219fvmpt2 7009 . . . . . . . 8 ((π‘œ ∈ (𝑇 ∩ 𝑅) ∧ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))) ∈ V) β†’ ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))β€˜π‘œ) = (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))
221195, 218, 220sylancl 585 . . . . . . 7 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))β€˜π‘œ) = (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))
222 f1of 6833 . . . . . . . . 9 ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 β„• ∩ Fin) β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))):(𝑇 ∩ 𝑅)⟢(𝒫 β„• ∩ Fin))
223211, 222mp1i 13 . . . . . . . 8 (⊀ β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))):(𝑇 ∩ 𝑅)⟢(𝒫 β„• ∩ Fin))
224223ffvelcdmda 7086 . . . . . . 7 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))β€˜π‘œ) ∈ (𝒫 β„• ∩ Fin))
225221, 224eqeltrrd 2833 . . . . . 6 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))) ∈ (𝒫 β„• ∩ Fin))
226 eqidd 2732 . . . . . 6 (⊀ β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))))
227 indf1o 33321 . . . . . . . . . . 11 (β„• ∈ V β†’ (πŸ­β€˜β„•):𝒫 ℕ–1-1-ontoβ†’({0, 1} ↑m β„•))
228 f1ofn 6834 . . . . . . . . . . 11 ((πŸ­β€˜β„•):𝒫 ℕ–1-1-ontoβ†’({0, 1} ↑m β„•) β†’ (πŸ­β€˜β„•) Fn 𝒫 β„•)
2291, 227, 228mp2b 10 . . . . . . . . . 10 (πŸ­β€˜β„•) Fn 𝒫 β„•
230 dffn5 6950 . . . . . . . . . 10 ((πŸ­β€˜β„•) Fn 𝒫 β„• ↔ (πŸ­β€˜β„•) = (𝑏 ∈ 𝒫 β„• ↦ ((πŸ­β€˜β„•)β€˜π‘)))
231229, 230mpbi 229 . . . . . . . . 9 (πŸ­β€˜β„•) = (𝑏 ∈ 𝒫 β„• ↦ ((πŸ­β€˜β„•)β€˜π‘))
232231reseq1i 5977 . . . . . . . 8 ((πŸ­β€˜β„•) β†Ύ Fin) = ((𝑏 ∈ 𝒫 β„• ↦ ((πŸ­β€˜β„•)β€˜π‘)) β†Ύ Fin)
233 resmpt3 6038 . . . . . . . 8 ((𝑏 ∈ 𝒫 β„• ↦ ((πŸ­β€˜β„•)β€˜π‘)) β†Ύ Fin) = (𝑏 ∈ (𝒫 β„• ∩ Fin) ↦ ((πŸ­β€˜β„•)β€˜π‘))
234232, 233eqtri 2759 . . . . . . 7 ((πŸ­β€˜β„•) β†Ύ Fin) = (𝑏 ∈ (𝒫 β„• ∩ Fin) ↦ ((πŸ­β€˜β„•)β€˜π‘))
235234a1i 11 . . . . . 6 (⊀ β†’ ((πŸ­β€˜β„•) β†Ύ Fin) = (𝑏 ∈ (𝒫 β„• ∩ Fin) ↦ ((πŸ­β€˜β„•)β€˜π‘)))
236 fveq2 6891 . . . . . 6 (𝑏 = (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))) β†’ ((πŸ­β€˜β„•)β€˜π‘) = ((πŸ­β€˜β„•)β€˜(𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))))
237225, 226, 235, 236fmptco 7129 . . . . 5 (⊀ β†’ (((πŸ­β€˜β„•) β†Ύ Fin) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ ((πŸ­β€˜β„•)β€˜(𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))))
238237mptru 1547 . . . 4 (((πŸ­β€˜β„•) β†Ύ Fin) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ ((πŸ­β€˜β„•)β€˜(𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))))
239214, 238eqtr4i 2762 . . 3 𝐺 = (((πŸ­β€˜β„•) β†Ύ Fin) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))))
240 f1oeq1 6821 . . 3 (𝐺 = (((πŸ­β€˜β„•) β†Ύ Fin) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))) β†’ (𝐺:(𝑇 ∩ 𝑅)–1-1-ontoβ†’(({0, 1} ↑m β„•) ∩ 𝑅) ↔ (((πŸ­β€˜β„•) β†Ύ Fin) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(({0, 1} ↑m β„•) ∩ 𝑅)))
241239, 240ax-mp 5 . 2 (𝐺:(𝑇 ∩ 𝑅)–1-1-ontoβ†’(({0, 1} ↑m β„•) ∩ 𝑅) ↔ (((πŸ­β€˜β„•) β†Ύ Fin) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(({0, 1} ↑m β„•) ∩ 𝑅))
242213, 241mpbir 230 1 𝐺:(𝑇 ∩ 𝑅)–1-1-ontoβ†’(({0, 1} ↑m β„•) ∩ 𝑅)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   ↔ wb 205   ∧ wa 395   ∧ w3a 1086   = wceq 1540  βŠ€wtru 1541   ∈ wcel 2105  {cab 2708  βˆ€wral 3060  βˆƒwrex 3069  {crab 3431  Vcvv 3473   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  π’« cpw 4602  {csn 4628  {cpr 4630   class class class wbr 5148  {copab 5210   ↦ cmpt 5231   Γ— cxp 5674  β—‘ccnv 5675  ran crn 5677   β†Ύ cres 5678   β€œ cima 5679   ∘ ccom 5680  Fun wfun 6537   Fn wfn 6538  βŸΆwf 6539  β€“1-1β†’wf1 6540  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543  (class class class)co 7412   ∈ cmpo 7414   supp csupp 8150   ↑m cmap 8824  Fincfn 8943   finSupp cfsupp 9365  0cc0 11114  1c1 11115   Β· cmul 11119   ≀ cle 11254  β„•cn 12217  2c2 12272  β„•0cn0 12477  β„€cz 12563  β†‘cexp 14032  Ξ£csu 15637   βˆ₯ cdvds 16202  bitscbits 16365  πŸ­cind 33307
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-inf2 9640  ax-ac2 10462  ax-cnex 11170  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190  ax-pre-mulgt0 11191  ax-pre-sup 11192
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-disj 5114  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-1st 7979  df-2nd 7980  df-supp 8151  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-1o 8470  df-2o 8471  df-oadd 8474  df-er 8707  df-map 8826  df-pm 8827  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-fsupp 9366  df-sup 9441  df-inf 9442  df-oi 9509  df-dju 9900  df-card 9938  df-acn 9941  df-ac 10115  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-div 11877  df-nn 12218  df-2 12280  df-3 12281  df-n0 12478  df-xnn0 12550  df-z 12564  df-uz 12828  df-rp 12980  df-fz 13490  df-fzo 13633  df-fl 13762  df-mod 13840  df-seq 13972  df-exp 14033  df-hash 14296  df-cj 15051  df-re 15052  df-im 15053  df-sqrt 15187  df-abs 15188  df-clim 15437  df-sum 15638  df-dvds 16203  df-bits 16368  df-ind 33308
This theorem is referenced by:  eulerpartlemgf  33677  eulerpartlemgs2  33678  eulerpartlemn  33679
  Copyright terms: Public domain W3C validator