Theorem bitsinv

Description: The inverse of the bits function. (Contributed by Mario Carneiro, 8-Sep-2016)

	Ref	Expression
Hypothesis	bitsinv.k	$$⊢K={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}$$
Assertion	bitsinv	$$⊢A\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to K\left(A\right)=\sum _{k\in A}{2}^k$$

Proof

Step	Hyp	Ref	Expression
1		bitsinv.k	$$⊢K={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}$$
2		sumeq1	$$⊢x=A\to \sum _{k\in x}{2}^k=\sum _{k\in A}{2}^k$$
3		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 _{k\in x}{2}^k\right)\right)$$
4	3	simpri	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}=\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼\sum _{k\in x}{2}^k\right)$$
5	1 4	eqtri	$$⊢K=\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼\sum _{k\in x}{2}^k\right)$$
6		sumex	$$⊢\sum _{k\in A}{2}^k\in \mathrm{V}$$
7	2 5 6	fvmpt	$$⊢A\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to K\left(A\right)=\sum _{k\in A}{2}^k$$