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	$$⊢\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}𝒫{\mathbb{N}}_0\cap \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		bitsf1ocnv	$$⊢\left(\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\wedge {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}=\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼\sum _{n\in x}{2}^n\right)\right)$$
2	1	simpli	$$⊢\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}𝒫{\mathbb{N}}_0\cap \mathrm{Fin}$$