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 ) : ℕ0 –1-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 ‘ 𝑘 ) ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ◡ ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑥 ( 2 ↑ 𝑛 ) ) ) )
31	30	simpld	⊢ ( ⊤ → ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) ) : ℕ0 –1-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	eqtrdi	⊢ ( ⊤ → ( bits ↾ ℕ0 ) = ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) ) )
40	39	f1oeq1d	⊢ ( ⊤ → ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ) )
41	31 40	mpbird	⊢ ( ⊤ → ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) )
42	39	cnveqd	⊢ ( ⊤ → ◡ ( bits ↾ ℕ0 ) = ◡ ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) ) )
43	30	simprd	⊢ ( ⊤ → ◡ ( 𝑘 ∈ ℕ0 ↦ ( bits ‘ 𝑘 ) ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑥 ( 2 ↑ 𝑛 ) ) )
44	42 43	eqtrd	⊢ ( ⊤ → ◡ ( bits ↾ ℕ0 ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑥 ( 2 ↑ 𝑛 ) ) )
45	41 44	jca	⊢ ( ⊤ → ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ◡ ( bits ↾ ℕ0 ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑥 ( 2 ↑ 𝑛 ) ) ) )
46	45	mptru	⊢ ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ◡ ( bits ↾ ℕ0 ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑥 ( 2 ↑ 𝑛 ) ) )