Metamath Proof Explorer


Theorem bitsf1ocnv

Description: The bits function restricted to nonnegative integers is a bijection from the integers to the finite sets of integers. It is in fact the inverse of the Ackermann bijection ackbijnn . (Contributed by Mario Carneiro, 8-Sep-2016)

Ref Expression
Assertion bitsf1ocnv ( ( bits ↾ ℕ0 ) : ℕ01-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( bits ↾ ℕ0 ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) )
2 bitsss ( bits ‘ 𝑘 ) ⊆ ℕ0
3 2 a1i ( 𝑘 ∈ ℕ0 → ( bits ‘ 𝑘 ) ⊆ ℕ0 )
4 bitsfi ( 𝑘 ∈ ℕ0 → ( bits ‘ 𝑘 ) ∈ Fin )
5 elfpw ( ( bits ‘ 𝑘 ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( bits ‘ 𝑘 ) ⊆ ℕ0 ∧ ( bits ‘ 𝑘 ) ∈ Fin ) )
6 3 4 5 sylanbrc ( 𝑘 ∈ ℕ0 → ( bits ‘ 𝑘 ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
7 6 adantl ( ( ⊤ ∧ 𝑘 ∈ ℕ0 ) → ( bits ‘ 𝑘 ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
8 elinel2 ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → 𝑥 ∈ Fin )
9 2nn0 2 ∈ ℕ0
10 9 a1i ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑛𝑥 ) → 2 ∈ ℕ0 )
11 elfpw ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( 𝑥 ⊆ ℕ0𝑥 ∈ Fin ) )
12 11 simplbi ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → 𝑥 ⊆ ℕ0 )
13 12 sselda ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑛𝑥 ) → 𝑛 ∈ ℕ0 )
14 10 13 nn0expcld ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑛𝑥 ) → ( 2 ↑ 𝑛 ) ∈ ℕ0 )
15 8 14 fsumnn0cl ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) ∈ ℕ0 )
16 15 adantl ( ( ⊤ ∧ 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ) → Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) ∈ ℕ0 )
17 bitsinv2 ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( bits ‘ Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) ) = 𝑥 )
18 17 eqcomd ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → 𝑥 = ( bits ‘ Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) ) )
19 18 ad2antll ( ( ⊤ ∧ ( 𝑘 ∈ ℕ0𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ) ) → 𝑥 = ( bits ‘ Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) ) )
20 fveq2 ( 𝑘 = Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) → ( bits ‘ 𝑘 ) = ( bits ‘ Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) ) )
21 20 eqeq2d ( 𝑘 = Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) → ( 𝑥 = ( bits ‘ 𝑘 ) ↔ 𝑥 = ( bits ‘ Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) ) ) )
22 19 21 syl5ibrcom ( ( ⊤ ∧ ( 𝑘 ∈ ℕ0𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ) ) → ( 𝑘 = Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) → 𝑥 = ( bits ‘ 𝑘 ) ) )
23 bitsinv1 ( 𝑘 ∈ ℕ0 → Σ 𝑛 ∈ ( bits ‘ 𝑘 ) ( 2 ↑ 𝑛 ) = 𝑘 )
24 23 eqcomd ( 𝑘 ∈ ℕ0𝑘 = Σ 𝑛 ∈ ( bits ‘ 𝑘 ) ( 2 ↑ 𝑛 ) )
25 24 ad2antrl ( ( ⊤ ∧ ( 𝑘 ∈ ℕ0𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ) ) → 𝑘 = Σ 𝑛 ∈ ( bits ‘ 𝑘 ) ( 2 ↑ 𝑛 ) )
26 sumeq1 ( 𝑥 = ( bits ‘ 𝑘 ) → Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) = Σ 𝑛 ∈ ( bits ‘ 𝑘 ) ( 2 ↑ 𝑛 ) )
27 26 eqeq2d ( 𝑥 = ( bits ‘ 𝑘 ) → ( 𝑘 = Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) ↔ 𝑘 = Σ 𝑛 ∈ ( bits ‘ 𝑘 ) ( 2 ↑ 𝑛 ) ) )
28 25 27 syl5ibrcom ( ( ⊤ ∧ ( 𝑘 ∈ ℕ0𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ) ) → ( 𝑥 = ( bits ‘ 𝑘 ) → 𝑘 = Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) ) )
29 22 28 impbid ( ( ⊤ ∧ ( 𝑘 ∈ ℕ0𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ) ) → ( 𝑘 = Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) ↔ 𝑥 = ( bits ‘ 𝑘 ) ) )
30 1 7 16 29 f1ocnv2d ( ⊤ → ( ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) ) : ℕ01-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) ) ) )
31 30 simpld ( ⊤ → ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) ) : ℕ01-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) )
32 bitsf bits : ℤ ⟶ 𝒫 ℕ0
33 32 a1i ( ⊤ → bits : ℤ ⟶ 𝒫 ℕ0 )
34 33 feqmptd ( ⊤ → bits = ( 𝑘 ∈ ℤ ↦ ( bits ‘ 𝑘 ) ) )
35 34 reseq1d ( ⊤ → ( bits ↾ ℕ0 ) = ( ( 𝑘 ∈ ℤ ↦ ( bits ‘ 𝑘 ) ) ↾ ℕ0 ) )
36 nn0ssz 0 ⊆ ℤ
37 resmpt ( ℕ0 ⊆ ℤ → ( ( 𝑘 ∈ ℤ ↦ ( bits ‘ 𝑘 ) ) ↾ ℕ0 ) = ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) ) )
38 36 37 ax-mp ( ( 𝑘 ∈ ℤ ↦ ( bits ‘ 𝑘 ) ) ↾ ℕ0 ) = ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) )
39 35 38 syl6eq ( ⊤ → ( bits ↾ ℕ0 ) = ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) ) )
40 f1oeq1 ( ( bits ↾ ℕ0 ) = ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) ) → ( ( bits ↾ ℕ0 ) : ℕ01-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) ) : ℕ01-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ) )
41 39 40 syl ( ⊤ → ( ( bits ↾ ℕ0 ) : ℕ01-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) ) : ℕ01-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ) )
42 31 41 mpbird ( ⊤ → ( bits ↾ ℕ0 ) : ℕ01-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) )
43 39 cnveqd ( ⊤ → ( bits ↾ ℕ0 ) = ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) ) )
44 30 simprd ( ⊤ → ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) ) )
45 43 44 eqtrd ( ⊤ → ( bits ↾ ℕ0 ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) ) )
46 42 45 jca ( ⊤ → ( ( bits ↾ ℕ0 ) : ℕ01-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( bits ↾ ℕ0 ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) ) ) )
47 46 mptru ( ( bits ↾ ℕ0 ) : ℕ01-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( bits ↾ ℕ0 ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛𝑥 ( 2 ↑ 𝑛 ) ) )