Step | Hyp | Ref
| Expression |
1 | | elinel2 4130 |
. . . . 5
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → 𝐴 ∈ Fin) |
2 | | 2nn0 12250 |
. . . . . . 7
⊢ 2 ∈
ℕ0 |
3 | 2 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑛 ∈ 𝐴) → 2 ∈
ℕ0) |
4 | | elfpw 9121 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) ↔ (𝐴 ⊆ ℕ0 ∧ 𝐴 ∈ Fin)) |
5 | 4 | simplbi 498 |
. . . . . . 7
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → 𝐴 ⊆
ℕ0) |
6 | 5 | sselda 3921 |
. . . . . 6
⊢ ((𝐴 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℕ0) |
7 | 3, 6 | nn0expcld 13961 |
. . . . 5
⊢ ((𝐴 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑛 ∈ 𝐴) → (2↑𝑛) ∈
ℕ0) |
8 | 1, 7 | fsumnn0cl 15448 |
. . . 4
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → Σ𝑛 ∈ 𝐴 (2↑𝑛) ∈
ℕ0) |
9 | | bitsinv1 16149 |
. . . 4
⊢
(Σ𝑛 ∈
𝐴 (2↑𝑛) ∈ ℕ0
→ Σ𝑚 ∈
(bits‘Σ𝑛 ∈
𝐴 (2↑𝑛))(2↑𝑚) = Σ𝑛 ∈ 𝐴 (2↑𝑛)) |
10 | 8, 9 | syl 17 |
. . 3
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → Σ𝑚 ∈ (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))(2↑𝑚) = Σ𝑛 ∈ 𝐴 (2↑𝑛)) |
11 | | bitsss 16133 |
. . . . . 6
⊢
(bits‘Σ𝑛
∈ 𝐴 (2↑𝑛)) ⊆
ℕ0 |
12 | 11 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) ⊆
ℕ0) |
13 | | bitsfi 16144 |
. . . . . 6
⊢
(Σ𝑛 ∈
𝐴 (2↑𝑛) ∈ ℕ0
→ (bits‘Σ𝑛
∈ 𝐴 (2↑𝑛)) ∈ Fin) |
14 | 8, 13 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) ∈ Fin) |
15 | | elfpw 9121 |
. . . . 5
⊢
((bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) ∈ (𝒫 ℕ0
∩ Fin) ↔ ((bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) ⊆ ℕ0 ∧
(bits‘Σ𝑛 ∈
𝐴 (2↑𝑛)) ∈ Fin)) |
16 | 12, 14, 15 | sylanbrc 583 |
. . . 4
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) ∈ (𝒫 ℕ0
∩ Fin)) |
17 | | oveq2 7283 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (2↑𝑛) = (2↑𝑚)) |
18 | 17 | cbvsumv 15408 |
. . . . . 6
⊢
Σ𝑛 ∈
𝑘 (2↑𝑛) = Σ𝑚 ∈ 𝑘 (2↑𝑚) |
19 | | sumeq1 15400 |
. . . . . 6
⊢ (𝑘 = (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) → Σ𝑚 ∈ 𝑘 (2↑𝑚) = Σ𝑚 ∈ (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))(2↑𝑚)) |
20 | 18, 19 | eqtrid 2790 |
. . . . 5
⊢ (𝑘 = (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) → Σ𝑛 ∈ 𝑘 (2↑𝑛) = Σ𝑚 ∈ (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))(2↑𝑚)) |
21 | | eqid 2738 |
. . . . 5
⊢ (𝑘 ∈ (𝒫
ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑘 (2↑𝑛)) = (𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛)) |
22 | | sumex 15399 |
. . . . 5
⊢
Σ𝑚 ∈
(bits‘Σ𝑛 ∈
𝐴 (2↑𝑛))(2↑𝑚) ∈ V |
23 | 20, 21, 22 | fvmpt 6875 |
. . . 4
⊢
((bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) ∈ (𝒫 ℕ0
∩ Fin) → ((𝑘
∈ (𝒫 ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑘 (2↑𝑛))‘(bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))) = Σ𝑚 ∈ (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))(2↑𝑚)) |
24 | 16, 23 | syl 17 |
. . 3
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → ((𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛))‘(bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))) = Σ𝑚 ∈ (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))(2↑𝑚)) |
25 | | sumeq1 15400 |
. . . 4
⊢ (𝑘 = 𝐴 → Σ𝑛 ∈ 𝑘 (2↑𝑛) = Σ𝑛 ∈ 𝐴 (2↑𝑛)) |
26 | | sumex 15399 |
. . . 4
⊢
Σ𝑛 ∈
𝐴 (2↑𝑛) ∈ V |
27 | 25, 21, 26 | fvmpt 6875 |
. . 3
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → ((𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛))‘𝐴) = Σ𝑛 ∈ 𝐴 (2↑𝑛)) |
28 | 10, 24, 27 | 3eqtr4d 2788 |
. 2
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → ((𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛))‘(bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))) = ((𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛))‘𝐴)) |
29 | 21 | ackbijnn 15540 |
. . . 4
⊢ (𝑘 ∈ (𝒫
ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑘 (2↑𝑛)):(𝒫 ℕ0 ∩
Fin)–1-1-onto→ℕ0 |
30 | | f1of1 6715 |
. . . 4
⊢ ((𝑘 ∈ (𝒫
ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑘 (2↑𝑛)):(𝒫 ℕ0 ∩
Fin)–1-1-onto→ℕ0 → (𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛)):(𝒫
ℕ0 ∩ Fin)–1-1→ℕ0) |
31 | 29, 30 | mp1i 13 |
. . 3
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → (𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛)):(𝒫
ℕ0 ∩ Fin)–1-1→ℕ0) |
32 | | id 22 |
. . 3
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → 𝐴 ∈ (𝒫 ℕ0 ∩
Fin)) |
33 | | f1fveq 7135 |
. . 3
⊢ (((𝑘 ∈ (𝒫
ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑘 (2↑𝑛)):(𝒫 ℕ0 ∩
Fin)–1-1→ℕ0
∧ ((bits‘Σ𝑛
∈ 𝐴 (2↑𝑛)) ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝐴 ∈ (𝒫 ℕ0 ∩
Fin))) → (((𝑘 ∈
(𝒫 ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑘 (2↑𝑛))‘(bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))) = ((𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛))‘𝐴) ↔ (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) = 𝐴)) |
34 | 31, 16, 32, 33 | syl12anc 834 |
. 2
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → (((𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛))‘(bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))) = ((𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛))‘𝐴) ↔ (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) = 𝐴)) |
35 | 28, 34 | mpbid 231 |
1
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) = 𝐴) |