| Step | Hyp | Ref
| Expression |
| 1 | | nnex 12272 |
. . . . 5
⊢ ℕ
∈ V |
| 2 | | indf1ofs 32851 |
. . . . 5
⊢ (ℕ
∈ V → ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ
∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m ℕ)
∣ (◡𝑓 “ {1}) ∈ Fin}) |
| 3 | 1, 2 | ax-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} |
| 6 | 5 | ineq2i 4217 |
. . . . . . 7
⊢ (({0, 1}
↑m ℕ) ∩ 𝑅) = (({0, 1} ↑m ℕ)
∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
| 7 | | dfrab2 4320 |
. . . . . . 7
⊢ {𝑓 ∈ ({0, 1}
↑m ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1}
↑m ℕ)) |
| 8 | 4, 6, 7 | 3eqtr4i 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}) |
| 11 | 10 | frnd 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}) |
| 14 | 13 | ineq2i 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 ∈ ℕ) |
| 18 | 16, 17 | mpbir 231 |
. . . . . . . . . . . . . 14
⊢ (ℕ
∩ {0}) = ∅ |
| 19 | | 1nn 12277 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℕ |
| 20 | | 1ex 11257 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
V |
| 21 | 20 | snss 4785 |
. . . . . . . . . . . . . . . . 17
⊢ (1 ∈
ℕ ↔ {1} ⊆ ℕ) |
| 22 | 19, 21 | mpbi 230 |
. . . . . . . . . . . . . . . 16
⊢ {1}
⊆ ℕ |
| 23 | | dfss 3970 |
. . . . . . . . . . . . . . . 16
⊢ ({1}
⊆ ℕ ↔ {1} = ({1} ∩ ℕ)) |
| 24 | 22, 23 | mpbi 230 |
. . . . . . . . . . . . . . 15
⊢ {1} =
({1} ∩ ℕ) |
| 25 | | incom 4209 |
. . . . . . . . . . . . . . 15
⊢ ({1}
∩ ℕ) = (ℕ ∩ {1}) |
| 26 | 24, 25 | eqtr2i 2766 |
. . . . . . . . . . . . . 14
⊢ (ℕ
∩ {1}) = {1} |
| 27 | 18, 26 | uneq12i 4166 |
. . . . . . . . . . . . 13
⊢ ((ℕ
∩ {0}) ∪ (ℕ ∩ {1})) = (∅ ∪ {1}) |
| 28 | 14, 15, 27 | 3eqtri 2769 |
. . . . . . . . . . . 12
⊢ (ℕ
∩ {0, 1}) = (∅ ∪ {1}) |
| 29 | | uncom 4158 |
. . . . . . . . . . . 12
⊢ (∅
∪ {1}) = ({1} ∪ ∅) |
| 30 | | un0 4394 |
. . . . . . . . . . . 12
⊢ ({1}
∪ ∅) = {1} |
| 31 | 28, 29, 30 | 3eqtri 2769 |
. . . . . . . . . . 11
⊢ (ℕ
∩ {0, 1}) = {1} |
| 32 | 31 | imaeq2i 6076 |
. . . . . . . . . 10
⊢ (◡𝑓 “ (ℕ ∩ {0, 1})) = (◡𝑓 “ {1}) |
| 33 | 12, 32 | eqtrdi 2793 |
. . . . . . . . 9
⊢ ((Fun
𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (◡𝑓 “ ℕ) = (◡𝑓 “ {1})) |
| 34 | 9, 11, 33 | syl2anc 584 |
. . . . . . . 8
⊢ (𝑓 ∈ ({0, 1}
↑m ℕ) → (◡𝑓 “ ℕ) = (◡𝑓 “ {1})) |
| 35 | 34 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑓 ∈ ({0, 1}
↑m ℕ) → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝑓 “ {1}) ∈ Fin)) |
| 36 | 35 | rabbiia 3440 |
. . . . . 6
⊢ {𝑓 ∈ ({0, 1}
↑m ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ ({0, 1}
↑m ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} |
| 37 | 8, 36 | eqtr2i 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 ℕ) ∩
𝑅))) |
| 39 | 37, 38 | ax-mp 5 |
. . . 4
⊢
(((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩
Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m ℕ)
∣ (◡𝑓 “ {1}) ∈ Fin} ↔
((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩
Fin)–1-1-onto→(({0, 1} ↑m ℕ) ∩
𝑅)) |
| 40 | 3, 39 | mpbi 230 |
. . 3
⊢
((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩
Fin)–1-1-onto→(({0, 1} ↑m ℕ) ∩
𝑅) |
| 41 | | eulerpart.j |
. . . . . . 7
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} |
| 42 | | eulerpart.f |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦
((2↑𝑦) · 𝑥)) |
| 43 | 41, 42 | oddpwdc 34356 |
. . . . . 6
⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ |
| 44 | | f1opwfi 9396 |
. . . . . 6
⊢ (𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ → (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin)
↦ (𝐹 “ 𝑎)):(𝒫 (𝐽 × ℕ0) ∩
Fin)–1-1-onto→(𝒫 ℕ ∩
Fin)) |
| 45 | 43, 44 | ax-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
⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) |
| 51 | 46, 47, 48, 41, 42, 49, 50 | eulerpartlem1 34369 |
. . . . . . 7
⊢ 𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩
Fin) |
| 52 | | bitsf1o 16482 |
. . . . . . . . . . . . . 14
⊢ (bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin) |
| 53 | 52 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin)) |
| 54 | 41, 1 | rabex2 5341 |
. . . . . . . . . . . . . 14
⊢ 𝐽 ∈ V |
| 55 | 54 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 𝐽 ∈
V) |
| 56 | | nn0ex 12532 |
. . . . . . . . . . . . . 14
⊢
ℕ0 ∈ V |
| 57 | 56 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ ℕ0 ∈ V) |
| 58 | 56 | pwex 5380 |
. . . . . . . . . . . . . . 15
⊢ 𝒫
ℕ0 ∈ V |
| 59 | 58 | inex1 5317 |
. . . . . . . . . . . . . 14
⊢
(𝒫 ℕ0 ∩ Fin) ∈ V |
| 60 | 59 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (𝒫 ℕ0 ∩ Fin) ∈ V) |
| 61 | | 0nn0 12541 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
| 62 | 61 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 0 ∈ ℕ0) |
| 63 | | fvres 6925 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
ℕ0 → ((bits ↾ ℕ0)‘0) =
(bits‘0)) |
| 64 | 61, 63 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((bits
↾ ℕ0)‘0) = (bits‘0) |
| 65 | | 0bits 16476 |
. . . . . . . . . . . . . 14
⊢
(bits‘0) = ∅ |
| 66 | 64, 65 | eqtr2i 2766 |
. . . . . . . . . . . . 13
⊢ ∅ =
((bits ↾ ℕ0)‘0) |
| 67 | | elmapi 8889 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ (ℕ0
↑m 𝐽)
→ 𝑓:𝐽⟶ℕ0) |
| 68 | | fcdmnn0supp 12583 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ V ∧ 𝑓:𝐽⟶ℕ0) → (𝑓 supp 0) = (◡𝑓 “ ℕ)) |
| 69 | 54, 67, 68 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ (ℕ0
↑m 𝐽)
→ (𝑓 supp 0) = (◡𝑓 “ ℕ)) |
| 70 | 69 | eleq1d 2826 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (ℕ0
↑m 𝐽)
→ ((𝑓 supp 0) ∈
Fin ↔ (◡𝑓 “ ℕ) ∈
Fin)) |
| 71 | 70 | rabbiia 3440 |
. . . . . . . . . . . . . 14
⊢ {𝑓 ∈ (ℕ0
↑m 𝐽)
∣ (𝑓 supp 0) ∈
Fin} = {𝑓 ∈
(ℕ0 ↑m 𝐽) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
| 72 | | elmapfun 8906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ (ℕ0
↑m 𝐽)
→ Fun 𝑓) |
| 73 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑓 ∈ V |
| 74 | | funisfsupp 9407 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝑓 ∧ 𝑓 ∈ V ∧ 0 ∈ ℕ0)
→ (𝑓 finSupp 0 ↔
(𝑓 supp 0) ∈
Fin)) |
| 75 | 73, 61, 74 | mp3an23 1455 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
𝑓 → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈
Fin)) |
| 76 | 72, 75 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (ℕ0
↑m 𝐽)
→ (𝑓 finSupp 0 ↔
(𝑓 supp 0) ∈
Fin)) |
| 77 | 76 | rabbiia 3440 |
. . . . . . . . . . . . . 14
⊢ {𝑓 ∈ (ℕ0
↑m 𝐽)
∣ 𝑓 finSupp 0} =
{𝑓 ∈
(ℕ0 ↑m 𝐽) ∣ (𝑓 supp 0) ∈ Fin} |
| 78 | | incom 4209 |
. . . . . . . . . . . . . . 15
⊢ ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩
(ℕ0 ↑m 𝐽)) = ((ℕ0
↑m 𝐽) ∩
{𝑓 ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
| 79 | | dfrab2 4320 |
. . . . . . . . . . . . . . 15
⊢ {𝑓 ∈ (ℕ0
↑m 𝐽)
∣ (◡𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩
(ℕ0 ↑m 𝐽)) |
| 80 | 5 | ineq2i 4217 |
. . . . . . . . . . . . . . 15
⊢
((ℕ0 ↑m 𝐽) ∩ 𝑅) = ((ℕ0 ↑m
𝐽) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
| 81 | 78, 79, 80 | 3eqtr4ri 2776 |
. . . . . . . . . . . . . 14
⊢
((ℕ0 ↑m 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0
↑m 𝐽)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
| 82 | 71, 77, 81 | 3eqtr4ri 2776 |
. . . . . . . . . . . . 13
⊢
((ℕ0 ↑m 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0
↑m 𝐽)
∣ 𝑓 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)) |
| 87 | 84, 85, 86 | mp3an23 1455 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
𝑟 → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈
Fin)) |
| 88 | 87 | bicomd 223 |
. . . . . . . . . . . . . . 15
⊢ (Fun
𝑟 → ((𝑟 supp ∅) ∈ Fin ↔
𝑟 finSupp
∅)) |
| 89 | 83, 88 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ ((𝒫
ℕ0 ∩ Fin) ↑m 𝐽) → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp
∅)) |
| 90 | 89 | rabbiia 3440 |
. . . . . . . . . . . . 13
⊢ {𝑟 ∈ ((𝒫
ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} = {𝑟 ∈ ((𝒫
ℕ0 ∩ Fin) ↑m 𝐽) ∣ 𝑟 finSupp ∅} |
| 91 | 53, 55, 57, 60, 62, 66, 82, 90 | fcobijfs 32734 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑓 ∈
((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits ↾
ℕ0) ∘ 𝑓)):((ℕ0 ↑m
𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑m 𝐽)
∣ (𝑟 supp ∅)
∈ Fin}) |
| 92 | | elinel1 4201 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ((ℕ0
↑m 𝐽) ∩
𝑅) → 𝑓 ∈ (ℕ0
↑m 𝐽)) |
| 93 | | frn 6743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:𝐽⟶ℕ0 → ran 𝑓 ⊆
ℕ0) |
| 94 | | cores 6269 |
. . . . . . . . . . . . . . . 16
⊢ (ran
𝑓 ⊆
ℕ0 → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓)) |
| 95 | 92, 67, 93, 94 | 4syl 19 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ ((ℕ0
↑m 𝐽) ∩
𝑅) → ((bits ↾
ℕ0) ∘ 𝑓) = (bits ∘ 𝑓)) |
| 96 | 95 | mpteq2ia 5245 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ((ℕ0
↑m 𝐽) ∩
𝑅) ↦ ((bits ↾
ℕ0) ∘ 𝑓)) = (𝑓 ∈ ((ℕ0
↑m 𝐽) ∩
𝑅) ↦ (bits ∘
𝑓)) |
| 97 | 96 | eqcomi 2746 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ((ℕ0
↑m 𝐽) ∩
𝑅) ↦ (bits ∘
𝑓)) = (𝑓 ∈ ((ℕ0
↑m 𝐽) ∩
𝑅) ↦ ((bits ↾
ℕ0) ∘ 𝑓)) |
| 98 | | f1oeq1 6836 |
. . . . . . . . . . . . 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})) |
| 99 | 97, 98 | mp1i 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})) |
| 100 | 91, 99 | mpbird 257 |
. . . . . . . . . . 11
⊢ (⊤
→ (𝑓 ∈
((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0 ↑m
𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑m 𝐽)
∣ (𝑟 supp ∅)
∈ Fin}) |
| 101 | 100 | mptru 1547 |
. . . . . . . . . 10
⊢ (𝑓 ∈ ((ℕ0
↑m 𝐽) ∩
𝑅) ↦ (bits ∘
𝑓)):((ℕ0
↑m 𝐽) ∩
𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑m 𝐽)
∣ (𝑟 supp ∅)
∈ Fin} |
| 102 | | ssrab2 4080 |
. . . . . . . . . . . . . . . 16
⊢ {𝑧 ∈ ℕ ∣ ¬ 2
∥ 𝑧} ⊆
ℕ |
| 103 | 41, 102 | eqsstri 4030 |
. . . . . . . . . . . . . . 15
⊢ 𝐽 ⊆
ℕ |
| 104 | 1, 56, 103 | 3pm3.2i 1340 |
. . . . . . . . . . . . . 14
⊢ (ℕ
∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ) |
| 105 | | eulerpart.t |
. . . . . . . . . . . . . . . 16
⊢ 𝑇 = {𝑓 ∈ (ℕ0
↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} |
| 106 | | cnveq 5884 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = 𝑜 → ◡𝑓 = ◡𝑜) |
| 107 | | dfn2 12539 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℕ =
(ℕ0 ∖ {0}) |
| 108 | 107 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = 𝑜 → ℕ = (ℕ0
∖ {0})) |
| 109 | 106, 108 | imaeq12d 6079 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = 𝑜 → (◡𝑓 “ ℕ) = (◡𝑜 “ (ℕ0 ∖
{0}))) |
| 110 | 109 | sseq1d 4015 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = 𝑜 → ((◡𝑓 “ ℕ) ⊆ 𝐽 ↔ (◡𝑜 “ (ℕ0 ∖ {0}))
⊆ 𝐽)) |
| 111 | 110 | cbvrabv 3447 |
. . . . . . . . . . . . . . . 16
⊢ {𝑓 ∈ (ℕ0
↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} = {𝑜 ∈ (ℕ0
↑m ℕ) ∣ (◡𝑜 “ (ℕ0 ∖ {0}))
⊆ 𝐽} |
| 112 | 105, 111 | eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢ 𝑇 = {𝑜 ∈ (ℕ0
↑m ℕ) ∣ (◡𝑜 “ (ℕ0 ∖ {0}))
⊆ 𝐽} |
| 113 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) |
| 114 | 112, 113 | resf1o 32741 |
. . . . . . . . . . . . . 14
⊢
(((ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ) ∧ 0 ∈
ℕ0) → (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0 ↑m 𝐽)) |
| 115 | 104, 61, 114 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0 ↑m 𝐽) |
| 116 | | f1of1 6847 |
. . . . . . . . . . . . 13
⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0 ↑m 𝐽) → (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑m 𝐽)) |
| 117 | 115, 116 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑m 𝐽) |
| 118 | | inss1 4237 |
. . . . . . . . . . . 12
⊢ (𝑇 ∩ 𝑅) ⊆ 𝑇 |
| 119 | | f1ores 6862 |
. . . . . . . . . . . 12
⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑m 𝐽) ∧ (𝑇 ∩ 𝑅) ⊆ 𝑇) → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅))) |
| 120 | 117, 118,
119 | mp2an 692 |
. . . . . . . . . . 11
⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) |
| 121 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑜 ∈ V |
| 122 | 121 | resex 6047 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑜 ↾ 𝐽) ∈ V |
| 123 | 122, 113 | fnmpti 6711 |
. . . . . . . . . . . . . . . 16
⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) Fn 𝑇 |
| 124 | | fvelimab 6981 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) Fn 𝑇 ∧ (𝑇 ∩ 𝑅) ⊆ 𝑇) → (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓)) |
| 125 | 123, 118,
124 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓) |
| 126 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) = (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) |
| 127 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑚 ∈ V |
| 128 | 127 | resex 6047 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ↾ 𝐽) ∈ V |
| 129 | 126, 128 | elrnmpti 5973 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑓 = (𝑚 ↾ 𝐽)) |
| 130 | 46, 47, 48, 41, 42, 49, 50, 5, 105 | eulerpartlemt 34373 |
. . . . . . . . . . . . . . . . 17
⊢
((ℕ0 ↑m 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) |
| 131 | 130 | eleq2i 2833 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ((ℕ0
↑m 𝐽) ∩
𝑅) ↔ 𝑓 ∈ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))) |
| 132 | | elinel1 4201 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → 𝑚 ∈ 𝑇) |
| 133 | 113 | fvtresfn 7018 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ 𝑇 → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = (𝑚 ↾ 𝐽)) |
| 134 | 133 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ 𝑇 → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ (𝑚 ↾ 𝐽) = 𝑓)) |
| 135 | 132, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ (𝑚 ↾ 𝐽) = 𝑓)) |
| 136 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 ↾ 𝐽) = 𝑓 ↔ 𝑓 = (𝑚 ↾ 𝐽)) |
| 137 | 135, 136 | bitrdi 287 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ 𝑓 = (𝑚 ↾ 𝐽))) |
| 138 | 137 | rexbiia 3092 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑚 ∈
(𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑓 = (𝑚 ↾ 𝐽)) |
| 139 | 129, 131,
138 | 3bitr4ri 304 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑚 ∈
(𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ 𝑓 ∈ ((ℕ0
↑m 𝐽) ∩
𝑅)) |
| 140 | 125, 139 | bitri 275 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ 𝑓 ∈ ((ℕ0
↑m 𝐽) ∩
𝑅)) |
| 141 | 140 | eqriv 2734 |
. . . . . . . . . . . . 13
⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) = ((ℕ0
↑m 𝐽) ∩
𝑅) |
| 142 | | f1oeq3 6838 |
. . . . . . . . . . . . 13
⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) = ((ℕ0
↑m 𝐽) ∩
𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅))) |
| 143 | 141, 142 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅)) |
| 144 | | resmpt 6055 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∩ 𝑅) ⊆ 𝑇 → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))) |
| 145 | | f1oeq1 6836 |
. . . . . . . . . . . . 13
⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅))) |
| 146 | 118, 144,
145 | mp2b 10 |
. . . . . . . . . . . 12
⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅)) |
| 147 | 143, 146 | bitri 275 |
. . . . . . . . . . 11
⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅)) |
| 148 | 120, 147 | mpbi 230 |
. . . . . . . . . 10
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅) |
| 149 | | f1oco 6871 |
. . . . . . . . . 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}) |
| 150 | 101, 148,
149 | mp2an 692 |
. . . . . . . . 9
⊢ ((𝑓 ∈ ((ℕ0
↑m 𝐽) ∩
𝑅) ↦ (bits ∘
𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑m 𝐽)
∣ (𝑟 supp ∅)
∈ Fin} |
| 151 | | f1of 6848 |
. . . . . . . . . . . . . 14
⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0
↑m 𝐽) ∩
𝑅)) |
| 152 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) |
| 153 | 152 | fmpt 7130 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑜 ∈
(𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0
↑m 𝐽) ∩
𝑅) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0
↑m 𝐽) ∩
𝑅)) |
| 154 | 153 | biimpri 228 |
. . . . . . . . . . . . . 14
⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0
↑m 𝐽) ∩
𝑅) → ∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0
↑m 𝐽) ∩
𝑅)) |
| 155 | 148, 151,
154 | mp2b 10 |
. . . . . . . . . . . . 13
⊢
∀𝑜 ∈
(𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0
↑m 𝐽) ∩
𝑅) |
| 156 | 155 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ ∀𝑜 ∈
(𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0
↑m 𝐽) ∩
𝑅)) |
| 157 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))) |
| 158 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑓 ∈
((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0
↑m 𝐽) ∩
𝑅) ↦ (bits ∘
𝑓))) |
| 159 | | coeq2 5869 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑜 ↾ 𝐽) → (bits ∘ 𝑓) = (bits ∘ (𝑜 ↾ 𝐽))) |
| 160 | 156, 157,
158, 159 | fmptcof 7150 |
. . . . . . . . . . 11
⊢ (⊤
→ ((𝑓 ∈
((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) |
| 161 | 160 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))) = ((𝑓 ∈ ((ℕ0
↑m 𝐽) ∩
𝑅) ↦ (bits ∘
𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)))) |
| 162 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑇 ∩ 𝑅) = (𝑇 ∩ 𝑅)) |
| 163 | 49 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ 𝐻 = {𝑟 ∈ ((𝒫
ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}) |
| 164 | 161, 162,
163 | f1oeq123d 6842 |
. . . . . . . . 9
⊢ (⊤
→ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻 ↔ ((𝑓 ∈ ((ℕ0
↑m 𝐽) ∩
𝑅) ↦ (bits ∘
𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑m 𝐽)
∣ (𝑟 supp ∅)
∈ Fin})) |
| 165 | 150, 164 | mpbiri 258 |
. . . . . . . 8
⊢ (⊤
→ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻) |
| 166 | 165 | mptru 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)) |
| 168 | 51, 166, 167 | mp2an 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) |
| 173 | 170, 171,
172 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ bits
∈ V |
| 174 | 173, 122 | coex 7952 |
. . . . . . . . . . . 12
⊢ (bits
∘ (𝑜 ↾ 𝐽)) ∈ V |
| 175 | 174 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → (bits ∘ (𝑜 ↾ 𝐽)) ∈ V) |
| 176 | 169, 175 | fvmpt2d 7029 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))‘𝑜) = (bits ∘ (𝑜 ↾ 𝐽))) |
| 177 | | f1of 6848 |
. . . . . . . . . . . 12
⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻 → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)⟶𝐻) |
| 178 | 165, 177 | syl 17 |
. . . . . . . . . . 11
⊢ (⊤
→ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)⟶𝐻) |
| 179 | 178 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))‘𝑜) ∈ 𝐻) |
| 180 | 176, 179 | eqeltrrd 2842 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → (bits ∘ (𝑜 ↾ 𝐽)) ∈ 𝐻) |
| 181 | | f1ofn 6849 |
. . . . . . . . . . . 12
⊢ (𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
→ 𝑀 Fn 𝐻) |
| 182 | 51, 181 | ax-mp 5 |
. . . . . . . . . . 11
⊢ 𝑀 Fn 𝐻 |
| 183 | | dffn5 6967 |
. . . . . . . . . . 11
⊢ (𝑀 Fn 𝐻 ↔ 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟))) |
| 184 | 182, 183 | mpbi 230 |
. . . . . . . . . 10
⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟)) |
| 185 | 184 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟))) |
| 186 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑟 = (bits ∘ (𝑜 ↾ 𝐽)) → (𝑀‘𝑟) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) |
| 187 | 180, 169,
185, 186 | fmptco 7149 |
. . . . . . . 8
⊢ (⊤
→ (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) |
| 188 | 187 | mptru 1547 |
. . . . . . 7
⊢ (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) |
| 189 | | f1oeq1 6836 |
. . . . . . 7
⊢ ((𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) → ((𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩
Fin))) |
| 190 | 188, 189 | ax-mp 5 |
. . . . . 6
⊢ ((𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩
Fin)) |
| 191 | 168, 190 | mpbi 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)) |
| 193 | 45, 191, 192 | mp2an 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 ∘ (𝑜 ↾ 𝐽)))) |
| 197 | 196 | fvmpt2 7027 |
. . . . . . . . 9
⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ∧ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ V) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) |
| 198 | 194, 195,
197 | sylancl 586 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) |
| 199 | | f1of 6848 |
. . . . . . . . . 10
⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
→ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩
Fin)) |
| 200 | 191, 199 | mp1i 13 |
. . . . . . . . 9
⊢ (⊤
→ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩
Fin)) |
| 201 | 200 | ffvelcdmda 7104 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) ∈ (𝒫 (𝐽 × ℕ0) ∩
Fin)) |
| 202 | 198, 201 | eqeltrrd 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 ∘ (𝑜 ↾ 𝐽))))) |
| 206 | 202, 203,
204, 205 | fmptco 7149 |
. . . . . 6
⊢ (⊤
→ ((𝑎 ∈
(𝒫 (𝐽 ×
ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) |
| 207 | 206 | mptru 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))) |
| 209 | 207, 208 | ax-mp 5 |
. . . 4
⊢ (((𝑎 ∈ (𝒫 (𝐽 × ℕ0)
∩ Fin) ↦ (𝐹
“ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩
Fin)) |
| 210 | 193, 209 | mpbi 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 ℕ) ∩ 𝑅)) |
| 212 | 40, 210, 211 | mp2an 692 |
. 2
⊢
(((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑m ℕ) ∩ 𝑅) |
| 213 | | eulerpart.g |
. . . 4
⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦
((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) |
| 214 | 42 | mpoexg 8101 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ V ∧
ℕ0 ∈ V) → 𝐹 ∈ V) |
| 215 | 54, 56, 214 | mp2an 692 |
. . . . . . . . 9
⊢ 𝐹 ∈ V |
| 216 | | imaexg 7935 |
. . . . . . . . 9
⊢ (𝐹 ∈ V → (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V) |
| 217 | 215, 216 | ax-mp 5 |
. . . . . . . 8
⊢ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V |
| 218 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) |
| 219 | 218 | fvmpt2 7027 |
. . . . . . . 8
⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ∧ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) |
| 220 | 194, 217,
219 | sylancl 586 |
. . . . . . 7
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) |
| 221 | | f1of 6848 |
. . . . . . . . 9
⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)⟶(𝒫 ℕ ∩
Fin)) |
| 222 | 210, 221 | mp1i 13 |
. . . . . . . 8
⊢ (⊤
→ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)⟶(𝒫 ℕ ∩
Fin)) |
| 223 | 222 | ffvelcdmda 7104 |
. . . . . . 7
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) ∈ (𝒫 ℕ ∩
Fin)) |
| 224 | 220, 223 | eqeltrrd 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 𝒫
ℕ) |
| 228 | 1, 226, 227 | mp2b 10 |
. . . . . . . . . 10
⊢
(𝟭‘ℕ) Fn 𝒫 ℕ |
| 229 | | dffn5 6967 |
. . . . . . . . . 10
⊢
((𝟭‘ℕ) Fn 𝒫 ℕ ↔
(𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦
((𝟭‘ℕ)‘𝑏))) |
| 230 | 228, 229 | mpbi 230 |
. . . . . . . . 9
⊢
(𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦
((𝟭‘ℕ)‘𝑏)) |
| 231 | 230 | reseq1i 5993 |
. . . . . . . 8
⊢
((𝟭‘ℕ) ↾ Fin) = ((𝑏 ∈ 𝒫 ℕ ↦
((𝟭‘ℕ)‘𝑏)) ↾ Fin) |
| 232 | | resmpt3 6056 |
. . . . . . . 8
⊢ ((𝑏 ∈ 𝒫 ℕ
↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
((𝟭‘ℕ)‘𝑏)) |
| 233 | 231, 232 | eqtri 2765 |
. . . . . . 7
⊢
((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
((𝟭‘ℕ)‘𝑏)) |
| 234 | 233 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
((𝟭‘ℕ)‘𝑏))) |
| 235 | | fveq2 6906 |
. . . . . 6
⊢ (𝑏 = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) →
((𝟭‘ℕ)‘𝑏) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) |
| 236 | 224, 225,
234, 235 | fmptco 7149 |
. . . . 5
⊢ (⊤
→ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦
((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))) |
| 237 | 236 | mptru 1547 |
. . . 4
⊢
(((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦
((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) |
| 238 | 213, 237 | eqtr4i 2768 |
. . 3
⊢ 𝐺 = (((𝟭‘ℕ)
↾ Fin) ∘ (𝑜
∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) |
| 239 | | f1oeq1 6836 |
. . 3
⊢ (𝐺 = (((𝟭‘ℕ)
↾ Fin) ∘ (𝑜
∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) → (𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑m ℕ) ∩ 𝑅) ↔ (((𝟭‘ℕ) ↾
Fin) ∘ (𝑜 ∈
(𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑m ℕ) ∩ 𝑅))) |
| 240 | 238, 239 | ax-mp 5 |
. 2
⊢ (𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑m ℕ) ∩ 𝑅) ↔ (((𝟭‘ℕ) ↾
Fin) ∘ (𝑜 ∈
(𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑m ℕ) ∩ 𝑅)) |
| 241 | 212, 240 | mpbir 231 |
1
⊢ 𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑m ℕ) ∩ 𝑅) |