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 33371
Description: Lemma for eulerpart 33381: 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 12218 . . . . 5 β„• ∈ V
2 indf1ofs 33024 . . . . 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 4202 . . . . . . 7 (({0, 1} ↑m β„•) ∩ {𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin}) = ({𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin} ∩ ({0, 1} ↑m β„•))
5 eulerpart.r . . . . . . . 8 𝑅 = {𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin}
65ineq2i 4210 . . . . . . 7 (({0, 1} ↑m β„•) ∩ 𝑅) = (({0, 1} ↑m β„•) ∩ {𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin})
7 dfrab2 4311 . . . . . . 7 {𝑓 ∈ ({0, 1} ↑m β„•) ∣ (◑𝑓 β€œ β„•) ∈ Fin} = ({𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin} ∩ ({0, 1} ↑m β„•))
84, 6, 73eqtr4i 2771 . . . . . 6 (({0, 1} ↑m β„•) ∩ 𝑅) = {𝑓 ∈ ({0, 1} ↑m β„•) ∣ (◑𝑓 β€œ β„•) ∈ Fin}
9 elmapfun 8860 . . . . . . . . 9 (𝑓 ∈ ({0, 1} ↑m β„•) β†’ Fun 𝑓)
10 elmapi 8843 . . . . . . . . . 10 (𝑓 ∈ ({0, 1} ↑m β„•) β†’ 𝑓:β„•βŸΆ{0, 1})
1110frnd 6726 . . . . . . . . 9 (𝑓 ∈ ({0, 1} ↑m β„•) β†’ ran 𝑓 βŠ† {0, 1})
12 fimacnvinrn2 7075 . . . . . . . . . 10 ((Fun 𝑓 ∧ ran 𝑓 βŠ† {0, 1}) β†’ (◑𝑓 β€œ β„•) = (◑𝑓 β€œ (β„• ∩ {0, 1})))
13 df-pr 4632 . . . . . . . . . . . . . 14 {0, 1} = ({0} βˆͺ {1})
1413ineq2i 4210 . . . . . . . . . . . . 13 (β„• ∩ {0, 1}) = (β„• ∩ ({0} βˆͺ {1}))
15 indi 4274 . . . . . . . . . . . . 13 (β„• ∩ ({0} βˆͺ {1})) = ((β„• ∩ {0}) βˆͺ (β„• ∩ {1}))
16 0nnn 12248 . . . . . . . . . . . . . . 15 Β¬ 0 ∈ β„•
17 disjsn 4716 . . . . . . . . . . . . . . 15 ((β„• ∩ {0}) = βˆ… ↔ Β¬ 0 ∈ β„•)
1816, 17mpbir 230 . . . . . . . . . . . . . 14 (β„• ∩ {0}) = βˆ…
19 1nn 12223 . . . . . . . . . . . . . . . . 17 1 ∈ β„•
20 1ex 11210 . . . . . . . . . . . . . . . . . 18 1 ∈ V
2120snss 4790 . . . . . . . . . . . . . . . . 17 (1 ∈ β„• ↔ {1} βŠ† β„•)
2219, 21mpbi 229 . . . . . . . . . . . . . . . 16 {1} βŠ† β„•
23 dfss 3967 . . . . . . . . . . . . . . . 16 ({1} βŠ† β„• ↔ {1} = ({1} ∩ β„•))
2422, 23mpbi 229 . . . . . . . . . . . . . . 15 {1} = ({1} ∩ β„•)
25 incom 4202 . . . . . . . . . . . . . . 15 ({1} ∩ β„•) = (β„• ∩ {1})
2624, 25eqtr2i 2762 . . . . . . . . . . . . . 14 (β„• ∩ {1}) = {1}
2718, 26uneq12i 4162 . . . . . . . . . . . . 13 ((β„• ∩ {0}) βˆͺ (β„• ∩ {1})) = (βˆ… βˆͺ {1})
2814, 15, 273eqtri 2765 . . . . . . . . . . . 12 (β„• ∩ {0, 1}) = (βˆ… βˆͺ {1})
29 uncom 4154 . . . . . . . . . . . 12 (βˆ… βˆͺ {1}) = ({1} βˆͺ βˆ…)
30 un0 4391 . . . . . . . . . . . 12 ({1} βˆͺ βˆ…) = {1}
3128, 29, 303eqtri 2765 . . . . . . . . . . 11 (β„• ∩ {0, 1}) = {1}
3231imaeq2i 6058 . . . . . . . . . 10 (◑𝑓 β€œ (β„• ∩ {0, 1})) = (◑𝑓 β€œ {1})
3312, 32eqtrdi 2789 . . . . . . . . 9 ((Fun 𝑓 ∧ ran 𝑓 βŠ† {0, 1}) β†’ (◑𝑓 β€œ β„•) = (◑𝑓 β€œ {1}))
349, 11, 33syl2anc 585 . . . . . . . 8 (𝑓 ∈ ({0, 1} ↑m β„•) β†’ (◑𝑓 β€œ β„•) = (◑𝑓 β€œ {1}))
3534eleq1d 2819 . . . . . . 7 (𝑓 ∈ ({0, 1} ↑m β„•) β†’ ((◑𝑓 β€œ β„•) ∈ Fin ↔ (◑𝑓 β€œ {1}) ∈ Fin))
3635rabbiia 3437 . . . . . 6 {𝑓 ∈ ({0, 1} ↑m β„•) ∣ (◑𝑓 β€œ β„•) ∈ Fin} = {𝑓 ∈ ({0, 1} ↑m β„•) ∣ (◑𝑓 β€œ {1}) ∈ Fin}
378, 36eqtr2i 2762 . . . . 5 {𝑓 ∈ ({0, 1} ↑m β„•) ∣ (◑𝑓 β€œ {1}) ∈ Fin} = (({0, 1} ↑m β„•) ∩ 𝑅)
38 f1oeq3 6824 . . . . 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 33353 . . . . . 6 𝐹:(𝐽 Γ— β„•0)–1-1-ontoβ†’β„•
44 f1opwfi 9356 . . . . . 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 33366 . . . . . . 7 𝑀:𝐻–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin)
52 bitsf1o 16386 . . . . . . . . . . . . . 14 (bits β†Ύ β„•0):β„•0–1-1-ontoβ†’(𝒫 β„•0 ∩ Fin)
5352a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ (bits β†Ύ β„•0):β„•0–1-1-ontoβ†’(𝒫 β„•0 ∩ Fin))
5441, 1rabex2 5335 . . . . . . . . . . . . . 14 𝐽 ∈ V
5554a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ 𝐽 ∈ V)
56 nn0ex 12478 . . . . . . . . . . . . . 14 β„•0 ∈ V
5756a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ β„•0 ∈ V)
5856pwex 5379 . . . . . . . . . . . . . . 15 𝒫 β„•0 ∈ V
5958inex1 5318 . . . . . . . . . . . . . 14 (𝒫 β„•0 ∩ Fin) ∈ V
6059a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ (𝒫 β„•0 ∩ Fin) ∈ V)
61 0nn0 12487 . . . . . . . . . . . . . 14 0 ∈ β„•0
6261a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ 0 ∈ β„•0)
63 fvres 6911 . . . . . . . . . . . . . . 15 (0 ∈ β„•0 β†’ ((bits β†Ύ β„•0)β€˜0) = (bitsβ€˜0))
6461, 63ax-mp 5 . . . . . . . . . . . . . 14 ((bits β†Ύ β„•0)β€˜0) = (bitsβ€˜0)
65 0bits 16380 . . . . . . . . . . . . . 14 (bitsβ€˜0) = βˆ…
6664, 65eqtr2i 2762 . . . . . . . . . . . . 13 βˆ… = ((bits β†Ύ β„•0)β€˜0)
67 elmapi 8843 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (β„•0 ↑m 𝐽) β†’ 𝑓:π½βŸΆβ„•0)
68 fcdmnn0supp 12528 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ V ∧ 𝑓:π½βŸΆβ„•0) β†’ (𝑓 supp 0) = (◑𝑓 β€œ β„•))
6954, 67, 68sylancr 588 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (β„•0 ↑m 𝐽) β†’ (𝑓 supp 0) = (◑𝑓 β€œ β„•))
7069eleq1d 2819 . . . . . . . . . . . . . . 15 (𝑓 ∈ (β„•0 ↑m 𝐽) β†’ ((𝑓 supp 0) ∈ Fin ↔ (◑𝑓 β€œ β„•) ∈ Fin))
7170rabbiia 3437 . . . . . . . . . . . . . 14 {𝑓 ∈ (β„•0 ↑m 𝐽) ∣ (𝑓 supp 0) ∈ Fin} = {𝑓 ∈ (β„•0 ↑m 𝐽) ∣ (◑𝑓 β€œ β„•) ∈ Fin}
72 elmapfun 8860 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (β„•0 ↑m 𝐽) β†’ Fun 𝑓)
73 vex 3479 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
74 funisfsupp 9367 . . . . . . . . . . . . . . . . 17 ((Fun 𝑓 ∧ 𝑓 ∈ V ∧ 0 ∈ β„•0) β†’ (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7573, 61, 74mp3an23 1454 . . . . . . . . . . . . . . . 16 (Fun 𝑓 β†’ (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7672, 75syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ (β„•0 ↑m 𝐽) β†’ (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7776rabbiia 3437 . . . . . . . . . . . . . 14 {𝑓 ∈ (β„•0 ↑m 𝐽) ∣ 𝑓 finSupp 0} = {𝑓 ∈ (β„•0 ↑m 𝐽) ∣ (𝑓 supp 0) ∈ Fin}
78 incom 4202 . . . . . . . . . . . . . . 15 ({𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin} ∩ (β„•0 ↑m 𝐽)) = ((β„•0 ↑m 𝐽) ∩ {𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin})
79 dfrab2 4311 . . . . . . . . . . . . . . 15 {𝑓 ∈ (β„•0 ↑m 𝐽) ∣ (◑𝑓 β€œ β„•) ∈ Fin} = ({𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin} ∩ (β„•0 ↑m 𝐽))
805ineq2i 4210 . . . . . . . . . . . . . . 15 ((β„•0 ↑m 𝐽) ∩ 𝑅) = ((β„•0 ↑m 𝐽) ∩ {𝑓 ∣ (◑𝑓 β€œ β„•) ∈ Fin})
8178, 79, 803eqtr4ri 2772 . . . . . . . . . . . . . 14 ((β„•0 ↑m 𝐽) ∩ 𝑅) = {𝑓 ∈ (β„•0 ↑m 𝐽) ∣ (◑𝑓 β€œ β„•) ∈ Fin}
8271, 77, 813eqtr4ri 2772 . . . . . . . . . . . . 13 ((β„•0 ↑m 𝐽) ∩ 𝑅) = {𝑓 ∈ (β„•0 ↑m 𝐽) ∣ 𝑓 finSupp 0}
83 elmapfun 8860 . . . . . . . . . . . . . . 15 (π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) β†’ Fun π‘Ÿ)
84 vex 3479 . . . . . . . . . . . . . . . . 17 π‘Ÿ ∈ V
85 0ex 5308 . . . . . . . . . . . . . . . . 17 βˆ… ∈ V
86 funisfsupp 9367 . . . . . . . . . . . . . . . . 17 ((Fun π‘Ÿ ∧ π‘Ÿ ∈ V ∧ βˆ… ∈ V) β†’ (π‘Ÿ finSupp βˆ… ↔ (π‘Ÿ supp βˆ…) ∈ Fin))
8784, 85, 86mp3an23 1454 . . . . . . . . . . . . . . . 16 (Fun π‘Ÿ β†’ (π‘Ÿ finSupp βˆ… ↔ (π‘Ÿ supp βˆ…) ∈ Fin))
8887bicomd 222 . . . . . . . . . . . . . . 15 (Fun π‘Ÿ β†’ ((π‘Ÿ supp βˆ…) ∈ Fin ↔ π‘Ÿ finSupp βˆ…))
8983, 88syl 17 . . . . . . . . . . . . . 14 (π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) β†’ ((π‘Ÿ supp βˆ…) ∈ Fin ↔ π‘Ÿ finSupp βˆ…))
9089rabbiia 3437 . . . . . . . . . . . . 13 {π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin} = {π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ π‘Ÿ finSupp βˆ…}
9153, 55, 57, 60, 62, 66, 82, 90fcobijfs 31948 . . . . . . . . . . . 12 (⊀ β†’ (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits β†Ύ β„•0) ∘ 𝑓)):((β„•0 ↑m 𝐽) ∩ 𝑅)–1-1-ontoβ†’{π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin})
92 elinel1 4196 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) β†’ 𝑓 ∈ (β„•0 ↑m 𝐽))
93 frn 6725 . . . . . . . . . . . . . . . . 17 (𝑓:π½βŸΆβ„•0 β†’ ran 𝑓 βŠ† β„•0)
94 cores 6249 . . . . . . . . . . . . . . . . 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 5252 . . . . . . . . . . . . . 14 (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits β†Ύ β„•0) ∘ 𝑓)) = (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓))
9897eqcomi 2742 . . . . . . . . . . . . 13 (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits β†Ύ β„•0) ∘ 𝑓))
99 f1oeq1 6822 . . . . . . . . . . . . 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 1549 . . . . . . . . . 10 (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((β„•0 ↑m 𝐽) ∩ 𝑅)–1-1-ontoβ†’{π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin}
103 ssrab2 4078 . . . . . . . . . . . . . . . 16 {𝑧 ∈ β„• ∣ Β¬ 2 βˆ₯ 𝑧} βŠ† β„•
10441, 103eqsstri 4017 . . . . . . . . . . . . . . 15 𝐽 βŠ† β„•
1051, 56, 1043pm3.2i 1340 . . . . . . . . . . . . . 14 (β„• ∈ V ∧ β„•0 ∈ V ∧ 𝐽 βŠ† β„•)
106 eulerpart.t . . . . . . . . . . . . . . . 16 𝑇 = {𝑓 ∈ (β„•0 ↑m β„•) ∣ (◑𝑓 β€œ β„•) βŠ† 𝐽}
107 cnveq 5874 . . . . . . . . . . . . . . . . . . 19 (𝑓 = π‘œ β†’ ◑𝑓 = β—‘π‘œ)
108 dfn2 12485 . . . . . . . . . . . . . . . . . . . 20 β„• = (β„•0 βˆ– {0})
109108a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑓 = π‘œ β†’ β„• = (β„•0 βˆ– {0}))
110107, 109imaeq12d 6061 . . . . . . . . . . . . . . . . . 18 (𝑓 = π‘œ β†’ (◑𝑓 β€œ β„•) = (β—‘π‘œ β€œ (β„•0 βˆ– {0})))
111110sseq1d 4014 . . . . . . . . . . . . . . . . 17 (𝑓 = π‘œ β†’ ((◑𝑓 β€œ β„•) βŠ† 𝐽 ↔ (β—‘π‘œ β€œ (β„•0 βˆ– {0})) βŠ† 𝐽))
112111cbvrabv 3443 . . . . . . . . . . . . . . . 16 {𝑓 ∈ (β„•0 ↑m β„•) ∣ (◑𝑓 β€œ β„•) βŠ† 𝐽} = {π‘œ ∈ (β„•0 ↑m β„•) ∣ (β—‘π‘œ β€œ (β„•0 βˆ– {0})) βŠ† 𝐽}
113106, 112eqtri 2761 . . . . . . . . . . . . . . 15 𝑇 = {π‘œ ∈ (β„•0 ↑m β„•) ∣ (β—‘π‘œ β€œ (β„•0 βˆ– {0})) βŠ† 𝐽}
114 eqid 2733 . . . . . . . . . . . . . . 15 (π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) = (π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))
115113, 114resf1o 31955 . . . . . . . . . . . . . 14 (((β„• ∈ V ∧ β„•0 ∈ V ∧ 𝐽 βŠ† β„•) ∧ 0 ∈ β„•0) β†’ (π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)):𝑇–1-1-ontoβ†’(β„•0 ↑m 𝐽))
116105, 61, 115mp2an 691 . . . . . . . . . . . . 13 (π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)):𝑇–1-1-ontoβ†’(β„•0 ↑m 𝐽)
117 f1of1 6833 . . . . . . . . . . . . 13 ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)):𝑇–1-1-ontoβ†’(β„•0 ↑m 𝐽) β†’ (π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)):𝑇–1-1β†’(β„•0 ↑m 𝐽))
118116, 117ax-mp 5 . . . . . . . . . . . 12 (π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)):𝑇–1-1β†’(β„•0 ↑m 𝐽)
119 inss1 4229 . . . . . . . . . . . 12 (𝑇 ∩ 𝑅) βŠ† 𝑇
120 f1ores 6848 . . . . . . . . . . . 12 (((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)):𝑇–1-1β†’(β„•0 ↑m 𝐽) ∧ (𝑇 ∩ 𝑅) βŠ† 𝑇) β†’ ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β†Ύ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β€œ (𝑇 ∩ 𝑅)))
121118, 119, 120mp2an 691 . . . . . . . . . . 11 ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β†Ύ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β€œ (𝑇 ∩ 𝑅))
122 vex 3479 . . . . . . . . . . . . . . . . . 18 π‘œ ∈ V
123122resex 6030 . . . . . . . . . . . . . . . . 17 (π‘œ β†Ύ 𝐽) ∈ V
124123, 114fnmpti 6694 . . . . . . . . . . . . . . . 16 (π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) Fn 𝑇
125 fvelimab 6965 . . . . . . . . . . . . . . . 16 (((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) Fn 𝑇 ∧ (𝑇 ∩ 𝑅) βŠ† 𝑇) β†’ (𝑓 ∈ ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β€œ (𝑇 ∩ 𝑅)) ↔ βˆƒπ‘š ∈ (𝑇 ∩ 𝑅)((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))β€˜π‘š) = 𝑓))
126124, 119, 125mp2an 691 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β€œ (𝑇 ∩ 𝑅)) ↔ βˆƒπ‘š ∈ (𝑇 ∩ 𝑅)((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))β€˜π‘š) = 𝑓)
127 eqid 2733 . . . . . . . . . . . . . . . . 17 (π‘š ∈ (𝑇 ∩ 𝑅) ↦ (π‘š β†Ύ 𝐽)) = (π‘š ∈ (𝑇 ∩ 𝑅) ↦ (π‘š β†Ύ 𝐽))
128 vex 3479 . . . . . . . . . . . . . . . . . 18 π‘š ∈ V
129128resex 6030 . . . . . . . . . . . . . . . . 17 (π‘š β†Ύ 𝐽) ∈ V
130127, 129elrnmpti 5960 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ran (π‘š ∈ (𝑇 ∩ 𝑅) ↦ (π‘š β†Ύ 𝐽)) ↔ βˆƒπ‘š ∈ (𝑇 ∩ 𝑅)𝑓 = (π‘š β†Ύ 𝐽))
13146, 47, 48, 41, 42, 49, 50, 5, 106eulerpartlemt 33370 . . . . . . . . . . . . . . . . 17 ((β„•0 ↑m 𝐽) ∩ 𝑅) = ran (π‘š ∈ (𝑇 ∩ 𝑅) ↦ (π‘š β†Ύ 𝐽))
132131eleq2i 2826 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↔ 𝑓 ∈ ran (π‘š ∈ (𝑇 ∩ 𝑅) ↦ (π‘š β†Ύ 𝐽)))
133 elinel1 4196 . . . . . . . . . . . . . . . . . . 19 (π‘š ∈ (𝑇 ∩ 𝑅) β†’ π‘š ∈ 𝑇)
134114fvtresfn 7001 . . . . . . . . . . . . . . . . . . . 20 (π‘š ∈ 𝑇 β†’ ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))β€˜π‘š) = (π‘š β†Ύ 𝐽))
135134eqeq1d 2735 . . . . . . . . . . . . . . . . . . 19 (π‘š ∈ 𝑇 β†’ (((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))β€˜π‘š) = 𝑓 ↔ (π‘š β†Ύ 𝐽) = 𝑓))
136133, 135syl 17 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ (𝑇 ∩ 𝑅) β†’ (((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))β€˜π‘š) = 𝑓 ↔ (π‘š β†Ύ 𝐽) = 𝑓))
137 eqcom 2740 . . . . . . . . . . . . . . . . . 18 ((π‘š β†Ύ 𝐽) = 𝑓 ↔ 𝑓 = (π‘š β†Ύ 𝐽))
138136, 137bitrdi 287 . . . . . . . . . . . . . . . . 17 (π‘š ∈ (𝑇 ∩ 𝑅) β†’ (((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))β€˜π‘š) = 𝑓 ↔ 𝑓 = (π‘š β†Ύ 𝐽)))
139138rexbiia 3093 . . . . . . . . . . . . . . . 16 (βˆƒπ‘š ∈ (𝑇 ∩ 𝑅)((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))β€˜π‘š) = 𝑓 ↔ βˆƒπ‘š ∈ (𝑇 ∩ 𝑅)𝑓 = (π‘š β†Ύ 𝐽))
140130, 132, 1393bitr4ri 304 . . . . . . . . . . . . . . 15 (βˆƒπ‘š ∈ (𝑇 ∩ 𝑅)((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽))β€˜π‘š) = 𝑓 ↔ 𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅))
141126, 140bitri 275 . . . . . . . . . . . . . 14 (𝑓 ∈ ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β€œ (𝑇 ∩ 𝑅)) ↔ 𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅))
142141eqriv 2730 . . . . . . . . . . . . 13 ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β€œ (𝑇 ∩ 𝑅)) = ((β„•0 ↑m 𝐽) ∩ 𝑅)
143 f1oeq3 6824 . . . . . . . . . . . . 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 6038 . . . . . . . . . . . . 13 ((𝑇 ∩ 𝑅) βŠ† 𝑇 β†’ ((π‘œ ∈ 𝑇 ↦ (π‘œ β†Ύ 𝐽)) β†Ύ (𝑇 ∩ 𝑅)) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)))
146 f1oeq1 6822 . . . . . . . . . . . . 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 6857 . . . . . . . . . 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 691 . . . . . . . . 9 ((𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’{π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin}
152 f1of 6834 . . . . . . . . . . . . . 14 ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)):(𝑇 ∩ 𝑅)–1-1-ontoβ†’((β„•0 ↑m 𝐽) ∩ 𝑅) β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)):(𝑇 ∩ 𝑅)⟢((β„•0 ↑m 𝐽) ∩ 𝑅))
153 eqid 2733 . . . . . . . . . . . . . . . 16 (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽))
154153fmpt 7110 . . . . . . . . . . . . . . 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 2734 . . . . . . . . . . . 12 (⊀ β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽)))
159 eqidd 2734 . . . . . . . . . . . 12 (⊀ β†’ (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)))
160 coeq2 5859 . . . . . . . . . . . 12 (𝑓 = (π‘œ β†Ύ 𝐽) β†’ (bits ∘ 𝑓) = (bits ∘ (π‘œ β†Ύ 𝐽)))
161157, 158, 159, 160fmptcof 7128 . . . . . . . . . . 11 (⊀ β†’ ((𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))))
162161eqcomd 2739 . . . . . . . . . 10 (⊀ β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))) = ((𝑓 ∈ ((β„•0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘œ β†Ύ 𝐽))))
163 eqidd 2734 . . . . . . . . . 10 (⊀ β†’ (𝑇 ∩ 𝑅) = (𝑇 ∩ 𝑅))
16449a1i 11 . . . . . . . . . 10 (⊀ β†’ 𝐻 = {π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin})
165162, 163, 164f1oeq123d 6828 . . . . . . . . 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 1549 . . . . . . 7 (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻
168 f1oco 6857 . . . . . . 7 ((𝑀:𝐻–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin) ∧ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻) β†’ (𝑀 ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin))
16951, 167, 168mp2an 691 . . . . . 6 (𝑀 ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin)
170 eqidd 2734 . . . . . . . . . . 11 (⊀ β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))))
171 bitsf 16368 . . . . . . . . . . . . . 14 bits:β„€βŸΆπ’« β„•0
172 zex 12567 . . . . . . . . . . . . . 14 β„€ ∈ V
173 fex 7228 . . . . . . . . . . . . . 14 ((bits:β„€βŸΆπ’« β„•0 ∧ β„€ ∈ V) β†’ bits ∈ V)
174171, 172, 173mp2an 691 . . . . . . . . . . . . 13 bits ∈ V
175174, 123coex 7921 . . . . . . . . . . . 12 (bits ∘ (π‘œ β†Ύ 𝐽)) ∈ V
176175a1i 11 . . . . . . . . . . 11 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ (bits ∘ (π‘œ β†Ύ 𝐽)) ∈ V)
177170, 176fvmpt2d 7012 . . . . . . . . . 10 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽)))β€˜π‘œ) = (bits ∘ (π‘œ β†Ύ 𝐽)))
178 f1of 6834 . . . . . . . . . . . 12 ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻 β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))):(𝑇 ∩ 𝑅)⟢𝐻)
179166, 178syl 17 . . . . . . . . . . 11 (⊀ β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽))):(𝑇 ∩ 𝑅)⟢𝐻)
180179ffvelcdmda 7087 . . . . . . . . . 10 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽)))β€˜π‘œ) ∈ 𝐻)
181177, 180eqeltrrd 2835 . . . . . . . . 9 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ (bits ∘ (π‘œ β†Ύ 𝐽)) ∈ 𝐻)
182 f1ofn 6835 . . . . . . . . . . . 12 (𝑀:𝐻–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin) β†’ 𝑀 Fn 𝐻)
18351, 182ax-mp 5 . . . . . . . . . . 11 𝑀 Fn 𝐻
184 dffn5 6951 . . . . . . . . . . 11 (𝑀 Fn 𝐻 ↔ 𝑀 = (π‘Ÿ ∈ 𝐻 ↦ (π‘€β€˜π‘Ÿ)))
185183, 184mpbi 229 . . . . . . . . . 10 𝑀 = (π‘Ÿ ∈ 𝐻 ↦ (π‘€β€˜π‘Ÿ))
186185a1i 11 . . . . . . . . 9 (⊀ β†’ 𝑀 = (π‘Ÿ ∈ 𝐻 ↦ (π‘€β€˜π‘Ÿ)))
187 fveq2 6892 . . . . . . . . 9 (π‘Ÿ = (bits ∘ (π‘œ β†Ύ 𝐽)) β†’ (π‘€β€˜π‘Ÿ) = (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))
188181, 170, 186, 187fmptco 7127 . . . . . . . 8 (⊀ β†’ (𝑀 ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽)))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))
189188mptru 1549 . . . . . . 7 (𝑀 ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (π‘œ β†Ύ 𝐽)))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))
190 f1oeq1 6822 . . . . . . 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 6857 . . . . 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 691 . . . 4 ((π‘Ž ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↦ (𝐹 β€œ π‘Ž)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 β„• ∩ Fin)
195 simpr 486 . . . . . . . . 9 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ π‘œ ∈ (𝑇 ∩ 𝑅))
196 fvex 6905 . . . . . . . . 9 (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))) ∈ V
197 eqid 2733 . . . . . . . . . 10 (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))
198197fvmpt2 7010 . . . . . . . . 9 ((π‘œ ∈ (𝑇 ∩ 𝑅) ∧ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))) ∈ V) β†’ ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))β€˜π‘œ) = (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))
199195, 196, 198sylancl 587 . . . . . . . 8 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))β€˜π‘œ) = (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))
200 f1of 6834 . . . . . . . . . 10 ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 (𝐽 Γ— β„•0) ∩ Fin) β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))):(𝑇 ∩ 𝑅)⟢(𝒫 (𝐽 Γ— β„•0) ∩ Fin))
201192, 200mp1i 13 . . . . . . . . 9 (⊀ β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))):(𝑇 ∩ 𝑅)⟢(𝒫 (𝐽 Γ— β„•0) ∩ Fin))
202201ffvelcdmda 7087 . . . . . . . 8 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))β€˜π‘œ) ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin))
203199, 202eqeltrrd 2835 . . . . . . 7 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))) ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin))
204 eqidd 2734 . . . . . . 7 (⊀ β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))
205 eqidd 2734 . . . . . . 7 (⊀ β†’ (π‘Ž ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↦ (𝐹 β€œ π‘Ž)) = (π‘Ž ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↦ (𝐹 β€œ π‘Ž)))
206 imaeq2 6056 . . . . . . 7 (π‘Ž = (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))) β†’ (𝐹 β€œ π‘Ž) = (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))
207203, 204, 205, 206fmptco 7127 . . . . . 6 (⊀ β†’ ((π‘Ž ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↦ (𝐹 β€œ π‘Ž)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))))
208207mptru 1549 . . . . 5 ((π‘Ž ∈ (𝒫 (𝐽 Γ— β„•0) ∩ Fin) ↦ (𝐹 β€œ π‘Ž)) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))
209 f1oeq1 6822 . . . . 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 6857 . . 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 691 . 2 (((πŸ­β€˜β„•) β†Ύ Fin) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(({0, 1} ↑m β„•) ∩ 𝑅)
214 eulerpart.g . . . 4 𝐺 = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ ((πŸ­β€˜β„•)β€˜(𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))))
21542mpoexg 8063 . . . . . . . . . 10 ((𝐽 ∈ V ∧ β„•0 ∈ V) β†’ 𝐹 ∈ V)
21654, 56, 215mp2an 691 . . . . . . . . 9 𝐹 ∈ V
217 imaexg 7906 . . . . . . . . 9 (𝐹 ∈ V β†’ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))) ∈ V)
218216, 217ax-mp 5 . . . . . . . 8 (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))) ∈ V
219 eqid 2733 . . . . . . . . 9 (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))
220219fvmpt2 7010 . . . . . . . 8 ((π‘œ ∈ (𝑇 ∩ 𝑅) ∧ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))) ∈ V) β†’ ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))β€˜π‘œ) = (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))
221195, 218, 220sylancl 587 . . . . . . 7 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))β€˜π‘œ) = (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))
222 f1of 6834 . . . . . . . . 9 ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-ontoβ†’(𝒫 β„• ∩ Fin) β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))):(𝑇 ∩ 𝑅)⟢(𝒫 β„• ∩ Fin))
223211, 222mp1i 13 . . . . . . . 8 (⊀ β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))):(𝑇 ∩ 𝑅)⟢(𝒫 β„• ∩ Fin))
224223ffvelcdmda 7087 . . . . . . 7 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ ((π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))β€˜π‘œ) ∈ (𝒫 β„• ∩ Fin))
225221, 224eqeltrrd 2835 . . . . . 6 ((⊀ ∧ π‘œ ∈ (𝑇 ∩ 𝑅)) β†’ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))) ∈ (𝒫 β„• ∩ Fin))
226 eqidd 2734 . . . . . 6 (⊀ β†’ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))))
227 indf1o 33022 . . . . . . . . . . 11 (β„• ∈ V β†’ (πŸ­β€˜β„•):𝒫 ℕ–1-1-ontoβ†’({0, 1} ↑m β„•))
228 f1ofn 6835 . . . . . . . . . . 11 ((πŸ­β€˜β„•):𝒫 ℕ–1-1-ontoβ†’({0, 1} ↑m β„•) β†’ (πŸ­β€˜β„•) Fn 𝒫 β„•)
2291, 227, 228mp2b 10 . . . . . . . . . 10 (πŸ­β€˜β„•) Fn 𝒫 β„•
230 dffn5 6951 . . . . . . . . . 10 ((πŸ­β€˜β„•) Fn 𝒫 β„• ↔ (πŸ­β€˜β„•) = (𝑏 ∈ 𝒫 β„• ↦ ((πŸ­β€˜β„•)β€˜π‘)))
231229, 230mpbi 229 . . . . . . . . 9 (πŸ­β€˜β„•) = (𝑏 ∈ 𝒫 β„• ↦ ((πŸ­β€˜β„•)β€˜π‘))
232231reseq1i 5978 . . . . . . . 8 ((πŸ­β€˜β„•) β†Ύ Fin) = ((𝑏 ∈ 𝒫 β„• ↦ ((πŸ­β€˜β„•)β€˜π‘)) β†Ύ Fin)
233 resmpt3 6039 . . . . . . . 8 ((𝑏 ∈ 𝒫 β„• ↦ ((πŸ­β€˜β„•)β€˜π‘)) β†Ύ Fin) = (𝑏 ∈ (𝒫 β„• ∩ Fin) ↦ ((πŸ­β€˜β„•)β€˜π‘))
234232, 233eqtri 2761 . . . . . . 7 ((πŸ­β€˜β„•) β†Ύ Fin) = (𝑏 ∈ (𝒫 β„• ∩ Fin) ↦ ((πŸ­β€˜β„•)β€˜π‘))
235234a1i 11 . . . . . 6 (⊀ β†’ ((πŸ­β€˜β„•) β†Ύ Fin) = (𝑏 ∈ (𝒫 β„• ∩ Fin) ↦ ((πŸ­β€˜β„•)β€˜π‘)))
236 fveq2 6892 . . . . . 6 (𝑏 = (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))) β†’ ((πŸ­β€˜β„•)β€˜π‘) = ((πŸ­β€˜β„•)β€˜(𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))))
237225, 226, 235, 236fmptco 7127 . . . . 5 (⊀ β†’ (((πŸ­β€˜β„•) β†Ύ Fin) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ ((πŸ­β€˜β„•)β€˜(𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))))
238237mptru 1549 . . . 4 (((πŸ­β€˜β„•) β†Ύ Fin) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽)))))) = (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ ((πŸ­β€˜β„•)β€˜(𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))))
239214, 238eqtr4i 2764 . . 3 𝐺 = (((πŸ­β€˜β„•) β†Ύ Fin) ∘ (π‘œ ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 β€œ (π‘€β€˜(bits ∘ (π‘œ β†Ύ 𝐽))))))
240 f1oeq1 6822 . . 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 397   ∧ w3a 1088   = wceq 1542  βŠ€wtru 1543   ∈ wcel 2107  {cab 2710  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βˆ– cdif 3946   βˆͺ cun 3947   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  π’« cpw 4603  {csn 4629  {cpr 4631   class class class wbr 5149  {copab 5211   ↦ cmpt 5232   Γ— cxp 5675  β—‘ccnv 5676  ran crn 5678   β†Ύ cres 5679   β€œ cima 5680   ∘ ccom 5681  Fun wfun 6538   Fn wfn 6539  βŸΆwf 6540  β€“1-1β†’wf1 6541  β€“1-1-ontoβ†’wf1o 6543  β€˜cfv 6544  (class class class)co 7409   ∈ cmpo 7411   supp csupp 8146   ↑m cmap 8820  Fincfn 8939   finSupp cfsupp 9361  0cc0 11110  1c1 11111   Β· cmul 11115   ≀ cle 11249  β„•cn 12212  2c2 12267  β„•0cn0 12472  β„€cz 12558  β†‘cexp 14027  Ξ£csu 15632   βˆ₯ cdvds 16197  bitscbits 16360  πŸ­cind 33008
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-ac2 10458  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-disj 5115  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-supp 8147  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-oadd 8470  df-er 8703  df-map 8822  df-pm 8823  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9362  df-sup 9437  df-inf 9438  df-oi 9505  df-dju 9896  df-card 9934  df-acn 9937  df-ac 10111  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-xnn0 12545  df-z 12559  df-uz 12823  df-rp 12975  df-fz 13485  df-fzo 13628  df-fl 13757  df-mod 13835  df-seq 13967  df-exp 14028  df-hash 14291  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-clim 15432  df-sum 15633  df-dvds 16198  df-bits 16363  df-ind 33009
This theorem is referenced by:  eulerpartlemgf  33378  eulerpartlemgs2  33379  eulerpartlemn  33380
  Copyright terms: Public domain W3C validator