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 34374
Description: Lemma for eulerpart 34384: The 𝐺 function is a bijection. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
Hypotheses
Ref Expression
eulerpart.p 𝑃 = {𝑓 ∈ (ℕ0m ℕ) ∣ ((𝑓 “ ℕ) ∈ 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 𝑇 = {𝑓 ∈ (ℕ0m ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽}
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 12272 . . . . 5 ℕ ∈ V
2 indf1ofs 32851 . . . . 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 4209 . . . . . . 7 (({0, 1} ↑m ℕ) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}) = ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑m ℕ))
5 eulerpart.r . . . . . . . 8 𝑅 = {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}
65ineq2i 4217 . . . . . . 7 (({0, 1} ↑m ℕ) ∩ 𝑅) = (({0, 1} ↑m ℕ) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin})
7 dfrab2 4320 . . . . . . 7 {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑m ℕ))
84, 6, 73eqtr4i 2775 . . . . . 6 (({0, 1} ↑m ℕ) ∩ 𝑅) = {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ ℕ) ∈ Fin}
9 elmapfun 8906 . . . . . . . . 9 (𝑓 ∈ ({0, 1} ↑m ℕ) → Fun 𝑓)
10 elmapi 8889 . . . . . . . . . 10 (𝑓 ∈ ({0, 1} ↑m ℕ) → 𝑓:ℕ⟶{0, 1})
1110frnd 6744 . . . . . . . . 9 (𝑓 ∈ ({0, 1} ↑m ℕ) → ran 𝑓 ⊆ {0, 1})
12 fimacnvinrn2 7092 . . . . . . . . . 10 ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓 “ ℕ) = (𝑓 “ (ℕ ∩ {0, 1})))
13 df-pr 4629 . . . . . . . . . . . . . 14 {0, 1} = ({0} ∪ {1})
1413ineq2i 4217 . . . . . . . . . . . . 13 (ℕ ∩ {0, 1}) = (ℕ ∩ ({0} ∪ {1}))
15 indi 4284 . . . . . . . . . . . . 13 (ℕ ∩ ({0} ∪ {1})) = ((ℕ ∩ {0}) ∪ (ℕ ∩ {1}))
16 0nnn 12302 . . . . . . . . . . . . . . 15 ¬ 0 ∈ ℕ
17 disjsn 4711 . . . . . . . . . . . . . . 15 ((ℕ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ)
1816, 17mpbir 231 . . . . . . . . . . . . . 14 (ℕ ∩ {0}) = ∅
19 1nn 12277 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ
20 1ex 11257 . . . . . . . . . . . . . . . . . 18 1 ∈ V
2120snss 4785 . . . . . . . . . . . . . . . . 17 (1 ∈ ℕ ↔ {1} ⊆ ℕ)
2219, 21mpbi 230 . . . . . . . . . . . . . . . 16 {1} ⊆ ℕ
23 dfss 3970 . . . . . . . . . . . . . . . 16 ({1} ⊆ ℕ ↔ {1} = ({1} ∩ ℕ))
2422, 23mpbi 230 . . . . . . . . . . . . . . 15 {1} = ({1} ∩ ℕ)
25 incom 4209 . . . . . . . . . . . . . . 15 ({1} ∩ ℕ) = (ℕ ∩ {1})
2624, 25eqtr2i 2766 . . . . . . . . . . . . . 14 (ℕ ∩ {1}) = {1}
2718, 26uneq12i 4166 . . . . . . . . . . . . 13 ((ℕ ∩ {0}) ∪ (ℕ ∩ {1})) = (∅ ∪ {1})
2814, 15, 273eqtri 2769 . . . . . . . . . . . 12 (ℕ ∩ {0, 1}) = (∅ ∪ {1})
29 uncom 4158 . . . . . . . . . . . 12 (∅ ∪ {1}) = ({1} ∪ ∅)
30 un0 4394 . . . . . . . . . . . 12 ({1} ∪ ∅) = {1}
3128, 29, 303eqtri 2769 . . . . . . . . . . 11 (ℕ ∩ {0, 1}) = {1}
3231imaeq2i 6076 . . . . . . . . . 10 (𝑓 “ (ℕ ∩ {0, 1})) = (𝑓 “ {1})
3312, 32eqtrdi 2793 . . . . . . . . 9 ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓 “ ℕ) = (𝑓 “ {1}))
349, 11, 33syl2anc 584 . . . . . . . 8 (𝑓 ∈ ({0, 1} ↑m ℕ) → (𝑓 “ ℕ) = (𝑓 “ {1}))
3534eleq1d 2826 . . . . . . 7 (𝑓 ∈ ({0, 1} ↑m ℕ) → ((𝑓 “ ℕ) ∈ Fin ↔ (𝑓 “ {1}) ∈ Fin))
3635rabbiia 3440 . . . . . 6 {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ {1}) ∈ Fin}
378, 36eqtr2i 2766 . . . . 5 {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ {1}) ∈ Fin} = (({0, 1} ↑m ℕ) ∩ 𝑅)
38 f1oeq3 6838 . . . . 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 230 . . 3 ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
41 eulerpart.j . . . . . . 7 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
42 eulerpart.f . . . . . . 7 𝐹 = (𝑥𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
4341, 42oddpwdc 34356 . . . . . 6 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
44 f1opwfi 9396 . . . . . 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 𝑃 = {𝑓 ∈ (ℕ0m ℕ) ∣ ((𝑓 “ ℕ) ∈ 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 34369 . . . . . . 7 𝑀:𝐻1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
52 bitsf1o 16482 . . . . . . . . . . . . . 14 (bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin)
5352a1i 11 . . . . . . . . . . . . 13 (⊤ → (bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin))
5441, 1rabex2 5341 . . . . . . . . . . . . . 14 𝐽 ∈ V
5554a1i 11 . . . . . . . . . . . . 13 (⊤ → 𝐽 ∈ V)
56 nn0ex 12532 . . . . . . . . . . . . . 14 0 ∈ V
5756a1i 11 . . . . . . . . . . . . 13 (⊤ → ℕ0 ∈ V)
5856pwex 5380 . . . . . . . . . . . . . . 15 𝒫 ℕ0 ∈ V
5958inex1 5317 . . . . . . . . . . . . . 14 (𝒫 ℕ0 ∩ Fin) ∈ V
6059a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝒫 ℕ0 ∩ Fin) ∈ V)
61 0nn0 12541 . . . . . . . . . . . . . 14 0 ∈ ℕ0
6261a1i 11 . . . . . . . . . . . . 13 (⊤ → 0 ∈ ℕ0)
63 fvres 6925 . . . . . . . . . . . . . . 15 (0 ∈ ℕ0 → ((bits ↾ ℕ0)‘0) = (bits‘0))
6461, 63ax-mp 5 . . . . . . . . . . . . . 14 ((bits ↾ ℕ0)‘0) = (bits‘0)
65 0bits 16476 . . . . . . . . . . . . . 14 (bits‘0) = ∅
6664, 65eqtr2i 2766 . . . . . . . . . . . . 13 ∅ = ((bits ↾ ℕ0)‘0)
67 elmapi 8889 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (ℕ0m 𝐽) → 𝑓:𝐽⟶ℕ0)
68 fcdmnn0supp 12583 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ V ∧ 𝑓:𝐽⟶ℕ0) → (𝑓 supp 0) = (𝑓 “ ℕ))
6954, 67, 68sylancr 587 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (ℕ0m 𝐽) → (𝑓 supp 0) = (𝑓 “ ℕ))
7069eleq1d 2826 . . . . . . . . . . . . . . 15 (𝑓 ∈ (ℕ0m 𝐽) → ((𝑓 supp 0) ∈ Fin ↔ (𝑓 “ ℕ) ∈ Fin))
7170rabbiia 3440 . . . . . . . . . . . . . 14 {𝑓 ∈ (ℕ0m 𝐽) ∣ (𝑓 supp 0) ∈ Fin} = {𝑓 ∈ (ℕ0m 𝐽) ∣ (𝑓 “ ℕ) ∈ Fin}
72 elmapfun 8906 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (ℕ0m 𝐽) → Fun 𝑓)
73 vex 3484 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
74 funisfsupp 9407 . . . . . . . . . . . . . . . . 17 ((Fun 𝑓𝑓 ∈ V ∧ 0 ∈ ℕ0) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7573, 61, 74mp3an23 1455 . . . . . . . . . . . . . . . 16 (Fun 𝑓 → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7672, 75syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ (ℕ0m 𝐽) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7776rabbiia 3440 . . . . . . . . . . . . . 14 {𝑓 ∈ (ℕ0m 𝐽) ∣ 𝑓 finSupp 0} = {𝑓 ∈ (ℕ0m 𝐽) ∣ (𝑓 supp 0) ∈ Fin}
78 incom 4209 . . . . . . . . . . . . . . 15 ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0m 𝐽)) = ((ℕ0m 𝐽) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin})
79 dfrab2 4320 . . . . . . . . . . . . . . 15 {𝑓 ∈ (ℕ0m 𝐽) ∣ (𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0m 𝐽))
805ineq2i 4217 . . . . . . . . . . . . . . 15 ((ℕ0m 𝐽) ∩ 𝑅) = ((ℕ0m 𝐽) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin})
8178, 79, 803eqtr4ri 2776 . . . . . . . . . . . . . 14 ((ℕ0m 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0m 𝐽) ∣ (𝑓 “ ℕ) ∈ Fin}
8271, 77, 813eqtr4ri 2776 . . . . . . . . . . . . 13 ((ℕ0m 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0m 𝐽) ∣ 𝑓 finSupp 0}
83 elmapfun 8906 . . . . . . . . . . . . . . 15 (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) → Fun 𝑟)
84 vex 3484 . . . . . . . . . . . . . . . . 17 𝑟 ∈ V
85 0ex 5307 . . . . . . . . . . . . . . . . 17 ∅ ∈ V
86 funisfsupp 9407 . . . . . . . . . . . . . . . . 17 ((Fun 𝑟𝑟 ∈ V ∧ ∅ ∈ V) → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
8784, 85, 86mp3an23 1455 . . . . . . . . . . . . . . . 16 (Fun 𝑟 → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
8887bicomd 223 . . . . . . . . . . . . . . 15 (Fun 𝑟 → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
8983, 88syl 17 . . . . . . . . . . . . . 14 (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
9089rabbiia 3440 . . . . . . . . . . . . 13 {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ 𝑟 finSupp ∅}
9153, 55, 57, 60, 62, 66, 82, 90fcobijfs 32734 . . . . . . . . . . . 12 (⊤ → (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
92 elinel1 4201 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) → 𝑓 ∈ (ℕ0m 𝐽))
93 frn 6743 . . . . . . . . . . . . . . . 16 (𝑓:𝐽⟶ℕ0 → ran 𝑓 ⊆ ℕ0)
94 cores 6269 . . . . . . . . . . . . . . . 16 (ran 𝑓 ⊆ ℕ0 → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
9592, 67, 93, 944syl 19 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
9695mpteq2ia 5245 . . . . . . . . . . . . . 14 (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)) = (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓))
9796eqcomi 2746 . . . . . . . . . . . . 13 (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓))
98 f1oeq1 6836 . . . . . . . . . . . . 13 ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)) → ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ↔ (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}))
9997, 98mp1i 13 . . . . . . . . . . . 12 (⊤ → ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ↔ (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}))
10091, 99mpbird 257 . . . . . . . . . . 11 (⊤ → (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
101100mptru 1547 . . . . . . . . . 10 (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
102 ssrab2 4080 . . . . . . . . . . . . . . . 16 {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
10341, 102eqsstri 4030 . . . . . . . . . . . . . . 15 𝐽 ⊆ ℕ
1041, 56, 1033pm3.2i 1340 . . . . . . . . . . . . . 14 (ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ)
105 eulerpart.t . . . . . . . . . . . . . . . 16 𝑇 = {𝑓 ∈ (ℕ0m ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽}
106 cnveq 5884 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑜𝑓 = 𝑜)
107 dfn2 12539 . . . . . . . . . . . . . . . . . . . 20 ℕ = (ℕ0 ∖ {0})
108107a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑜 → ℕ = (ℕ0 ∖ {0}))
109106, 108imaeq12d 6079 . . . . . . . . . . . . . . . . . 18 (𝑓 = 𝑜 → (𝑓 “ ℕ) = (𝑜 “ (ℕ0 ∖ {0})))
110109sseq1d 4015 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑜 → ((𝑓 “ ℕ) ⊆ 𝐽 ↔ (𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽))
111110cbvrabv 3447 . . . . . . . . . . . . . . . 16 {𝑓 ∈ (ℕ0m ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽} = {𝑜 ∈ (ℕ0m ℕ) ∣ (𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
112105, 111eqtri 2765 . . . . . . . . . . . . . . 15 𝑇 = {𝑜 ∈ (ℕ0m ℕ) ∣ (𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
113 eqid 2737 . . . . . . . . . . . . . . 15 (𝑜𝑇 ↦ (𝑜𝐽)) = (𝑜𝑇 ↦ (𝑜𝐽))
114112, 113resf1o 32741 . . . . . . . . . . . . . 14 (((ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ) ∧ 0 ∈ ℕ0) → (𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1-onto→(ℕ0m 𝐽))
115104, 61, 114mp2an 692 . . . . . . . . . . . . 13 (𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1-onto→(ℕ0m 𝐽)
116 f1of1 6847 . . . . . . . . . . . . 13 ((𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1-onto→(ℕ0m 𝐽) → (𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1→(ℕ0m 𝐽))
117115, 116ax-mp 5 . . . . . . . . . . . 12 (𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1→(ℕ0m 𝐽)
118 inss1 4237 . . . . . . . . . . . 12 (𝑇𝑅) ⊆ 𝑇
119 f1ores 6862 . . . . . . . . . . . 12 (((𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1→(ℕ0m 𝐽) ∧ (𝑇𝑅) ⊆ 𝑇) → ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)))
120117, 118, 119mp2an 692 . . . . . . . . . . 11 ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅))
121 vex 3484 . . . . . . . . . . . . . . . . . 18 𝑜 ∈ V
122121resex 6047 . . . . . . . . . . . . . . . . 17 (𝑜𝐽) ∈ V
123122, 113fnmpti 6711 . . . . . . . . . . . . . . . 16 (𝑜𝑇 ↦ (𝑜𝐽)) Fn 𝑇
124 fvelimab 6981 . . . . . . . . . . . . . . . 16 (((𝑜𝑇 ↦ (𝑜𝐽)) Fn 𝑇 ∧ (𝑇𝑅) ⊆ 𝑇) → (𝑓 ∈ ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓))
125123, 118, 124mp2an 692 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓)
126 eqid 2737 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽)) = (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽))
127 vex 3484 . . . . . . . . . . . . . . . . . 18 𝑚 ∈ V
128127resex 6047 . . . . . . . . . . . . . . . . 17 (𝑚𝐽) ∈ V
129126, 128elrnmpti 5973 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽)) ↔ ∃𝑚 ∈ (𝑇𝑅)𝑓 = (𝑚𝐽))
13046, 47, 48, 41, 42, 49, 50, 5, 105eulerpartlemt 34373 . . . . . . . . . . . . . . . . 17 ((ℕ0m 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽))
131130eleq2i 2833 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↔ 𝑓 ∈ ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽)))
132 elinel1 4201 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ (𝑇𝑅) → 𝑚𝑇)
133113fvtresfn 7018 . . . . . . . . . . . . . . . . . . . 20 (𝑚𝑇 → ((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = (𝑚𝐽))
134133eqeq1d 2739 . . . . . . . . . . . . . . . . . . 19 (𝑚𝑇 → (((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓 ↔ (𝑚𝐽) = 𝑓))
135132, 134syl 17 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (𝑇𝑅) → (((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓 ↔ (𝑚𝐽) = 𝑓))
136 eqcom 2744 . . . . . . . . . . . . . . . . . 18 ((𝑚𝐽) = 𝑓𝑓 = (𝑚𝐽))
137135, 136bitrdi 287 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ (𝑇𝑅) → (((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓𝑓 = (𝑚𝐽)))
138137rexbiia 3092 . . . . . . . . . . . . . . . 16 (∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓 ↔ ∃𝑚 ∈ (𝑇𝑅)𝑓 = (𝑚𝐽))
139129, 131, 1383bitr4ri 304 . . . . . . . . . . . . . . 15 (∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅))
140125, 139bitri 275 . . . . . . . . . . . . . 14 (𝑓 ∈ ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ 𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅))
141140eqriv 2734 . . . . . . . . . . . . 13 ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) = ((ℕ0m 𝐽) ∩ 𝑅)
142 f1oeq3 6838 . . . . . . . . . . . . 13 (((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) = ((ℕ0m 𝐽) ∩ 𝑅) → (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅)))
143141, 142ax-mp 5 . . . . . . . . . . . 12 (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅))
144 resmpt 6055 . . . . . . . . . . . . 13 ((𝑇𝑅) ⊆ 𝑇 → ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)))
145 f1oeq1 6836 . . . . . . . . . . . . 13 (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)) → (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅)))
146118, 144, 145mp2b 10 . . . . . . . . . . . 12 (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅))
147143, 146bitri 275 . . . . . . . . . . 11 (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅))
148120, 147mpbi 230 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅)
149 f1oco 6871 . . . . . . . . . 10 (((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ∧ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅)) → ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))):(𝑇𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
150101, 148, 149mp2an 692 . . . . . . . . 9 ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))):(𝑇𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
151 f1of 6848 . . . . . . . . . . . . . 14 ((𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅) → (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)⟶((ℕ0m 𝐽) ∩ 𝑅))
152 eqid 2737 . . . . . . . . . . . . . . . 16 (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))
153152fmpt 7130 . . . . . . . . . . . . . . 15 (∀𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)⟶((ℕ0m 𝐽) ∩ 𝑅))
154153biimpri 228 . . . . . . . . . . . . . 14 ((𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)⟶((ℕ0m 𝐽) ∩ 𝑅) → ∀𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0m 𝐽) ∩ 𝑅))
155148, 151, 154mp2b 10 . . . . . . . . . . . . 13 𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0m 𝐽) ∩ 𝑅)
156155a1i 11 . . . . . . . . . . . 12 (⊤ → ∀𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0m 𝐽) ∩ 𝑅))
157 eqidd 2738 . . . . . . . . . . . 12 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)))
158 eqidd 2738 . . . . . . . . . . . 12 (⊤ → (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)))
159 coeq2 5869 . . . . . . . . . . . 12 (𝑓 = (𝑜𝐽) → (bits ∘ 𝑓) = (bits ∘ (𝑜𝐽)))
160156, 157, 158, 159fmptcof 7150 . . . . . . . . . . 11 (⊤ → ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))) = (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))))
161160eqcomd 2743 . . . . . . . . . 10 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))) = ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))))
162 eqidd 2738 . . . . . . . . . 10 (⊤ → (𝑇𝑅) = (𝑇𝑅))
16349a1i 11 . . . . . . . . . 10 (⊤ → 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
164161, 162, 163f1oeq123d 6842 . . . . . . . . 9 (⊤ → ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻 ↔ ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))):(𝑇𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}))
165150, 164mpbiri 258 . . . . . . . 8 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻)
166165mptru 1547 . . . . . . 7 (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻
167 f1oco 6871 . . . . . . 7 ((𝑀:𝐻1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ∧ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻) → (𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin))
16851, 166, 167mp2an 692 . . . . . 6 (𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
169 eqidd 2738 . . . . . . . . . . 11 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))) = (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))))
170 bitsf 16464 . . . . . . . . . . . . . 14 bits:ℤ⟶𝒫 ℕ0
171 zex 12622 . . . . . . . . . . . . . 14 ℤ ∈ V
172 fex 7246 . . . . . . . . . . . . . 14 ((bits:ℤ⟶𝒫 ℕ0 ∧ ℤ ∈ V) → bits ∈ V)
173170, 171, 172mp2an 692 . . . . . . . . . . . . 13 bits ∈ V
174173, 122coex 7952 . . . . . . . . . . . 12 (bits ∘ (𝑜𝐽)) ∈ V
175174a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (bits ∘ (𝑜𝐽)) ∈ V)
176169, 175fvmpt2d 7029 . . . . . . . . . 10 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))‘𝑜) = (bits ∘ (𝑜𝐽)))
177 f1of 6848 . . . . . . . . . . . 12 ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻 → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)⟶𝐻)
178165, 177syl 17 . . . . . . . . . . 11 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)⟶𝐻)
179178ffvelcdmda 7104 . . . . . . . . . 10 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))‘𝑜) ∈ 𝐻)
180176, 179eqeltrrd 2842 . . . . . . . . 9 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (bits ∘ (𝑜𝐽)) ∈ 𝐻)
181 f1ofn 6849 . . . . . . . . . . . 12 (𝑀:𝐻1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → 𝑀 Fn 𝐻)
18251, 181ax-mp 5 . . . . . . . . . . 11 𝑀 Fn 𝐻
183 dffn5 6967 . . . . . . . . . . 11 (𝑀 Fn 𝐻𝑀 = (𝑟𝐻 ↦ (𝑀𝑟)))
184182, 183mpbi 230 . . . . . . . . . 10 𝑀 = (𝑟𝐻 ↦ (𝑀𝑟))
185184a1i 11 . . . . . . . . 9 (⊤ → 𝑀 = (𝑟𝐻 ↦ (𝑀𝑟)))
186 fveq2 6906 . . . . . . . . 9 (𝑟 = (bits ∘ (𝑜𝐽)) → (𝑀𝑟) = (𝑀‘(bits ∘ (𝑜𝐽))))
187180, 169, 185, 186fmptco 7149 . . . . . . . 8 (⊤ → (𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))))
188187mptru 1547 . . . . . . 7 (𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))
189 f1oeq1 6836 . . . . . . 7 ((𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))) → ((𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)))
190188, 189ax-mp 5 . . . . . 6 ((𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin))
191168, 190mpbi 230 . . . . 5 (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
192 f1oco 6871 . . . . 5 (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)):(𝒫 (𝐽 × ℕ0) ∩ Fin)–1-1-onto→(𝒫 ℕ ∩ Fin) ∧ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)) → ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin))
19345, 191, 192mp2an 692 . . . 4 ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)
194 simpr 484 . . . . . . . . 9 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → 𝑜 ∈ (𝑇𝑅))
195 fvex 6919 . . . . . . . . 9 (𝑀‘(bits ∘ (𝑜𝐽))) ∈ V
196 eqid 2737 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))
197196fvmpt2 7027 . . . . . . . . 9 ((𝑜 ∈ (𝑇𝑅) ∧ (𝑀‘(bits ∘ (𝑜𝐽))) ∈ V) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜𝐽))))
198194, 195, 197sylancl 586 . . . . . . . 8 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜𝐽))))
199 f1of 6848 . . . . . . . . . 10 ((𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
200191, 199mp1i 13 . . . . . . . . 9 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
201200ffvelcdmda 7104 . . . . . . . 8 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))‘𝑜) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
202198, 201eqeltrrd 2842 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (𝑀‘(bits ∘ (𝑜𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
203 eqidd 2738 . . . . . . 7 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))))
204 eqidd 2738 . . . . . . 7 (⊤ → (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) = (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)))
205 imaeq2 6074 . . . . . . 7 (𝑎 = (𝑀‘(bits ∘ (𝑜𝐽))) → (𝐹𝑎) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
206202, 203, 204, 205fmptco 7149 . . . . . 6 (⊤ → ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
207206mptru 1547 . . . . 5 ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
208 f1oeq1 6836 . . . . 5 (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))) → (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)))
209207, 208ax-mp 5 . . . 4 (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin))
210193, 209mpbi 230 . . 3 (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)
211 f1oco 6871 . . 3 ((((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅) ∧ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)) → (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))):(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅))
21240, 210, 211mp2an 692 . 2 (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))):(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
213 eulerpart.g . . . 4 𝐺 = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
21442mpoexg 8101 . . . . . . . . . 10 ((𝐽 ∈ V ∧ ℕ0 ∈ V) → 𝐹 ∈ V)
21554, 56, 214mp2an 692 . . . . . . . . 9 𝐹 ∈ V
216 imaexg 7935 . . . . . . . . 9 (𝐹 ∈ V → (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) ∈ V)
217215, 216ax-mp 5 . . . . . . . 8 (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) ∈ V
218 eqid 2737 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
219218fvmpt2 7027 . . . . . . . 8 ((𝑜 ∈ (𝑇𝑅) ∧ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) ∈ V) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
220194, 217, 219sylancl 586 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
221 f1of 6848 . . . . . . . . 9 ((𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) → (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)⟶(𝒫 ℕ ∩ Fin))
222210, 221mp1i 13 . . . . . . . 8 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)⟶(𝒫 ℕ ∩ Fin))
223222ffvelcdmda 7104 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))‘𝑜) ∈ (𝒫 ℕ ∩ Fin))
224220, 223eqeltrrd 2842 . . . . . 6 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) ∈ (𝒫 ℕ ∩ Fin))
225 eqidd 2738 . . . . . 6 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
226 indf1o 32849 . . . . . . . . . . 11 (ℕ ∈ V → (𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑m ℕ))
227 f1ofn 6849 . . . . . . . . . . 11 ((𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑m ℕ) → (𝟭‘ℕ) Fn 𝒫 ℕ)
2281, 226, 227mp2b 10 . . . . . . . . . 10 (𝟭‘ℕ) Fn 𝒫 ℕ
229 dffn5 6967 . . . . . . . . . 10 ((𝟭‘ℕ) Fn 𝒫 ℕ ↔ (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)))
230228, 229mpbi 230 . . . . . . . . 9 (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏))
231230reseq1i 5993 . . . . . . . 8 ((𝟭‘ℕ) ↾ Fin) = ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin)
232 resmpt3 6056 . . . . . . . 8 ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
233231, 232eqtri 2765 . . . . . . 7 ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
234233a1i 11 . . . . . 6 (⊤ → ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏)))
235 fveq2 6906 . . . . . 6 (𝑏 = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) → ((𝟭‘ℕ)‘𝑏) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
236224, 225, 234, 235fmptco 7149 . . . . 5 (⊤ → (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))))
237236mptru 1547 . . . 4 (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
238213, 237eqtr4i 2768 . . 3 𝐺 = (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
239 f1oeq1 6836 . . 3 (𝐺 = (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅) ↔ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))):(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)))
240238, 239ax-mp 5 . 2 (𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅) ↔ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))):(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅))
241212, 240mpbir 231 1 𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wa 395  w3a 1087   = wceq 1540  wtru 1541  wcel 2108  {cab 2714  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  cdif 3948  cun 3949  cin 3950  wss 3951  c0 4333  𝒫 cpw 4600  {csn 4626  {cpr 4628   class class class wbr 5143  {copab 5205  cmpt 5225   × cxp 5683  ccnv 5684  ran crn 5686  cres 5687  cima 5688  ccom 5689  Fun wfun 6555   Fn wfn 6556  wf 6557  1-1wf1 6558  1-1-ontowf1o 6560  cfv 6561  (class class class)co 7431  cmpo 7433   supp csupp 8185  m cmap 8866  Fincfn 8985   finSupp cfsupp 9401  0cc0 11155  1c1 11156   · cmul 11160  cle 11296  cn 12266  2c2 12321  0cn0 12526  cz 12613  cexp 14102  Σcsu 15722  cdvds 16290  bitscbits 16456  𝟭cind 32835
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-ac2 10503  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-disj 5111  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-map 8868  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-acn 9982  df-ac 10156  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-xnn0 12600  df-z 12614  df-uz 12879  df-rp 13035  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723  df-dvds 16291  df-bits 16459  df-ind 32836
This theorem is referenced by:  eulerpartlemgf  34381  eulerpartlemgs2  34382  eulerpartlemn  34383
  Copyright terms: Public domain W3C validator