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 : ℤ ⟶ 𝒫 ℕ0

Proof

Step	Hyp	Ref	Expression
1		df-bits	⊢ bits = ( 𝑛 ∈ ℤ ↦ { 𝑘 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑛 / ( 2 ↑ 𝑘 ) ) ) } )
2		nn0ex	⊢ ℕ0 ∈ V
3		ssrab2	⊢ { 𝑘 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑛 / ( 2 ↑ 𝑘 ) ) ) } ⊆ ℕ0
4	2 3	elpwi2	⊢ { 𝑘 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑛 / ( 2 ↑ 𝑘 ) ) ) } ∈ 𝒫 ℕ0
5	4	a1i	⊢ ( 𝑛 ∈ ℤ → { 𝑘 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑛 / ( 2 ↑ 𝑘 ) ) ) } ∈ 𝒫 ℕ0 )
6	1 5	fmpti	⊢ bits : ℤ ⟶ 𝒫 ℕ0