Theorem bitsf

Description: The bits function is a function from integers to subsets of nonnegative integers. (Contributed by Mario Carneiro, 5-Sep-2016)

	Ref	Expression
Assertion	bitsf	|- bits : ZZ --> ~P NN0

Proof

Step	Hyp	Ref	Expression
1		df-bits	|- bits = ( n e. ZZ |-> { k e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ k ) ) ) } )
2		nn0ex	|- NN0 e. _V
3		ssrab2	|- { k e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ k ) ) ) } C_ NN0
4	2 3	elpwi2	|- { k e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ k ) ) ) } e. ~P NN0
5	4	a1i	|- ( n e. ZZ -> { k e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ k ) ) ) } e. ~P NN0 )
6	1 5	fmpti	|- bits : ZZ --> ~P NN0