Step | Hyp | Ref
| Expression |
1 | | eqid 2823 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
↦ (bits‘𝑘)) =
(𝑘 ∈
ℕ0 ↦ (bits‘𝑘)) |
2 | | bitsss 15777 |
. . . . . . . . 9
⊢
(bits‘𝑘)
⊆ ℕ0 |
3 | 2 | a1i 11 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (bits‘𝑘)
⊆ ℕ0) |
4 | | bitsfi 15788 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (bits‘𝑘)
∈ Fin) |
5 | | elfpw 8828 |
. . . . . . . 8
⊢
((bits‘𝑘)
∈ (𝒫 ℕ0 ∩ Fin) ↔ ((bits‘𝑘) ⊆ ℕ0
∧ (bits‘𝑘) ∈
Fin)) |
6 | 3, 4, 5 | sylanbrc 585 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (bits‘𝑘)
∈ (𝒫 ℕ0 ∩ Fin)) |
7 | 6 | adantl 484 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (bits‘𝑘) ∈ (𝒫 ℕ0 ∩
Fin)) |
8 | | elinel2 4175 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → 𝑥 ∈ Fin) |
9 | | 2nn0 11917 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
10 | 9 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑛 ∈ 𝑥) → 2 ∈
ℕ0) |
11 | | elfpw 8828 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ↔ (𝑥 ⊆ ℕ0 ∧ 𝑥 ∈ Fin)) |
12 | 11 | simplbi 500 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → 𝑥 ⊆
ℕ0) |
13 | 12 | sselda 3969 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑛 ∈ 𝑥) → 𝑛 ∈ ℕ0) |
14 | 10, 13 | nn0expcld 13610 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑛 ∈ 𝑥) → (2↑𝑛) ∈
ℕ0) |
15 | 8, 14 | fsumnn0cl 15095 |
. . . . . . 7
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → Σ𝑛 ∈ 𝑥 (2↑𝑛) ∈
ℕ0) |
16 | 15 | adantl 484 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (𝒫 ℕ0 ∩ Fin)) → Σ𝑛 ∈ 𝑥 (2↑𝑛) ∈
ℕ0) |
17 | | bitsinv2 15794 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → (bits‘Σ𝑛 ∈ 𝑥 (2↑𝑛)) = 𝑥) |
18 | 17 | eqcomd 2829 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → 𝑥 = (bits‘Σ𝑛 ∈ 𝑥 (2↑𝑛))) |
19 | 18 | ad2antll 727 |
. . . . . . . 8
⊢
((⊤ ∧ (𝑘
∈ ℕ0 ∧ 𝑥 ∈ (𝒫 ℕ0 ∩
Fin))) → 𝑥 =
(bits‘Σ𝑛 ∈
𝑥 (2↑𝑛))) |
20 | | fveq2 6672 |
. . . . . . . . 9
⊢ (𝑘 = Σ𝑛 ∈ 𝑥 (2↑𝑛) → (bits‘𝑘) = (bits‘Σ𝑛 ∈ 𝑥 (2↑𝑛))) |
21 | 20 | eqeq2d 2834 |
. . . . . . . 8
⊢ (𝑘 = Σ𝑛 ∈ 𝑥 (2↑𝑛) → (𝑥 = (bits‘𝑘) ↔ 𝑥 = (bits‘Σ𝑛 ∈ 𝑥 (2↑𝑛)))) |
22 | 19, 21 | syl5ibrcom 249 |
. . . . . . 7
⊢
((⊤ ∧ (𝑘
∈ ℕ0 ∧ 𝑥 ∈ (𝒫 ℕ0 ∩
Fin))) → (𝑘 =
Σ𝑛 ∈ 𝑥 (2↑𝑛) → 𝑥 = (bits‘𝑘))) |
23 | | bitsinv1 15793 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ Σ𝑛 ∈
(bits‘𝑘)(2↑𝑛) = 𝑘) |
24 | 23 | eqcomd 2829 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ 𝑘 = Σ𝑛 ∈ (bits‘𝑘)(2↑𝑛)) |
25 | 24 | ad2antrl 726 |
. . . . . . . 8
⊢
((⊤ ∧ (𝑘
∈ ℕ0 ∧ 𝑥 ∈ (𝒫 ℕ0 ∩
Fin))) → 𝑘 =
Σ𝑛 ∈
(bits‘𝑘)(2↑𝑛)) |
26 | | sumeq1 15047 |
. . . . . . . . 9
⊢ (𝑥 = (bits‘𝑘) → Σ𝑛 ∈ 𝑥 (2↑𝑛) = Σ𝑛 ∈ (bits‘𝑘)(2↑𝑛)) |
27 | 26 | eqeq2d 2834 |
. . . . . . . 8
⊢ (𝑥 = (bits‘𝑘) → (𝑘 = Σ𝑛 ∈ 𝑥 (2↑𝑛) ↔ 𝑘 = Σ𝑛 ∈ (bits‘𝑘)(2↑𝑛))) |
28 | 25, 27 | syl5ibrcom 249 |
. . . . . . 7
⊢
((⊤ ∧ (𝑘
∈ ℕ0 ∧ 𝑥 ∈ (𝒫 ℕ0 ∩
Fin))) → (𝑥 =
(bits‘𝑘) → 𝑘 = Σ𝑛 ∈ 𝑥 (2↑𝑛))) |
29 | 22, 28 | impbid 214 |
. . . . . 6
⊢
((⊤ ∧ (𝑘
∈ ℕ0 ∧ 𝑥 ∈ (𝒫 ℕ0 ∩
Fin))) → (𝑘 =
Σ𝑛 ∈ 𝑥 (2↑𝑛) ↔ 𝑥 = (bits‘𝑘))) |
30 | 1, 7, 16, 29 | f1ocnv2d 7400 |
. . . . 5
⊢ (⊤
→ ((𝑘 ∈
ℕ0 ↦ (bits‘𝑘)):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
∧ ◡(𝑘 ∈ ℕ0 ↦
(bits‘𝑘)) = (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 (2↑𝑛)))) |
31 | 30 | simpld 497 |
. . . 4
⊢ (⊤
→ (𝑘 ∈
ℕ0 ↦ (bits‘𝑘)):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin)) |
32 | | bitsf 15778 |
. . . . . . . . 9
⊢
bits:ℤ⟶𝒫 ℕ0 |
33 | 32 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ bits:ℤ⟶𝒫 ℕ0) |
34 | 33 | feqmptd 6735 |
. . . . . . 7
⊢ (⊤
→ bits = (𝑘 ∈
ℤ ↦ (bits‘𝑘))) |
35 | 34 | reseq1d 5854 |
. . . . . 6
⊢ (⊤
→ (bits ↾ ℕ0) = ((𝑘 ∈ ℤ ↦ (bits‘𝑘)) ↾
ℕ0)) |
36 | | nn0ssz 12006 |
. . . . . . 7
⊢
ℕ0 ⊆ ℤ |
37 | | resmpt 5907 |
. . . . . . 7
⊢
(ℕ0 ⊆ ℤ → ((𝑘 ∈ ℤ ↦ (bits‘𝑘)) ↾ ℕ0)
= (𝑘 ∈
ℕ0 ↦ (bits‘𝑘))) |
38 | 36, 37 | ax-mp 5 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ↦
(bits‘𝑘)) ↾
ℕ0) = (𝑘
∈ ℕ0 ↦ (bits‘𝑘)) |
39 | 35, 38 | syl6eq 2874 |
. . . . 5
⊢ (⊤
→ (bits ↾ ℕ0) = (𝑘 ∈ ℕ0 ↦
(bits‘𝑘))) |
40 | | f1oeq1 6606 |
. . . . 5
⊢ ((bits
↾ ℕ0) = (𝑘 ∈ ℕ0 ↦
(bits‘𝑘)) →
((bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
↔ (𝑘 ∈
ℕ0 ↦ (bits‘𝑘)):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin))) |
41 | 39, 40 | syl 17 |
. . . 4
⊢ (⊤
→ ((bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
↔ (𝑘 ∈
ℕ0 ↦ (bits‘𝑘)):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin))) |
42 | 31, 41 | mpbird 259 |
. . 3
⊢ (⊤
→ (bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin)) |
43 | 39 | cnveqd 5748 |
. . . 4
⊢ (⊤
→ ◡(bits ↾
ℕ0) = ◡(𝑘 ∈ ℕ0
↦ (bits‘𝑘))) |
44 | 30 | simprd 498 |
. . . 4
⊢ (⊤
→ ◡(𝑘 ∈ ℕ0 ↦
(bits‘𝑘)) = (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 (2↑𝑛))) |
45 | 43, 44 | eqtrd 2858 |
. . 3
⊢ (⊤
→ ◡(bits ↾
ℕ0) = (𝑥
∈ (𝒫 ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 (2↑𝑛))) |
46 | 42, 45 | jca 514 |
. 2
⊢ (⊤
→ ((bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
∧ ◡(bits ↾
ℕ0) = (𝑥
∈ (𝒫 ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 (2↑𝑛)))) |
47 | 46 | mptru 1544 |
1
⊢ ((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
∧ ◡(bits ↾
ℕ0) = (𝑥
∈ (𝒫 ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 (2↑𝑛))) |