Theorem bitsinv

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

	Ref	Expression
Hypothesis	bitsinv.k	|- K = `' ( bits |` NN0 )
Assertion	bitsinv	|- ( A e. ( ~P NN0 i^i Fin ) -> ( K ` A ) = sum_ k e. A ( 2 ^ k ) )

Proof

Step	Hyp	Ref	Expression
1		bitsinv.k	|- K = `' ( bits |` NN0 )
2		sumeq1	|- ( x = A -> sum_ k e. x ( 2 ^ k ) = sum_ k e. A ( 2 ^ k ) )
3		bitsf1ocnv	|- ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) /\ `' ( bits |` NN0 ) = ( x e. ( ~P NN0 i^i Fin ) |-> sum_ k e. x ( 2 ^ k ) ) )
4	3	simpri	|- `' ( bits |` NN0 ) = ( x e. ( ~P NN0 i^i Fin ) |-> sum_ k e. x ( 2 ^ k ) )
5	1 4	eqtri	|- K = ( x e. ( ~P NN0 i^i Fin ) |-> sum_ k e. x ( 2 ^ k ) )
6		sumex	|- sum_ k e. A ( 2 ^ k ) e. _V
7	2 5 6	fvmpt	|- ( A e. ( ~P NN0 i^i Fin ) -> ( K ` A ) = sum_ k e. A ( 2 ^ k ) )