ackbij1

Description: The Ackermann bijection, part 1: each natural number can be uniquely coded in binary as a finite set of natural numbers and conversely. (Contributed by Stefan O'Rear, 18-Nov-2014)

		Ref	Expression
	Hypothesis	ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
	Assertion	ackbij1	$⊢ F : 𝒫 ω \cap Fin \underset{1-1 onto}{⟶} ω$

Proof

Step	Hyp	Ref	Expression
1		ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
2	1	ackbij1lem17	$⊢ F : 𝒫 ω \cap Fin \underset{1-1}{⟶} ω$
3		f1f	$⊢ F : 𝒫 ω \cap Fin \underset{1-1}{⟶} ω \to F : 𝒫 ω \cap Fin ⟶ ω$
4		frn	$⊢ F : 𝒫 ω \cap Fin ⟶ ω \to ran F \subseteq ω$
5	2 3 4	mp2b	$⊢ ran F \subseteq ω$
6		eleq1	$⊢ b = \emptyset \to (b \in ran F \leftrightarrow \emptyset \in ran F)$
7		eleq1	$⊢ b = a \to (b \in ran F \leftrightarrow a \in ran F)$
8		eleq1	$⊢ b = suc a \to (b \in ran F \leftrightarrow suc a \in ran F)$
9		peano1	$⊢ \emptyset \in ω$
10		ackbij1lem3	$⊢ \emptyset \in ω \to \emptyset \in (𝒫 ω \cap Fin)$
11	9 10	ax-mp	$⊢ \emptyset \in (𝒫 ω \cap Fin)$
12	1	ackbij1lem13	$⊢ F (\emptyset) = \emptyset$
13		fveqeq2	$⊢ a = \emptyset \to (F (a) = \emptyset \leftrightarrow F (\emptyset) = \emptyset)$
14	13	rspcev	$⊢ (\emptyset \in (𝒫 ω \cap Fin) \land F (\emptyset) = \emptyset) \to \exists a \in (𝒫 ω \cap Fin) F (a) = \emptyset$
15	11 12 14	mp2an	$⊢ \exists a \in (𝒫 ω \cap Fin) F (a) = \emptyset$
16		f1fn	$⊢ F : 𝒫 ω \cap Fin \underset{1-1}{⟶} ω \to F Fn (𝒫 ω \cap Fin)$
17	2 16	ax-mp	$⊢ F Fn (𝒫 ω \cap Fin)$
18		fvelrnb	$⊢ F Fn (𝒫 ω \cap Fin) \to (\emptyset \in ran F \leftrightarrow \exists a \in (𝒫 ω \cap Fin) F (a) = \emptyset)$
19	17 18	ax-mp	$⊢ \emptyset \in ran F \leftrightarrow \exists a \in (𝒫 ω \cap Fin) F (a) = \emptyset$
20	15 19	mpbir	$⊢ \emptyset \in ran F$
21	1	ackbij1lem18	$⊢ c \in (𝒫 ω \cap Fin) \to \exists b \in (𝒫 ω \cap Fin) F (b) = suc F (c)$
22	21	adantl	$⊢ (a \in ω \land c \in (𝒫 ω \cap Fin)) \to \exists b \in (𝒫 ω \cap Fin) F (b) = suc F (c)$
23		suceq	$⊢ F (c) = a \to suc F (c) = suc a$
24	23	eqeq2d	$⊢ F (c) = a \to (F (b) = suc F (c) \leftrightarrow F (b) = suc a)$
25	24	rexbidv	$⊢ F (c) = a \to (\exists b \in (𝒫 ω \cap Fin) F (b) = suc F (c) \leftrightarrow \exists b \in (𝒫 ω \cap Fin) F (b) = suc a)$
26	22 25	syl5ibcom	$⊢ (a \in ω \land c \in (𝒫 ω \cap Fin)) \to (F (c) = a \to \exists b \in (𝒫 ω \cap Fin) F (b) = suc a)$
27	26	rexlimdva	$⊢ a \in ω \to (\exists c \in (𝒫 ω \cap Fin) F (c) = a \to \exists b \in (𝒫 ω \cap Fin) F (b) = suc a)$
28		fvelrnb	$⊢ F Fn (𝒫 ω \cap Fin) \to (a \in ran F \leftrightarrow \exists c \in (𝒫 ω \cap Fin) F (c) = a)$
29	17 28	ax-mp	$⊢ a \in ran F \leftrightarrow \exists c \in (𝒫 ω \cap Fin) F (c) = a$
30		fvelrnb	$⊢ F Fn (𝒫 ω \cap Fin) \to (suc a \in ran F \leftrightarrow \exists b \in (𝒫 ω \cap Fin) F (b) = suc a)$
31	17 30	ax-mp	$⊢ suc a \in ran F \leftrightarrow \exists b \in (𝒫 ω \cap Fin) F (b) = suc a$
32	27 29 31	3imtr4g	$⊢ a \in ω \to (a \in ran F \to suc a \in ran F)$
33	6 7 8 7 20 32	finds	$⊢ a \in ω \to a \in ran F$
34	33	ssriv	$⊢ ω \subseteq ran F$
35	5 34	eqssi	$⊢ ran F = ω$
36		dff1o5	$⊢ F : 𝒫 ω \cap Fin \underset{1-1 onto}{⟶} ω \leftrightarrow (F : 𝒫 ω \cap Fin \underset{1-1}{⟶} ω \land ran F = ω)$
37	2 35 36	mpbir2an	$⊢ F : 𝒫 ω \cap Fin \underset{1-1 onto}{⟶} ω$

Metamath Proof Explorer

Theorem ackbij1

Proof