Theorem bitsf1o

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	bitsf1o	⊢ ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin )

Proof

Step	Hyp	Ref	Expression
1		bitsf1ocnv	⊢ ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ◡ ( bits ↾ ℕ0 ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑥 ( 2 ↑ 𝑛 ) ) )
2	1	simpli	⊢ ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin )