bitsf1ocnv

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	bitsf1ocnv	$⊢ (({bits ↾}_{ℕ_{0}}) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin \land {({bits ↾}_{ℕ_{0}})}^{-1} = (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in x} 2^{n}))$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ (k \in ℕ_{0} ⟼ bits (k)) = (k \in ℕ_{0} ⟼ bits (k))$
2		bitsss	$⊢ bits (k) \subseteq ℕ_{0}$
3	2	a1i	$⊢ k \in ℕ_{0} \to bits (k) \subseteq ℕ_{0}$
4		bitsfi	$⊢ k \in ℕ_{0} \to bits (k) \in Fin$
5		elfpw	$⊢ bits (k) \in (𝒫 ℕ_{0} \cap Fin) \leftrightarrow (bits (k) \subseteq ℕ_{0} \land bits (k) \in Fin)$
6	3 4 5	sylanbrc	$⊢ k \in ℕ_{0} \to bits (k) \in (𝒫 ℕ_{0} \cap Fin)$
7	6	adantl	$⊢ (⊤ \land k \in ℕ_{0}) \to bits (k) \in (𝒫 ℕ_{0} \cap Fin)$
8		elinel2	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to x \in Fin$
9		2nn0	$⊢ 2 \in ℕ_{0}$
10	9	a1i	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land n \in x) \to 2 \in ℕ_{0}$
11		elfpw	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \leftrightarrow (x \subseteq ℕ_{0} \land x \in Fin)$
12	11	simplbi	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to x \subseteq ℕ_{0}$
13	12	sselda	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land n \in x) \to n \in ℕ_{0}$
14	10 13	nn0expcld	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land n \in x) \to 2^{n} \in ℕ_{0}$
15	8 14	fsumnn0cl	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to \sum_{n \in x} 2^{n} \in ℕ_{0}$
16	15	adantl	$⊢ (⊤ \land x \in (𝒫 ℕ_{0} \cap Fin)) \to \sum_{n \in x} 2^{n} \in ℕ_{0}$
17		bitsinv2	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to bits (\sum_{n \in x} 2^{n}) = x$
18	17	eqcomd	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to x = bits (\sum_{n \in x} 2^{n})$
19	18	ad2antll	$⊢ (⊤ \land (k \in ℕ_{0} \land x \in (𝒫 ℕ_{0} \cap Fin))) \to x = bits (\sum_{n \in x} 2^{n})$
20		fveq2	$⊢ k = \sum_{n \in x} 2^{n} \to bits (k) = bits (\sum_{n \in x} 2^{n})$
21	20	eqeq2d	$⊢ k = \sum_{n \in x} 2^{n} \to (x = bits (k) \leftrightarrow x = bits (\sum_{n \in x} 2^{n}))$
22	19 21	syl5ibrcom	$⊢ (⊤ \land (k \in ℕ_{0} \land x \in (𝒫 ℕ_{0} \cap Fin))) \to (k = \sum_{n \in x} 2^{n} \to x = bits (k))$
23		bitsinv1	$⊢ k \in ℕ_{0} \to \sum_{n \in bits (k)} 2^{n} = k$
24	23	eqcomd	$⊢ k \in ℕ_{0} \to k = \sum_{n \in bits (k)} 2^{n}$
25	24	ad2antrl	$⊢ (⊤ \land (k \in ℕ_{0} \land x \in (𝒫 ℕ_{0} \cap Fin))) \to k = \sum_{n \in bits (k)} 2^{n}$
26		sumeq1	$⊢ x = bits (k) \to \sum_{n \in x} 2^{n} = \sum_{n \in bits (k)} 2^{n}$
27	26	eqeq2d	$⊢ x = bits (k) \to (k = \sum_{n \in x} 2^{n} \leftrightarrow k = \sum_{n \in bits (k)} 2^{n})$
28	25 27	syl5ibrcom	$⊢ (⊤ \land (k \in ℕ_{0} \land x \in (𝒫 ℕ_{0} \cap Fin))) \to (x = bits (k) \to k = \sum_{n \in x} 2^{n})$
29	22 28	impbid	$⊢ (⊤ \land (k \in ℕ_{0} \land x \in (𝒫 ℕ_{0} \cap Fin))) \to (k = \sum_{n \in x} 2^{n} \leftrightarrow x = bits (k))$
30	1 7 16 29	f1ocnv2d	$⊢ ⊤ \to ((k \in ℕ_{0} ⟼ bits (k)) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin \land {(k \in ℕ_{0} ⟼ bits (k))}^{-1} = (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in x} 2^{n}))$
31	30	simpld	$⊢ ⊤ \to (k \in ℕ_{0} ⟼ bits (k)) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin$
32		bitsf	$⊢ bits : ℤ ⟶ 𝒫 ℕ_{0}$
33	32	a1i	$⊢ ⊤ \to bits : ℤ ⟶ 𝒫 ℕ_{0}$
34	33	feqmptd	$⊢ ⊤ \to bits = (k \in ℤ ⟼ bits (k))$
35	34	reseq1d	$⊢ ⊤ \to {bits ↾}_{ℕ_{0}} = {(k \in ℤ ⟼ bits (k)) ↾}_{ℕ_{0}}$
36		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
37		resmpt	$⊢ ℕ_{0} \subseteq ℤ \to {(k \in ℤ ⟼ bits (k)) ↾}_{ℕ_{0}} = (k \in ℕ_{0} ⟼ bits (k))$
38	36 37	ax-mp	$⊢ {(k \in ℤ ⟼ bits (k)) ↾}_{ℕ_{0}} = (k \in ℕ_{0} ⟼ bits (k))$
39	35 38	syl6eq	$⊢ ⊤ \to {bits ↾}_{ℕ_{0}} = (k \in ℕ_{0} ⟼ bits (k))$
40		f1oeq1	$⊢ {bits ↾}_{ℕ_{0}} = (k \in ℕ_{0} ⟼ bits (k)) \to (({bits ↾}_{ℕ_{0}}) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin \leftrightarrow (k \in ℕ_{0} ⟼ bits (k)) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin)$
41	39 40	syl	$⊢ ⊤ \to (({bits ↾}_{ℕ_{0}}) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin \leftrightarrow (k \in ℕ_{0} ⟼ bits (k)) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin)$
42	31 41	mpbird	$⊢ ⊤ \to ({bits ↾}_{ℕ_{0}}) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin$
43	39	cnveqd	$⊢ ⊤ \to {({bits ↾}_{ℕ_{0}})}^{-1} = {(k \in ℕ_{0} ⟼ bits (k))}^{-1}$
44	30	simprd	$⊢ ⊤ \to {(k \in ℕ_{0} ⟼ bits (k))}^{-1} = (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in x} 2^{n})$
45	43 44	eqtrd	$⊢ ⊤ \to {({bits ↾}_{ℕ_{0}})}^{-1} = (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in x} 2^{n})$
46	42 45	jca	$⊢ ⊤ \to (({bits ↾}_{ℕ_{0}}) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin \land {({bits ↾}_{ℕ_{0}})}^{-1} = (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in x} 2^{n}))$
47	46	mptru	$⊢ (({bits ↾}_{ℕ_{0}}) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin \land {({bits ↾}_{ℕ_{0}})}^{-1} = (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{n \in x} 2^{n}))$

Metamath Proof Explorer

Theorem bitsf1ocnv

Proof