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 |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )

Proof

Step	Hyp	Ref	Expression
1		bitsf1ocnv	|- ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) /\ `' ( bits |` NN0 ) = ( x e. ( ~P NN0 i^i Fin ) |-> sum_ n e. x ( 2 ^ n ) ) )
2	1	simpli	|- ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )