| Step | Hyp | Ref
| Expression |
| 1 | | elinel2 4202 |
. . . . 5
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → 𝐴 ∈ Fin) |
| 2 | | 2nn0 12543 |
. . . . . . 7
⊢ 2 ∈
ℕ0 |
| 3 | 2 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑛 ∈ 𝐴) → 2 ∈
ℕ0) |
| 4 | | elfpw 9394 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) ↔ (𝐴 ⊆ ℕ0 ∧ 𝐴 ∈ Fin)) |
| 5 | 4 | simplbi 497 |
. . . . . . 7
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → 𝐴 ⊆
ℕ0) |
| 6 | 5 | sselda 3983 |
. . . . . 6
⊢ ((𝐴 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℕ0) |
| 7 | 3, 6 | nn0expcld 14285 |
. . . . 5
⊢ ((𝐴 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑛 ∈ 𝐴) → (2↑𝑛) ∈
ℕ0) |
| 8 | 1, 7 | fsumnn0cl 15772 |
. . . 4
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → Σ𝑛 ∈ 𝐴 (2↑𝑛) ∈
ℕ0) |
| 9 | | bitsinv1 16479 |
. . . 4
⊢
(Σ𝑛 ∈
𝐴 (2↑𝑛) ∈ ℕ0
→ Σ𝑚 ∈
(bits‘Σ𝑛 ∈
𝐴 (2↑𝑛))(2↑𝑚) = Σ𝑛 ∈ 𝐴 (2↑𝑛)) |
| 10 | 8, 9 | syl 17 |
. . 3
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → Σ𝑚 ∈ (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))(2↑𝑚) = Σ𝑛 ∈ 𝐴 (2↑𝑛)) |
| 11 | | bitsss 16463 |
. . . . . 6
⊢
(bits‘Σ𝑛
∈ 𝐴 (2↑𝑛)) ⊆
ℕ0 |
| 12 | 11 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) ⊆
ℕ0) |
| 13 | | bitsfi 16474 |
. . . . . 6
⊢
(Σ𝑛 ∈
𝐴 (2↑𝑛) ∈ ℕ0
→ (bits‘Σ𝑛
∈ 𝐴 (2↑𝑛)) ∈ Fin) |
| 14 | 8, 13 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) ∈ Fin) |
| 15 | | elfpw 9394 |
. . . . 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 7439 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (2↑𝑛) = (2↑𝑚)) |
| 18 | 17 | cbvsumv 15732 |
. . . . . 6
⊢
Σ𝑛 ∈
𝑘 (2↑𝑛) = Σ𝑚 ∈ 𝑘 (2↑𝑚) |
| 19 | | sumeq1 15725 |
. . . . . 6
⊢ (𝑘 = (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) → Σ𝑚 ∈ 𝑘 (2↑𝑚) = Σ𝑚 ∈ (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))(2↑𝑚)) |
| 20 | 18, 19 | eqtrid 2789 |
. . . . 5
⊢ (𝑘 = (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) → Σ𝑛 ∈ 𝑘 (2↑𝑛) = Σ𝑚 ∈ (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))(2↑𝑚)) |
| 21 | | eqid 2737 |
. . . . 5
⊢ (𝑘 ∈ (𝒫
ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑘 (2↑𝑛)) = (𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛)) |
| 22 | | sumex 15724 |
. . . . 5
⊢
Σ𝑚 ∈
(bits‘Σ𝑛 ∈
𝐴 (2↑𝑛))(2↑𝑚) ∈ V |
| 23 | 20, 21, 22 | fvmpt 7016 |
. . . 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 15725 |
. . . 4
⊢ (𝑘 = 𝐴 → Σ𝑛 ∈ 𝑘 (2↑𝑛) = Σ𝑛 ∈ 𝐴 (2↑𝑛)) |
| 26 | | sumex 15724 |
. . . 4
⊢
Σ𝑛 ∈
𝐴 (2↑𝑛) ∈ V |
| 27 | 25, 21, 26 | fvmpt 7016 |
. . 3
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → ((𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛))‘𝐴) = Σ𝑛 ∈ 𝐴 (2↑𝑛)) |
| 28 | 10, 24, 27 | 3eqtr4d 2787 |
. 2
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → ((𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛))‘(bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))) = ((𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛))‘𝐴)) |
| 29 | 21 | ackbijnn 15864 |
. . . 4
⊢ (𝑘 ∈ (𝒫
ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑘 (2↑𝑛)):(𝒫 ℕ0 ∩
Fin)–1-1-onto→ℕ0 |
| 30 | | f1of1 6847 |
. . . 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 7282 |
. . 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 837 |
. 2
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → (((𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛))‘(bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛))) = ((𝑘 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑛
∈ 𝑘 (2↑𝑛))‘𝐴) ↔ (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) = 𝐴)) |
| 35 | 28, 34 | mpbid 232 |
1
⊢ (𝐴 ∈ (𝒫
ℕ0 ∩ Fin) → (bits‘Σ𝑛 ∈ 𝐴 (2↑𝑛)) = 𝐴) |