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 34353
Description: Lemma for eulerpart 34363: 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 12269 . . . . 5 ℕ ∈ V
2 indf1ofs 34006 . . . . 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 4216 . . . . . . 7 (({0, 1} ↑m ℕ) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}) = ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑m ℕ))
5 eulerpart.r . . . . . . . 8 𝑅 = {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}
65ineq2i 4224 . . . . . . 7 (({0, 1} ↑m ℕ) ∩ 𝑅) = (({0, 1} ↑m ℕ) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin})
7 dfrab2 4325 . . . . . . 7 {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑m ℕ))
84, 6, 73eqtr4i 2772 . . . . . 6 (({0, 1} ↑m ℕ) ∩ 𝑅) = {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ ℕ) ∈ Fin}
9 elmapfun 8904 . . . . . . . . 9 (𝑓 ∈ ({0, 1} ↑m ℕ) → Fun 𝑓)
10 elmapi 8887 . . . . . . . . . 10 (𝑓 ∈ ({0, 1} ↑m ℕ) → 𝑓:ℕ⟶{0, 1})
1110frnd 6744 . . . . . . . . 9 (𝑓 ∈ ({0, 1} ↑m ℕ) → ran 𝑓 ⊆ {0, 1})
12 fimacnvinrn2 7091 . . . . . . . . . 10 ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓 “ ℕ) = (𝑓 “ (ℕ ∩ {0, 1})))
13 df-pr 4633 . . . . . . . . . . . . . 14 {0, 1} = ({0} ∪ {1})
1413ineq2i 4224 . . . . . . . . . . . . 13 (ℕ ∩ {0, 1}) = (ℕ ∩ ({0} ∪ {1}))
15 indi 4289 . . . . . . . . . . . . 13 (ℕ ∩ ({0} ∪ {1})) = ((ℕ ∩ {0}) ∪ (ℕ ∩ {1}))
16 0nnn 12299 . . . . . . . . . . . . . . 15 ¬ 0 ∈ ℕ
17 disjsn 4715 . . . . . . . . . . . . . . 15 ((ℕ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ)
1816, 17mpbir 231 . . . . . . . . . . . . . 14 (ℕ ∩ {0}) = ∅
19 1nn 12274 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ
20 1ex 11254 . . . . . . . . . . . . . . . . . 18 1 ∈ V
2120snss 4789 . . . . . . . . . . . . . . . . 17 (1 ∈ ℕ ↔ {1} ⊆ ℕ)
2219, 21mpbi 230 . . . . . . . . . . . . . . . 16 {1} ⊆ ℕ
23 dfss 3981 . . . . . . . . . . . . . . . 16 ({1} ⊆ ℕ ↔ {1} = ({1} ∩ ℕ))
2422, 23mpbi 230 . . . . . . . . . . . . . . 15 {1} = ({1} ∩ ℕ)
25 incom 4216 . . . . . . . . . . . . . . 15 ({1} ∩ ℕ) = (ℕ ∩ {1})
2624, 25eqtr2i 2763 . . . . . . . . . . . . . 14 (ℕ ∩ {1}) = {1}
2718, 26uneq12i 4175 . . . . . . . . . . . . 13 ((ℕ ∩ {0}) ∪ (ℕ ∩ {1})) = (∅ ∪ {1})
2814, 15, 273eqtri 2766 . . . . . . . . . . . 12 (ℕ ∩ {0, 1}) = (∅ ∪ {1})
29 uncom 4167 . . . . . . . . . . . 12 (∅ ∪ {1}) = ({1} ∪ ∅)
30 un0 4399 . . . . . . . . . . . 12 ({1} ∪ ∅) = {1}
3128, 29, 303eqtri 2766 . . . . . . . . . . 11 (ℕ ∩ {0, 1}) = {1}
3231imaeq2i 6077 . . . . . . . . . 10 (𝑓 “ (ℕ ∩ {0, 1})) = (𝑓 “ {1})
3312, 32eqtrdi 2790 . . . . . . . . 9 ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓 “ ℕ) = (𝑓 “ {1}))
349, 11, 33syl2anc 584 . . . . . . . 8 (𝑓 ∈ ({0, 1} ↑m ℕ) → (𝑓 “ ℕ) = (𝑓 “ {1}))
3534eleq1d 2823 . . . . . . 7 (𝑓 ∈ ({0, 1} ↑m ℕ) → ((𝑓 “ ℕ) ∈ Fin ↔ (𝑓 “ {1}) ∈ Fin))
3635rabbiia 3436 . . . . . 6 {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ {1}) ∈ Fin}
378, 36eqtr2i 2763 . . . . 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 34335 . . . . . 6 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
44 f1opwfi 9393 . . . . . 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 34348 . . . . . . 7 𝑀:𝐻1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
52 bitsf1o 16478 . . . . . . . . . . . . . 14 (bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin)
5352a1i 11 . . . . . . . . . . . . 13 (⊤ → (bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin))
5441, 1rabex2 5346 . . . . . . . . . . . . . 14 𝐽 ∈ V
5554a1i 11 . . . . . . . . . . . . 13 (⊤ → 𝐽 ∈ V)
56 nn0ex 12529 . . . . . . . . . . . . . 14 0 ∈ V
5756a1i 11 . . . . . . . . . . . . 13 (⊤ → ℕ0 ∈ V)
5856pwex 5385 . . . . . . . . . . . . . . 15 𝒫 ℕ0 ∈ V
5958inex1 5322 . . . . . . . . . . . . . 14 (𝒫 ℕ0 ∩ Fin) ∈ V
6059a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝒫 ℕ0 ∩ Fin) ∈ V)
61 0nn0 12538 . . . . . . . . . . . . . 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 16472 . . . . . . . . . . . . . 14 (bits‘0) = ∅
6664, 65eqtr2i 2763 . . . . . . . . . . . . 13 ∅ = ((bits ↾ ℕ0)‘0)
67 elmapi 8887 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (ℕ0m 𝐽) → 𝑓:𝐽⟶ℕ0)
68 fcdmnn0supp 12580 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ V ∧ 𝑓:𝐽⟶ℕ0) → (𝑓 supp 0) = (𝑓 “ ℕ))
6954, 67, 68sylancr 587 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (ℕ0m 𝐽) → (𝑓 supp 0) = (𝑓 “ ℕ))
7069eleq1d 2823 . . . . . . . . . . . . . . 15 (𝑓 ∈ (ℕ0m 𝐽) → ((𝑓 supp 0) ∈ Fin ↔ (𝑓 “ ℕ) ∈ Fin))
7170rabbiia 3436 . . . . . . . . . . . . . 14 {𝑓 ∈ (ℕ0m 𝐽) ∣ (𝑓 supp 0) ∈ Fin} = {𝑓 ∈ (ℕ0m 𝐽) ∣ (𝑓 “ ℕ) ∈ Fin}
72 elmapfun 8904 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (ℕ0m 𝐽) → Fun 𝑓)
73 vex 3481 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
74 funisfsupp 9404 . . . . . . . . . . . . . . . . 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 (𝑓 ∈ (ℕ0m 𝐽) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7776rabbiia 3436 . . . . . . . . . . . . . 14 {𝑓 ∈ (ℕ0m 𝐽) ∣ 𝑓 finSupp 0} = {𝑓 ∈ (ℕ0m 𝐽) ∣ (𝑓 supp 0) ∈ Fin}
78 incom 4216 . . . . . . . . . . . . . . 15 ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0m 𝐽)) = ((ℕ0m 𝐽) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin})
79 dfrab2 4325 . . . . . . . . . . . . . . 15 {𝑓 ∈ (ℕ0m 𝐽) ∣ (𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0m 𝐽))
805ineq2i 4224 . . . . . . . . . . . . . . 15 ((ℕ0m 𝐽) ∩ 𝑅) = ((ℕ0m 𝐽) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin})
8178, 79, 803eqtr4ri 2773 . . . . . . . . . . . . . 14 ((ℕ0m 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0m 𝐽) ∣ (𝑓 “ ℕ) ∈ Fin}
8271, 77, 813eqtr4ri 2773 . . . . . . . . . . . . 13 ((ℕ0m 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0m 𝐽) ∣ 𝑓 finSupp 0}
83 elmapfun 8904 . . . . . . . . . . . . . . 15 (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) → Fun 𝑟)
84 vex 3481 . . . . . . . . . . . . . . . . 17 𝑟 ∈ V
85 0ex 5312 . . . . . . . . . . . . . . . . 17 ∅ ∈ V
86 funisfsupp 9404 . . . . . . . . . . . . . . . . 17 ((Fun 𝑟𝑟 ∈ V ∧ ∅ ∈ V) → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
8784, 85, 86mp3an23 1452 . . . . . . . . . . . . . . . 16 (Fun 𝑟 → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
8887bicomd 223 . . . . . . . . . . . . . . 15 (Fun 𝑟 → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
8983, 88syl 17 . . . . . . . . . . . . . 14 (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
9089rabbiia 3436 . . . . . . . . . . . . 13 {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ 𝑟 finSupp ∅}
9153, 55, 57, 60, 62, 66, 82, 90fcobijfs 32740 . . . . . . . . . . . 12 (⊤ → (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
92 elinel1 4210 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) → 𝑓 ∈ (ℕ0m 𝐽))
93 frn 6743 . . . . . . . . . . . . . . . 16 (𝑓:𝐽⟶ℕ0 → ran 𝑓 ⊆ ℕ0)
94 cores 6270 . . . . . . . . . . . . . . . 16 (ran 𝑓 ⊆ ℕ0 → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
9592, 67, 93, 944syl 19 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
9695mpteq2ia 5250 . . . . . . . . . . . . . 14 (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)) = (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓))
9796eqcomi 2743 . . . . . . . . . . . . 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 1543 . . . . . . . . . 10 (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
102 ssrab2 4089 . . . . . . . . . . . . . . . 16 {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
10341, 102eqsstri 4029 . . . . . . . . . . . . . . 15 𝐽 ⊆ ℕ
1041, 56, 1033pm3.2i 1338 . . . . . . . . . . . . . 14 (ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ)
105 eulerpart.t . . . . . . . . . . . . . . . 16 𝑇 = {𝑓 ∈ (ℕ0m ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽}
106 cnveq 5886 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑜𝑓 = 𝑜)
107 dfn2 12536 . . . . . . . . . . . . . . . . . . . 20 ℕ = (ℕ0 ∖ {0})
108107a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑜 → ℕ = (ℕ0 ∖ {0}))
109106, 108imaeq12d 6080 . . . . . . . . . . . . . . . . . 18 (𝑓 = 𝑜 → (𝑓 “ ℕ) = (𝑜 “ (ℕ0 ∖ {0})))
110109sseq1d 4026 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑜 → ((𝑓 “ ℕ) ⊆ 𝐽 ↔ (𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽))
111110cbvrabv 3443 . . . . . . . . . . . . . . . 16 {𝑓 ∈ (ℕ0m ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽} = {𝑜 ∈ (ℕ0m ℕ) ∣ (𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
112105, 111eqtri 2762 . . . . . . . . . . . . . . 15 𝑇 = {𝑜 ∈ (ℕ0m ℕ) ∣ (𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
113 eqid 2734 . . . . . . . . . . . . . . 15 (𝑜𝑇 ↦ (𝑜𝐽)) = (𝑜𝑇 ↦ (𝑜𝐽))
114112, 113resf1o 32747 . . . . . . . . . . . . . 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 4244 . . . . . . . . . . . 12 (𝑇𝑅) ⊆ 𝑇
119 f1ores 6862 . . . . . . . . . . . 12 (((𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1→(ℕ0m 𝐽) ∧ (𝑇𝑅) ⊆ 𝑇) → ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)))
120117, 118, 119mp2an 692 . . . . . . . . . . 11 ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅))
121 vex 3481 . . . . . . . . . . . . . . . . . 18 𝑜 ∈ V
122121resex 6048 . . . . . . . . . . . . . . . . 17 (𝑜𝐽) ∈ V
123122, 113fnmpti 6711 . . . . . . . . . . . . . . . 16 (𝑜𝑇 ↦ (𝑜𝐽)) Fn 𝑇
124 fvelimab 6980 . . . . . . . . . . . . . . . 16 (((𝑜𝑇 ↦ (𝑜𝐽)) Fn 𝑇 ∧ (𝑇𝑅) ⊆ 𝑇) → (𝑓 ∈ ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓))
125123, 118, 124mp2an 692 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓)
126 eqid 2734 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽)) = (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽))
127 vex 3481 . . . . . . . . . . . . . . . . . 18 𝑚 ∈ V
128127resex 6048 . . . . . . . . . . . . . . . . 17 (𝑚𝐽) ∈ V
129126, 128elrnmpti 5975 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽)) ↔ ∃𝑚 ∈ (𝑇𝑅)𝑓 = (𝑚𝐽))
13046, 47, 48, 41, 42, 49, 50, 5, 105eulerpartlemt 34352 . . . . . . . . . . . . . . . . 17 ((ℕ0m 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽))
131130eleq2i 2830 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↔ 𝑓 ∈ ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽)))
132 elinel1 4210 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ (𝑇𝑅) → 𝑚𝑇)
133113fvtresfn 7017 . . . . . . . . . . . . . . . . . . . 20 (𝑚𝑇 → ((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = (𝑚𝐽))
134133eqeq1d 2736 . . . . . . . . . . . . . . . . . . 19 (𝑚𝑇 → (((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓 ↔ (𝑚𝐽) = 𝑓))
135132, 134syl 17 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (𝑇𝑅) → (((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓 ↔ (𝑚𝐽) = 𝑓))
136 eqcom 2741 . . . . . . . . . . . . . . . . . 18 ((𝑚𝐽) = 𝑓𝑓 = (𝑚𝐽))
137135, 136bitrdi 287 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ (𝑇𝑅) → (((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓𝑓 = (𝑚𝐽)))
138137rexbiia 3089 . . . . . . . . . . . . . . . 16 (∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓 ↔ ∃𝑚 ∈ (𝑇𝑅)𝑓 = (𝑚𝐽))
139129, 131, 1383bitr4ri 304 . . . . . . . . . . . . . . 15 (∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅))
140125, 139bitri 275 . . . . . . . . . . . . . 14 (𝑓 ∈ ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ 𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅))
141140eqriv 2731 . . . . . . . . . . . . 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 6056 . . . . . . . . . . . . 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 2734 . . . . . . . . . . . . . . . 16 (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))
153152fmpt 7129 . . . . . . . . . . . . . . 15 (∀𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)⟶((ℕ0m 𝐽) ∩ 𝑅))
154153biimpri 228 . . . . . . . . . . . . . 14 ((𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)⟶((ℕ0m 𝐽) ∩ 𝑅) → ∀𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0m 𝐽) ∩ 𝑅))
155148, 151, 154mp2b 10 . . . . . . . . . . . . 13 𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0m 𝐽) ∩ 𝑅)
156155a1i 11 . . . . . . . . . . . 12 (⊤ → ∀𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0m 𝐽) ∩ 𝑅))
157 eqidd 2735 . . . . . . . . . . . 12 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)))
158 eqidd 2735 . . . . . . . . . . . 12 (⊤ → (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)))
159 coeq2 5871 . . . . . . . . . . . 12 (𝑓 = (𝑜𝐽) → (bits ∘ 𝑓) = (bits ∘ (𝑜𝐽)))
160156, 157, 158, 159fmptcof 7149 . . . . . . . . . . 11 (⊤ → ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))) = (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))))
161160eqcomd 2740 . . . . . . . . . 10 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))) = ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))))
162 eqidd 2735 . . . . . . . . . 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 1543 . . . . . . 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 2735 . . . . . . . . . . 11 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))) = (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))))
170 bitsf 16460 . . . . . . . . . . . . . 14 bits:ℤ⟶𝒫 ℕ0
171 zex 12619 . . . . . . . . . . . . . 14 ℤ ∈ V
172 fex 7245 . . . . . . . . . . . . . 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 7028 . . . . . . . . . 10 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))‘𝑜) = (bits ∘ (𝑜𝐽)))
177 f1of 6848 . . . . . . . . . . . 12 ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻 → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)⟶𝐻)
178165, 177syl 17 . . . . . . . . . . 11 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)⟶𝐻)
179178ffvelcdmda 7103 . . . . . . . . . 10 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))‘𝑜) ∈ 𝐻)
180176, 179eqeltrrd 2839 . . . . . . . . 9 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (bits ∘ (𝑜𝐽)) ∈ 𝐻)
181 f1ofn 6849 . . . . . . . . . . . 12 (𝑀:𝐻1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → 𝑀 Fn 𝐻)
18251, 181ax-mp 5 . . . . . . . . . . 11 𝑀 Fn 𝐻
183 dffn5 6966 . . . . . . . . . . 11 (𝑀 Fn 𝐻𝑀 = (𝑟𝐻 ↦ (𝑀𝑟)))
184182, 183mpbi 230 . . . . . . . . . 10 𝑀 = (𝑟𝐻 ↦ (𝑀𝑟))
185184a1i 11 . . . . . . . . 9 (⊤ → 𝑀 = (𝑟𝐻 ↦ (𝑀𝑟)))
186 fveq2 6906 . . . . . . . . 9 (𝑟 = (bits ∘ (𝑜𝐽)) → (𝑀𝑟) = (𝑀‘(bits ∘ (𝑜𝐽))))
187180, 169, 185, 186fmptco 7148 . . . . . . . 8 (⊤ → (𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))))
188187mptru 1543 . . . . . . 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 2734 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))
197196fvmpt2 7026 . . . . . . . . 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 7103 . . . . . . . 8 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))‘𝑜) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
202198, 201eqeltrrd 2839 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (𝑀‘(bits ∘ (𝑜𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
203 eqidd 2735 . . . . . . 7 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))))
204 eqidd 2735 . . . . . . 7 (⊤ → (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) = (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)))
205 imaeq2 6075 . . . . . . 7 (𝑎 = (𝑀‘(bits ∘ (𝑜𝐽))) → (𝐹𝑎) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
206202, 203, 204, 205fmptco 7148 . . . . . 6 (⊤ → ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
207206mptru 1543 . . . . 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 8099 . . . . . . . . . 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 2734 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
219218fvmpt2 7026 . . . . . . . 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 7103 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))‘𝑜) ∈ (𝒫 ℕ ∩ Fin))
224220, 223eqeltrrd 2839 . . . . . 6 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) ∈ (𝒫 ℕ ∩ Fin))
225 eqidd 2735 . . . . . 6 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
226 indf1o 34004 . . . . . . . . . . 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 6966 . . . . . . . . . 10 ((𝟭‘ℕ) Fn 𝒫 ℕ ↔ (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)))
230228, 229mpbi 230 . . . . . . . . 9 (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏))
231230reseq1i 5995 . . . . . . . 8 ((𝟭‘ℕ) ↾ Fin) = ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin)
232 resmpt3 6057 . . . . . . . 8 ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
233231, 232eqtri 2762 . . . . . . 7 ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
234233a1i 11 . . . . . 6 (⊤ → ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏)))
235 fveq2 6906 . . . . . 6 (𝑏 = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) → ((𝟭‘ℕ)‘𝑏) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
236224, 225, 234, 235fmptco 7148 . . . . 5 (⊤ → (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))))
237236mptru 1543 . . . 4 (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
238213, 237eqtr4i 2765 . . 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 1086   = wceq 1536  wtru 1537  wcel 2105  {cab 2711  wral 3058  wrex 3067  {crab 3432  Vcvv 3477  cdif 3959  cun 3960  cin 3961  wss 3962  c0 4338  𝒫 cpw 4604  {csn 4630  {cpr 4632   class class class wbr 5147  {copab 5209  cmpt 5230   × cxp 5686  ccnv 5687  ran crn 5689  cres 5690  cima 5691  ccom 5692  Fun wfun 6556   Fn wfn 6557  wf 6558  1-1wf1 6559  1-1-ontowf1o 6561  cfv 6562  (class class class)co 7430  cmpo 7432   supp csupp 8183  m cmap 8864  Fincfn 8983   finSupp cfsupp 9398  0cc0 11152  1c1 11153   · cmul 11157  cle 11293  cn 12263  2c2 12318  0cn0 12523  cz 12610  cexp 14098  Σcsu 15718  cdvds 16286  bitscbits 16452  𝟭cind 33990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-ac2 10500  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-disj 5115  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-oadd 8508  df-er 8743  df-map 8866  df-pm 8867  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-sup 9479  df-inf 9480  df-oi 9547  df-dju 9938  df-card 9976  df-acn 9979  df-ac 10153  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-xnn0 12597  df-z 12611  df-uz 12876  df-rp 13032  df-fz 13544  df-fzo 13691  df-fl 13828  df-mod 13906  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719  df-dvds 16287  df-bits 16455  df-ind 33991
This theorem is referenced by:  eulerpartlemgf  34360  eulerpartlemgs2  34361  eulerpartlemn  34362
  Copyright terms: Public domain W3C validator