Step | Hyp | Ref
| Expression |
1 | | nnex 10903 |
. . . . 5
⊢ ℕ
∈ V |
2 | | indf1ofs 29415 |
. . . . 5
⊢ (ℕ
∈ V → ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ
∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚
ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin}) |
3 | 1, 2 | ax-mp 5 |
. . . 4
⊢
((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩
Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚
ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} |
4 | | incom 3767 |
. . . . . . 7
⊢ (({0, 1}
↑𝑚 ℕ) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}) = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1}
↑𝑚 ℕ)) |
5 | | eulerpart.r |
. . . . . . . 8
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈
Fin} |
6 | 5 | ineq2i 3773 |
. . . . . . 7
⊢ (({0, 1}
↑𝑚 ℕ) ∩ 𝑅) = (({0, 1} ↑𝑚
ℕ) ∩ {𝑓 ∣
(◡𝑓 “ ℕ) ∈
Fin}) |
7 | | dfrab2 3862 |
. . . . . . 7
⊢ {𝑓 ∈ ({0, 1}
↑𝑚 ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1}
↑𝑚 ℕ)) |
8 | 4, 6, 7 | 3eqtr4i 2642 |
. . . . . 6
⊢ (({0, 1}
↑𝑚 ℕ) ∩ 𝑅) = {𝑓 ∈ ({0, 1} ↑𝑚
ℕ) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
9 | | elmapfun 7767 |
. . . . . . . . 9
⊢ (𝑓 ∈ ({0, 1}
↑𝑚 ℕ) → Fun 𝑓) |
10 | | elmapi 7765 |
. . . . . . . . . 10
⊢ (𝑓 ∈ ({0, 1}
↑𝑚 ℕ) → 𝑓:ℕ⟶{0, 1}) |
11 | | frn 5966 |
. . . . . . . . . 10
⊢ (𝑓:ℕ⟶{0, 1} →
ran 𝑓 ⊆ {0,
1}) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝑓 ∈ ({0, 1}
↑𝑚 ℕ) → ran 𝑓 ⊆ {0, 1}) |
13 | | fimacnvinrn2 6257 |
. . . . . . . . . 10
⊢ ((Fun
𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (◡𝑓 “ ℕ) = (◡𝑓 “ (ℕ ∩ {0,
1}))) |
14 | | df-pr 4128 |
. . . . . . . . . . . . . 14
⊢ {0, 1} =
({0} ∪ {1}) |
15 | 14 | ineq2i 3773 |
. . . . . . . . . . . . 13
⊢ (ℕ
∩ {0, 1}) = (ℕ ∩ ({0} ∪ {1})) |
16 | | indi 3832 |
. . . . . . . . . . . . 13
⊢ (ℕ
∩ ({0} ∪ {1})) = ((ℕ ∩ {0}) ∪ (ℕ ∩
{1})) |
17 | | 0nnn 10929 |
. . . . . . . . . . . . . . 15
⊢ ¬ 0
∈ ℕ |
18 | | disjsn 4192 |
. . . . . . . . . . . . . . 15
⊢ ((ℕ
∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ) |
19 | 17, 18 | mpbir 220 |
. . . . . . . . . . . . . 14
⊢ (ℕ
∩ {0}) = ∅ |
20 | | 1nn 10908 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℕ |
21 | | 1ex 9914 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
V |
22 | 21 | snss 4259 |
. . . . . . . . . . . . . . . . 17
⊢ (1 ∈
ℕ ↔ {1} ⊆ ℕ) |
23 | 20, 22 | mpbi 219 |
. . . . . . . . . . . . . . . 16
⊢ {1}
⊆ ℕ |
24 | | dfss 3555 |
. . . . . . . . . . . . . . . 16
⊢ ({1}
⊆ ℕ ↔ {1} = ({1} ∩ ℕ)) |
25 | 23, 24 | mpbi 219 |
. . . . . . . . . . . . . . 15
⊢ {1} =
({1} ∩ ℕ) |
26 | | incom 3767 |
. . . . . . . . . . . . . . 15
⊢ ({1}
∩ ℕ) = (ℕ ∩ {1}) |
27 | 25, 26 | eqtr2i 2633 |
. . . . . . . . . . . . . 14
⊢ (ℕ
∩ {1}) = {1} |
28 | 19, 27 | uneq12i 3727 |
. . . . . . . . . . . . 13
⊢ ((ℕ
∩ {0}) ∪ (ℕ ∩ {1})) = (∅ ∪ {1}) |
29 | 15, 16, 28 | 3eqtri 2636 |
. . . . . . . . . . . 12
⊢ (ℕ
∩ {0, 1}) = (∅ ∪ {1}) |
30 | | uncom 3719 |
. . . . . . . . . . . 12
⊢ (∅
∪ {1}) = ({1} ∪ ∅) |
31 | | un0 3919 |
. . . . . . . . . . . 12
⊢ ({1}
∪ ∅) = {1} |
32 | 29, 30, 31 | 3eqtri 2636 |
. . . . . . . . . . 11
⊢ (ℕ
∩ {0, 1}) = {1} |
33 | 32 | imaeq2i 5383 |
. . . . . . . . . 10
⊢ (◡𝑓 “ (ℕ ∩ {0, 1})) = (◡𝑓 “ {1}) |
34 | 13, 33 | syl6eq 2660 |
. . . . . . . . 9
⊢ ((Fun
𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (◡𝑓 “ ℕ) = (◡𝑓 “ {1})) |
35 | 9, 12, 34 | syl2anc 691 |
. . . . . . . 8
⊢ (𝑓 ∈ ({0, 1}
↑𝑚 ℕ) → (◡𝑓 “ ℕ) = (◡𝑓 “ {1})) |
36 | 35 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑓 ∈ ({0, 1}
↑𝑚 ℕ) → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝑓 “ {1}) ∈ Fin)) |
37 | 36 | rabbiia 3161 |
. . . . . 6
⊢ {𝑓 ∈ ({0, 1}
↑𝑚 ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ ({0, 1}
↑𝑚 ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} |
38 | 8, 37 | eqtr2i 2633 |
. . . . 5
⊢ {𝑓 ∈ ({0, 1}
↑𝑚 ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} = (({0, 1}
↑𝑚 ℕ) ∩ 𝑅) |
39 | | f1oeq3 6042 |
. . . . 5
⊢ ({𝑓 ∈ ({0, 1}
↑𝑚 ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} = (({0, 1}
↑𝑚 ℕ) ∩ 𝑅) → (((𝟭‘ℕ) ↾
Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚
ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} ↔
((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩
Fin)–1-1-onto→(({0, 1} ↑𝑚 ℕ)
∩ 𝑅))) |
40 | 38, 39 | ax-mp 5 |
. . . 4
⊢
(((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩
Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚
ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} ↔
((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩
Fin)–1-1-onto→(({0, 1} ↑𝑚 ℕ)
∩ 𝑅)) |
41 | 3, 40 | mpbi 219 |
. . 3
⊢
((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩
Fin)–1-1-onto→(({0, 1} ↑𝑚 ℕ)
∩ 𝑅) |
42 | | eulerpart.j |
. . . . . . 7
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} |
43 | | eulerpart.f |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦
((2↑𝑦) · 𝑥)) |
44 | 42, 43 | oddpwdc 29743 |
. . . . . 6
⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ |
45 | | f1opwfi 8153 |
. . . . . 6
⊢ (𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ → (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin)
↦ (𝐹 “ 𝑎)):(𝒫 (𝐽 × ℕ0) ∩
Fin)–1-1-onto→(𝒫 ℕ ∩
Fin)) |
46 | 44, 45 | ax-mp 5 |
. . . . 5
⊢ (𝑎 ∈ (𝒫 (𝐽 × ℕ0)
∩ Fin) ↦ (𝐹
“ 𝑎)):(𝒫
(𝐽 ×
ℕ0) ∩ Fin)–1-1-onto→(𝒫 ℕ ∩ Fin) |
47 | | eulerpart.p |
. . . . . . . 8
⊢ 𝑃 = {𝑓 ∈ (ℕ0
↑𝑚 ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝑓‘𝑘) · 𝑘) = 𝑁)} |
48 | | eulerpart.o |
. . . . . . . 8
⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} |
49 | | eulerpart.d |
. . . . . . . 8
⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} |
50 | | eulerpart.h |
. . . . . . . 8
⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} |
51 | | eulerpart.m |
. . . . . . . 8
⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) |
52 | 47, 48, 49, 42, 43, 50, 51 | eulerpartlem1 29756 |
. . . . . . 7
⊢ 𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩
Fin) |
53 | | bitsf1o 15005 |
. . . . . . . . . . . . . 14
⊢ (bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin) |
54 | 53 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin)) |
55 | 42, 1 | rabex2 4742 |
. . . . . . . . . . . . . 14
⊢ 𝐽 ∈ V |
56 | 55 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 𝐽 ∈
V) |
57 | | nn0ex 11175 |
. . . . . . . . . . . . . 14
⊢
ℕ0 ∈ V |
58 | 57 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ ℕ0 ∈ V) |
59 | 57 | pwex 4774 |
. . . . . . . . . . . . . . 15
⊢ 𝒫
ℕ0 ∈ V |
60 | 59 | inex1 4727 |
. . . . . . . . . . . . . 14
⊢
(𝒫 ℕ0 ∩ Fin) ∈ V |
61 | 60 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (𝒫 ℕ0 ∩ Fin) ∈ V) |
62 | | 0nn0 11184 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
63 | 62 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 0 ∈ ℕ0) |
64 | | fvres 6117 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
ℕ0 → ((bits ↾ ℕ0)‘0) =
(bits‘0)) |
65 | 62, 64 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((bits
↾ ℕ0)‘0) = (bits‘0) |
66 | | 0bits 14999 |
. . . . . . . . . . . . . 14
⊢
(bits‘0) = ∅ |
67 | 65, 66 | eqtr2i 2633 |
. . . . . . . . . . . . 13
⊢ ∅ =
((bits ↾ ℕ0)‘0) |
68 | | elmapi 7765 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ (ℕ0
↑𝑚 𝐽) → 𝑓:𝐽⟶ℕ0) |
69 | | frnnn0supp 11226 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ V ∧ 𝑓:𝐽⟶ℕ0) → (𝑓 supp 0) = (◡𝑓 “ ℕ)) |
70 | 55, 68, 69 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ (ℕ0
↑𝑚 𝐽) → (𝑓 supp 0) = (◡𝑓 “ ℕ)) |
71 | 70 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (ℕ0
↑𝑚 𝐽) → ((𝑓 supp 0) ∈ Fin ↔ (◡𝑓 “ ℕ) ∈
Fin)) |
72 | 71 | rabbiia 3161 |
. . . . . . . . . . . . . 14
⊢ {𝑓 ∈ (ℕ0
↑𝑚 𝐽) ∣ (𝑓 supp 0) ∈ Fin} = {𝑓 ∈ (ℕ0
↑𝑚 𝐽) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
73 | | elmapfun 7767 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ (ℕ0
↑𝑚 𝐽) → Fun 𝑓) |
74 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑓 ∈ V |
75 | | funisfsupp 8163 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝑓 ∧ 𝑓 ∈ V ∧ 0 ∈ ℕ0)
→ (𝑓 finSupp 0 ↔
(𝑓 supp 0) ∈
Fin)) |
76 | 74, 62, 75 | mp3an23 1408 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
𝑓 → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈
Fin)) |
77 | 73, 76 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (ℕ0
↑𝑚 𝐽) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin)) |
78 | 77 | rabbiia 3161 |
. . . . . . . . . . . . . 14
⊢ {𝑓 ∈ (ℕ0
↑𝑚 𝐽) ∣ 𝑓 finSupp 0} = {𝑓 ∈ (ℕ0
↑𝑚 𝐽) ∣ (𝑓 supp 0) ∈ Fin} |
79 | | incom 3767 |
. . . . . . . . . . . . . . 15
⊢ ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩
(ℕ0 ↑𝑚 𝐽)) = ((ℕ0
↑𝑚 𝐽) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
80 | | dfrab2 3862 |
. . . . . . . . . . . . . . 15
⊢ {𝑓 ∈ (ℕ0
↑𝑚 𝐽) ∣ (◡𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩
(ℕ0 ↑𝑚 𝐽)) |
81 | 5 | ineq2i 3773 |
. . . . . . . . . . . . . . 15
⊢
((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) = ((ℕ0
↑𝑚 𝐽) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
82 | 79, 80, 81 | 3eqtr4ri 2643 |
. . . . . . . . . . . . . 14
⊢
((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0
↑𝑚 𝐽) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
83 | 72, 78, 82 | 3eqtr4ri 2643 |
. . . . . . . . . . . . 13
⊢
((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0
↑𝑚 𝐽) ∣ 𝑓 finSupp 0} |
84 | | elmapfun 7767 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 ∈ ((𝒫
ℕ0 ∩ Fin) ↑𝑚 𝐽) → Fun 𝑟) |
85 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑟 ∈ V |
86 | | 0ex 4718 |
. . . . . . . . . . . . . . . . 17
⊢ ∅
∈ V |
87 | | funisfsupp 8163 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝑟 ∧ 𝑟 ∈ V ∧ ∅ ∈ V) →
(𝑟 finSupp ∅ ↔
(𝑟 supp ∅) ∈
Fin)) |
88 | 85, 86, 87 | mp3an23 1408 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
𝑟 → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈
Fin)) |
89 | 88 | bicomd 212 |
. . . . . . . . . . . . . . 15
⊢ (Fun
𝑟 → ((𝑟 supp ∅) ∈ Fin ↔
𝑟 finSupp
∅)) |
90 | 84, 89 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ ((𝒫
ℕ0 ∩ Fin) ↑𝑚 𝐽) → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp
∅)) |
91 | 90 | rabbiia 3161 |
. . . . . . . . . . . . 13
⊢ {𝑟 ∈ ((𝒫
ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} = {𝑟 ∈ ((𝒫
ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ 𝑟 finSupp ∅} |
92 | 54, 56, 58, 61, 63, 67, 83, 91 | fcobijfs 28889 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑓 ∈
((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾
ℕ0) ∘ 𝑓)):((ℕ0
↑𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}) |
93 | | elinel1 3761 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) → 𝑓 ∈ (ℕ0
↑𝑚 𝐽)) |
94 | | frn 5966 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:𝐽⟶ℕ0 → ran 𝑓 ⊆
ℕ0) |
95 | | cores 5555 |
. . . . . . . . . . . . . . . . 17
⊢ (ran
𝑓 ⊆
ℕ0 → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓)) |
96 | 68, 94, 95 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ (ℕ0
↑𝑚 𝐽) → ((bits ↾ ℕ0)
∘ 𝑓) = (bits ∘
𝑓)) |
97 | 93, 96 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) → ((bits ↾ ℕ0)
∘ 𝑓) = (bits ∘
𝑓)) |
98 | 97 | mpteq2ia 4668 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾
ℕ0) ∘ 𝑓)) = (𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) |
99 | 98 | eqcomi 2619 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾
ℕ0) ∘ 𝑓)) |
100 | | f1oeq1 6040 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾
ℕ0) ∘ 𝑓)) → ((𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0
↑𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ↔ (𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾
ℕ0) ∘ 𝑓)):((ℕ0
↑𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})) |
101 | 99, 100 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (⊤
→ ((𝑓 ∈
((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0
↑𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ↔ (𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾
ℕ0) ∘ 𝑓)):((ℕ0
↑𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})) |
102 | 92, 101 | mpbird 246 |
. . . . . . . . . . 11
⊢ (⊤
→ (𝑓 ∈
((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0
↑𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}) |
103 | 102 | trud 1484 |
. . . . . . . . . 10
⊢ (𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0
↑𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} |
104 | | ssrab2 3650 |
. . . . . . . . . . . . . . . 16
⊢ {𝑧 ∈ ℕ ∣ ¬ 2
∥ 𝑧} ⊆
ℕ |
105 | 42, 104 | eqsstri 3598 |
. . . . . . . . . . . . . . 15
⊢ 𝐽 ⊆
ℕ |
106 | 1, 57, 105 | 3pm3.2i 1232 |
. . . . . . . . . . . . . 14
⊢ (ℕ
∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ) |
107 | | eulerpart.t |
. . . . . . . . . . . . . . . 16
⊢ 𝑇 = {𝑓 ∈ (ℕ0
↑𝑚 ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} |
108 | | cnveq 5218 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = 𝑜 → ◡𝑓 = ◡𝑜) |
109 | | dfn2 11182 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℕ =
(ℕ0 ∖ {0}) |
110 | 109 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = 𝑜 → ℕ = (ℕ0
∖ {0})) |
111 | 108, 110 | imaeq12d 5386 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = 𝑜 → (◡𝑓 “ ℕ) = (◡𝑜 “ (ℕ0 ∖
{0}))) |
112 | 111 | sseq1d 3595 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = 𝑜 → ((◡𝑓 “ ℕ) ⊆ 𝐽 ↔ (◡𝑜 “ (ℕ0 ∖ {0}))
⊆ 𝐽)) |
113 | 112 | cbvrabv 3172 |
. . . . . . . . . . . . . . . 16
⊢ {𝑓 ∈ (ℕ0
↑𝑚 ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} = {𝑜 ∈ (ℕ0
↑𝑚 ℕ) ∣ (◡𝑜 “ (ℕ0 ∖ {0}))
⊆ 𝐽} |
114 | 107, 113 | eqtri 2632 |
. . . . . . . . . . . . . . 15
⊢ 𝑇 = {𝑜 ∈ (ℕ0
↑𝑚 ℕ) ∣ (◡𝑜 “ (ℕ0 ∖ {0}))
⊆ 𝐽} |
115 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) |
116 | 114, 115 | resf1o 28893 |
. . . . . . . . . . . . . 14
⊢
(((ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ) ∧ 0 ∈
ℕ0) → (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0
↑𝑚 𝐽)) |
117 | 106, 62, 116 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0
↑𝑚 𝐽) |
118 | | f1of1 6049 |
. . . . . . . . . . . . 13
⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0
↑𝑚 𝐽) → (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑𝑚
𝐽)) |
119 | 117, 118 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑𝑚
𝐽) |
120 | | inss1 3795 |
. . . . . . . . . . . 12
⊢ (𝑇 ∩ 𝑅) ⊆ 𝑇 |
121 | | f1ores 6064 |
. . . . . . . . . . . 12
⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑𝑚
𝐽) ∧ (𝑇 ∩ 𝑅) ⊆ 𝑇) → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅))) |
122 | 119, 120,
121 | mp2an 704 |
. . . . . . . . . . 11
⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) |
123 | | vex 3176 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑜 ∈ V |
124 | 123 | resex 5363 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑜 ↾ 𝐽) ∈ V |
125 | 124, 115 | fnmpti 5935 |
. . . . . . . . . . . . . . . 16
⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) Fn 𝑇 |
126 | | fvelimab 6163 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) Fn 𝑇 ∧ (𝑇 ∩ 𝑅) ⊆ 𝑇) → (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓)) |
127 | 125, 120,
126 | mp2an 704 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓) |
128 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) = (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) |
129 | | vex 3176 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑚 ∈ V |
130 | 129 | resex 5363 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ↾ 𝐽) ∈ V |
131 | 128, 130 | elrnmpti 5297 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑓 = (𝑚 ↾ 𝐽)) |
132 | 47, 48, 49, 42, 43, 50, 51, 5, 107 | eulerpartlemt 29760 |
. . . . . . . . . . . . . . . . 17
⊢
((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) |
133 | 132 | eleq2i 2680 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↔ 𝑓 ∈ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))) |
134 | | elinel1 3761 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → 𝑚 ∈ 𝑇) |
135 | 115 | fvtresfn 6193 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ 𝑇 → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = (𝑚 ↾ 𝐽)) |
136 | 135 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ 𝑇 → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ (𝑚 ↾ 𝐽) = 𝑓)) |
137 | 134, 136 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ (𝑚 ↾ 𝐽) = 𝑓)) |
138 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 ↾ 𝐽) = 𝑓 ↔ 𝑓 = (𝑚 ↾ 𝐽)) |
139 | 137, 138 | syl6bb 275 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ 𝑓 = (𝑚 ↾ 𝐽))) |
140 | 139 | rexbiia 3022 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑚 ∈
(𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑓 = (𝑚 ↾ 𝐽)) |
141 | 131, 133,
140 | 3bitr4ri 292 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑚 ∈
(𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ 𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅)) |
142 | 127, 141 | bitri 263 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ 𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅)) |
143 | 142 | eqriv 2607 |
. . . . . . . . . . . . 13
⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) = ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) |
144 | | f1oeq3 6042 |
. . . . . . . . . . . . 13
⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) = ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0
↑𝑚 𝐽) ∩ 𝑅))) |
145 | 143, 144 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0
↑𝑚 𝐽) ∩ 𝑅)) |
146 | | resmpt 5369 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∩ 𝑅) ⊆ 𝑇 → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))) |
147 | | f1oeq1 6040 |
. . . . . . . . . . . . 13
⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0
↑𝑚 𝐽) ∩ 𝑅))) |
148 | 120, 146,
147 | mp2b 10 |
. . . . . . . . . . . 12
⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0
↑𝑚 𝐽) ∩ 𝑅)) |
149 | 145, 148 | bitri 263 |
. . . . . . . . . . 11
⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0
↑𝑚 𝐽) ∩ 𝑅)) |
150 | 122, 149 | mpbi 219 |
. . . . . . . . . 10
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0
↑𝑚 𝐽) ∩ 𝑅) |
151 | | f1oco 6072 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0
↑𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ∧ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0
↑𝑚 𝐽) ∩ 𝑅)) → ((𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}) |
152 | 103, 150,
151 | mp2an 704 |
. . . . . . . . 9
⊢ ((𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} |
153 | | f1of 6050 |
. . . . . . . . . . . . . 14
⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0
↑𝑚 𝐽) ∩ 𝑅) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0
↑𝑚 𝐽) ∩ 𝑅)) |
154 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) |
155 | 154 | fmpt 6289 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑜 ∈
(𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0
↑𝑚 𝐽) ∩ 𝑅)) |
156 | 155 | biimpri 217 |
. . . . . . . . . . . . . 14
⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0
↑𝑚 𝐽) ∩ 𝑅) → ∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅)) |
157 | 150, 153,
156 | mp2b 10 |
. . . . . . . . . . . . 13
⊢
∀𝑜 ∈
(𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) |
158 | 157 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ ∀𝑜 ∈
(𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅)) |
159 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))) |
160 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑓 ∈
((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓))) |
161 | | coeq2 5202 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑜 ↾ 𝐽) → (bits ∘ 𝑓) = (bits ∘ (𝑜 ↾ 𝐽))) |
162 | 158, 159,
160, 161 | fmptcof 6304 |
. . . . . . . . . . 11
⊢ (⊤
→ ((𝑓 ∈
((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) |
163 | 162 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))) = ((𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)))) |
164 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑇 ∩ 𝑅) = (𝑇 ∩ 𝑅)) |
165 | 50 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ 𝐻 = {𝑟 ∈ ((𝒫
ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}) |
166 | 163, 164,
165 | f1oeq123d 6046 |
. . . . . . . . 9
⊢ (⊤
→ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻 ↔ ((𝑓 ∈ ((ℕ0
↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})) |
167 | 152, 166 | mpbiri 247 |
. . . . . . . 8
⊢ (⊤
→ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻) |
168 | 167 | trud 1484 |
. . . . . . 7
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻 |
169 | | f1oco 6072 |
. . . . . . 7
⊢ ((𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
∧ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻) → (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩
Fin)) |
170 | 52, 168, 169 | mp2an 704 |
. . . . . 6
⊢ (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩
Fin) |
171 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (⊤
→ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) |
172 | | bitsf 14987 |
. . . . . . . . . . . . . 14
⊢
bits:ℤ⟶𝒫 ℕ0 |
173 | | zex 11263 |
. . . . . . . . . . . . . 14
⊢ ℤ
∈ V |
174 | | fex 6394 |
. . . . . . . . . . . . . 14
⊢
((bits:ℤ⟶𝒫 ℕ0 ∧ ℤ ∈
V) → bits ∈ V) |
175 | 172, 173,
174 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ bits
∈ V |
176 | 175, 124 | coex 7011 |
. . . . . . . . . . . 12
⊢ (bits
∘ (𝑜 ↾ 𝐽)) ∈ V |
177 | 176 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → (bits ∘ (𝑜 ↾ 𝐽)) ∈ V) |
178 | 171, 177 | fvmpt2d 6202 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))‘𝑜) = (bits ∘ (𝑜 ↾ 𝐽))) |
179 | | f1of 6050 |
. . . . . . . . . . . 12
⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻 → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)⟶𝐻) |
180 | 167, 179 | syl 17 |
. . . . . . . . . . 11
⊢ (⊤
→ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)⟶𝐻) |
181 | 180 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))‘𝑜) ∈ 𝐻) |
182 | 178, 181 | eqeltrrd 2689 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → (bits ∘ (𝑜 ↾ 𝐽)) ∈ 𝐻) |
183 | | f1ofn 6051 |
. . . . . . . . . . . 12
⊢ (𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
→ 𝑀 Fn 𝐻) |
184 | 52, 183 | ax-mp 5 |
. . . . . . . . . . 11
⊢ 𝑀 Fn 𝐻 |
185 | | dffn5 6151 |
. . . . . . . . . . 11
⊢ (𝑀 Fn 𝐻 ↔ 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟))) |
186 | 184, 185 | mpbi 219 |
. . . . . . . . . 10
⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟)) |
187 | 186 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟))) |
188 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑟 = (bits ∘ (𝑜 ↾ 𝐽)) → (𝑀‘𝑟) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) |
189 | 182, 171,
187, 188 | fmptco 6303 |
. . . . . . . 8
⊢ (⊤
→ (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) |
190 | 189 | trud 1484 |
. . . . . . 7
⊢ (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) |
191 | | f1oeq1 6040 |
. . . . . . 7
⊢ ((𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) → ((𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩
Fin))) |
192 | 190, 191 | ax-mp 5 |
. . . . . 6
⊢ ((𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩
Fin)) |
193 | 170, 192 | mpbi 219 |
. . . . 5
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩
Fin) |
194 | | f1oco 6072 |
. . . . 5
⊢ (((𝑎 ∈ (𝒫 (𝐽 × ℕ0)
∩ Fin) ↦ (𝐹
“ 𝑎)):(𝒫
(𝐽 ×
ℕ0) ∩ Fin)–1-1-onto→(𝒫 ℕ ∩ Fin) ∧ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin))
→ ((𝑎 ∈
(𝒫 (𝐽 ×
ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩
Fin)) |
195 | 46, 193, 194 | mp2an 704 |
. . . 4
⊢ ((𝑎 ∈ (𝒫 (𝐽 × ℕ0)
∩ Fin) ↦ (𝐹
“ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) |
196 | | simpr 476 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → 𝑜 ∈ (𝑇 ∩ 𝑅)) |
197 | | fvex 6113 |
. . . . . . . . 9
⊢ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ V |
198 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) |
199 | 198 | fvmpt2 6200 |
. . . . . . . . 9
⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ∧ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ V) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) |
200 | 196, 197,
199 | sylancl 693 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) |
201 | | f1of 6050 |
. . . . . . . . . 10
⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
→ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩
Fin)) |
202 | 193, 201 | mp1i 13 |
. . . . . . . . 9
⊢ (⊤
→ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩
Fin)) |
203 | 202 | ffvelrnda 6267 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) ∈ (𝒫 (𝐽 × ℕ0) ∩
Fin)) |
204 | 200, 203 | eqeltrrd 2689 |
. . . . . . 7
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩
Fin)) |
205 | | eqidd 2611 |
. . . . . . 7
⊢ (⊤
→ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) |
206 | | eqidd 2611 |
. . . . . . 7
⊢ (⊤
→ (𝑎 ∈ (𝒫
(𝐽 ×
ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) = (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin)
↦ (𝐹 “ 𝑎))) |
207 | | imaeq2 5381 |
. . . . . . 7
⊢ (𝑎 = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) → (𝐹 “ 𝑎) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) |
208 | 204, 205,
206, 207 | fmptco 6303 |
. . . . . 6
⊢ (⊤
→ ((𝑎 ∈
(𝒫 (𝐽 ×
ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) |
209 | 208 | trud 1484 |
. . . . 5
⊢ ((𝑎 ∈ (𝒫 (𝐽 × ℕ0)
∩ Fin) ↦ (𝐹
“ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) |
210 | | f1oeq1 6040 |
. . . . 5
⊢ (((𝑎 ∈ (𝒫 (𝐽 × ℕ0)
∩ Fin) ↦ (𝐹
“ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) → (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin)
↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩
Fin))) |
211 | 209, 210 | ax-mp 5 |
. . . 4
⊢ (((𝑎 ∈ (𝒫 (𝐽 × ℕ0)
∩ Fin) ↦ (𝐹
“ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩
Fin)) |
212 | 195, 211 | mpbi 219 |
. . 3
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) |
213 | | f1oco 6072 |
. . 3
⊢
((((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩
Fin)–1-1-onto→(({0, 1} ↑𝑚 ℕ)
∩ 𝑅) ∧ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)) →
(((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑𝑚 ℕ) ∩ 𝑅)) |
214 | 41, 212, 213 | mp2an 704 |
. 2
⊢
(((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑𝑚 ℕ) ∩ 𝑅) |
215 | | eulerpart.g |
. . . 4
⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦
((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) |
216 | 43 | mpt2exg 7134 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ V ∧
ℕ0 ∈ V) → 𝐹 ∈ V) |
217 | 55, 57, 216 | mp2an 704 |
. . . . . . . . 9
⊢ 𝐹 ∈ V |
218 | | imaexg 6995 |
. . . . . . . . 9
⊢ (𝐹 ∈ V → (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V) |
219 | 217, 218 | ax-mp 5 |
. . . . . . . 8
⊢ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V |
220 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) |
221 | 220 | fvmpt2 6200 |
. . . . . . . 8
⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ∧ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) |
222 | 196, 219,
221 | sylancl 693 |
. . . . . . 7
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) |
223 | | f1of 6050 |
. . . . . . . . 9
⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)⟶(𝒫 ℕ ∩
Fin)) |
224 | 212, 223 | mp1i 13 |
. . . . . . . 8
⊢ (⊤
→ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)⟶(𝒫 ℕ ∩
Fin)) |
225 | 224 | ffvelrnda 6267 |
. . . . . . 7
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) ∈ (𝒫 ℕ ∩
Fin)) |
226 | 222, 225 | eqeltrrd 2689 |
. . . . . 6
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ (𝒫 ℕ ∩
Fin)) |
227 | | eqidd 2611 |
. . . . . 6
⊢ (⊤
→ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) |
228 | | indf1o 29413 |
. . . . . . . . . . 11
⊢ (ℕ
∈ V → (𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0,
1} ↑𝑚 ℕ)) |
229 | | f1ofn 6051 |
. . . . . . . . . . 11
⊢
((𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0,
1} ↑𝑚 ℕ) → (𝟭‘ℕ) Fn
𝒫 ℕ) |
230 | 1, 228, 229 | mp2b 10 |
. . . . . . . . . 10
⊢
(𝟭‘ℕ) Fn 𝒫 ℕ |
231 | | dffn5 6151 |
. . . . . . . . . 10
⊢
((𝟭‘ℕ) Fn 𝒫 ℕ ↔
(𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦
((𝟭‘ℕ)‘𝑏))) |
232 | 230, 231 | mpbi 219 |
. . . . . . . . 9
⊢
(𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦
((𝟭‘ℕ)‘𝑏)) |
233 | 232 | reseq1i 5313 |
. . . . . . . 8
⊢
((𝟭‘ℕ) ↾ Fin) = ((𝑏 ∈ 𝒫 ℕ ↦
((𝟭‘ℕ)‘𝑏)) ↾ Fin) |
234 | | resmpt3 5370 |
. . . . . . . 8
⊢ ((𝑏 ∈ 𝒫 ℕ
↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
((𝟭‘ℕ)‘𝑏)) |
235 | 233, 234 | eqtri 2632 |
. . . . . . 7
⊢
((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
((𝟭‘ℕ)‘𝑏)) |
236 | 235 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
((𝟭‘ℕ)‘𝑏))) |
237 | | fveq2 6103 |
. . . . . 6
⊢ (𝑏 = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) →
((𝟭‘ℕ)‘𝑏) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) |
238 | 226, 227,
236, 237 | fmptco 6303 |
. . . . 5
⊢ (⊤
→ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦
((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))) |
239 | 238 | trud 1484 |
. . . 4
⊢
(((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦
((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) |
240 | 215, 239 | eqtr4i 2635 |
. . 3
⊢ 𝐺 = (((𝟭‘ℕ)
↾ Fin) ∘ (𝑜
∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) |
241 | | f1oeq1 6040 |
. . 3
⊢ (𝐺 = (((𝟭‘ℕ)
↾ Fin) ∘ (𝑜
∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) → (𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑𝑚 ℕ) ∩ 𝑅) ↔ (((𝟭‘ℕ) ↾
Fin) ∘ (𝑜 ∈
(𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑𝑚 ℕ) ∩ 𝑅))) |
242 | 240, 241 | ax-mp 5 |
. 2
⊢ (𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑𝑚 ℕ) ∩ 𝑅) ↔ (((𝟭‘ℕ) ↾
Fin) ∘ (𝑜 ∈
(𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑𝑚 ℕ) ∩ 𝑅)) |
243 | 214, 242 | mpbir 220 |
1
⊢ 𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑𝑚 ℕ) ∩ 𝑅) |