Step | Hyp | Ref
| Expression |
1 | | elinel2 4084 |
. . . . 5
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → 𝐴 ∈ Fin) |
2 | | 2nn0 11986 |
. . . . . . 7
⊢ 2 ∈
ℕ0 |
3 | 2 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑛 ∈ 𝐴) → 2 ∈
ℕ0) |
4 | | elfpw 8892 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) ↔ (𝐴 ⊆ ℕ0 ∧ 𝐴 ∈ Fin)) |
5 | 4 | simplbi 501 |
. . . . . . 7
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → 𝐴 ⊆
ℕ0) |
6 | 5 | sselda 3875 |
. . . . . 6
⊢ ((𝐴 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℕ0) |
7 | 3, 6 | nn0expcld 13692 |
. . . . 5
⊢ ((𝐴 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑛 ∈ 𝐴) → (2↑𝑛) ∈
ℕ0) |
8 | 1, 7 | fsumnn0cl 15179 |
. . . 4
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → Σ𝑛 ∈ 𝐴 (2↑𝑛) ∈
ℕ0) |
9 | | bitsinv1 15878 |
. . . 4
⊢
(Σ𝑛 ∈
𝐴 (2↑𝑛) ∈ ℕ0
→ Σ𝑚 ∈
(bits‘Σ𝑛 ∈
𝐴 (2↑𝑛))(2↑𝑚) = Σ𝑛 ∈ 𝐴 (2↑𝑛)) |
10 | 8, 9 | syl 17 |
. . 3
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → Σ𝑚 ∈ (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))(2↑𝑚) = Σ𝑛 ∈ 𝐴 (2↑𝑛)) |
11 | | bitsss 15862 |
. . . . . 6
⊢
(bits‘Σ𝑛
∈ 𝐴 (2↑𝑛)) ⊆
ℕ0 |
12 | 11 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) ⊆
ℕ0) |
13 | | bitsfi 15873 |
. . . . . 6
⊢
(Σ𝑛 ∈
𝐴 (2↑𝑛) ∈ ℕ0
→ (bits‘Σ𝑛
∈ 𝐴 (2↑𝑛)) ∈ Fin) |
14 | 8, 13 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) ∈ Fin) |
15 | | elfpw 8892 |
. . . . 5
⊢
((bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) ∈ (𝒫 ℕ0
∩ Fin) ↔ ((bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) ⊆ ℕ0 ∧
(bits‘Σ𝑛 ∈
𝐴 (2↑𝑛)) ∈ Fin)) |
16 | 12, 14, 15 | sylanbrc 586 |
. . . 4
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) ∈ (𝒫 ℕ0
∩ Fin)) |
17 | | oveq2 7172 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (2↑𝑛) = (2↑𝑚)) |
18 | 17 | cbvsumv 15139 |
. . . . . 6
⊢
Σ𝑛 ∈
𝑘 (2↑𝑛) = Σ𝑚 ∈ 𝑘 (2↑𝑚) |
19 | | sumeq1 15131 |
. . . . . 6
⊢ (𝑘 = (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) → Σ𝑚 ∈ 𝑘 (2↑𝑚) = Σ𝑚 ∈ (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))(2↑𝑚)) |
20 | 18, 19 | syl5eq 2785 |
. . . . 5
⊢ (𝑘 = (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) → Σ𝑛 ∈ 𝑘 (2↑𝑛) = Σ𝑚 ∈ (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))(2↑𝑚)) |
21 | | eqid 2738 |
. . . . 5
⊢ (𝑘 ∈ (𝒫
ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑘 (2↑𝑛)) = (𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛)) |
22 | | sumex 15130 |
. . . . 5
⊢
Σ𝑚 ∈
(bits‘Σ𝑛 ∈
𝐴 (2↑𝑛))(2↑𝑚) ∈ V |
23 | 20, 21, 22 | fvmpt 6769 |
. . . 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 15131 |
. . . 4
⊢ (𝑘 = 𝐴 → Σ𝑛 ∈ 𝑘 (2↑𝑛) = Σ𝑛 ∈ 𝐴 (2↑𝑛)) |
26 | | sumex 15130 |
. . . 4
⊢
Σ𝑛 ∈
𝐴 (2↑𝑛) ∈ V |
27 | 25, 21, 26 | fvmpt 6769 |
. . 3
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → ((𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛))‘𝐴) = Σ𝑛 ∈ 𝐴 (2↑𝑛)) |
28 | 10, 24, 27 | 3eqtr4d 2783 |
. 2
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → ((𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛))‘(bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))) = ((𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛))‘𝐴)) |
29 | 21 | ackbijnn 15269 |
. . . 4
⊢ (𝑘 ∈ (𝒫
ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑘 (2↑𝑛)):(𝒫 ℕ0 ∩
Fin)–1-1-onto→ℕ0 |
30 | | f1of1 6611 |
. . . 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 7025 |
. . 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 836 |
. 2
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → (((𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛))‘(bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))) = ((𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛))‘𝐴) ↔ (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) = 𝐴)) |
35 | 28, 34 | mpbid 235 |
1
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) = 𝐴) |