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	$$⊢\mathrm{bits}:\mathbb{Z}⟶𝒫{\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		df-bits	$$⊢\mathrm{bits}=\left(n\in \mathbb{Z}⟼\left\{k\in {\mathbb{N}}_0|\neg 2\parallel ⌊\frac{n}{2^k}⌋\right\}\right)$$
2		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
3		ssrab2	$$⊢\left\{k\in {\mathbb{N}}_0|\neg 2\parallel ⌊\frac{n}{2^k}⌋\right\}\subseteq {\mathbb{N}}_0$$
4	2 3	elpwi2	$$⊢\left\{k\in {\mathbb{N}}_0|\neg 2\parallel ⌊\frac{n}{2^k}⌋\right\}\in 𝒫{\mathbb{N}}_0$$
5	4	a1i	$$⊢n\in \mathbb{Z}\to \left\{k\in {\mathbb{N}}_0|\neg 2\parallel ⌊\frac{n}{2^k}⌋\right\}\in 𝒫{\mathbb{N}}_0$$
6	1 5	fmpti	$$⊢\mathrm{bits}:\mathbb{Z}⟶𝒫{\mathbb{N}}_0$$