Theorem 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	⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
Assertion	ackbij1	⊢ 𝐹 : ( 𝒫 ω ∩ Fin ) –1-1-onto→ ω

Proof

Step	Hyp	Ref	Expression
1		ackbij.f	⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
2	1	ackbij1lem17	⊢ 𝐹 : ( 𝒫 ω ∩ Fin ) –1-1→ ω
3		f1f	⊢ ( 𝐹 : ( 𝒫 ω ∩ Fin ) –1-1→ ω → 𝐹 : ( 𝒫 ω ∩ Fin ) ⟶ ω )
4		frn	⊢ ( 𝐹 : ( 𝒫 ω ∩ Fin ) ⟶ ω → ran 𝐹 ⊆ ω )
5	2 3 4	mp2b	⊢ ran 𝐹 ⊆ ω
6		eleq1	⊢ ( 𝑏 = ∅ → ( 𝑏 ∈ ran 𝐹 ↔ ∅ ∈ ran 𝐹 ) )
7		eleq1	⊢ ( 𝑏 = 𝑎 → ( 𝑏 ∈ ran 𝐹 ↔ 𝑎 ∈ ran 𝐹 ) )
8		eleq1	⊢ ( 𝑏 = suc 𝑎 → ( 𝑏 ∈ ran 𝐹 ↔ suc 𝑎 ∈ ran 𝐹 ) )
9		peano1	⊢ ∅ ∈ ω
10		ackbij1lem3	⊢ ( ∅ ∈ ω → ∅ ∈ ( 𝒫 ω ∩ Fin ) )
11	9 10	ax-mp	⊢ ∅ ∈ ( 𝒫 ω ∩ Fin )
12	1	ackbij1lem13	⊢ ( 𝐹 ‘ ∅ ) = ∅
13		fveqeq2	⊢ ( 𝑎 = ∅ → ( ( 𝐹 ‘ 𝑎 ) = ∅ ↔ ( 𝐹 ‘ ∅ ) = ∅ ) )
14	13	rspcev	⊢ ( ( ∅ ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐹 ‘ ∅ ) = ∅ ) → ∃ 𝑎 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑎 ) = ∅ )
15	11 12 14	mp2an	⊢ ∃ 𝑎 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑎 ) = ∅
16		f1fn	⊢ ( 𝐹 : ( 𝒫 ω ∩ Fin ) –1-1→ ω → 𝐹 Fn ( 𝒫 ω ∩ Fin ) )
17	2 16	ax-mp	⊢ 𝐹 Fn ( 𝒫 ω ∩ Fin )
18		fvelrnb	⊢ ( 𝐹 Fn ( 𝒫 ω ∩ Fin ) → ( ∅ ∈ ran 𝐹 ↔ ∃ 𝑎 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑎 ) = ∅ ) )
19	17 18	ax-mp	⊢ ( ∅ ∈ ran 𝐹 ↔ ∃ 𝑎 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑎 ) = ∅ )
20	15 19	mpbir	⊢ ∅ ∈ ran 𝐹
21	1	ackbij1lem18	⊢ ( 𝑐 ∈ ( 𝒫 ω ∩ Fin ) → ∃ 𝑏 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑏 ) = suc ( 𝐹 ‘ 𝑐 ) )
22	21	adantl	⊢ ( ( 𝑎 ∈ ω ∧ 𝑐 ∈ ( 𝒫 ω ∩ Fin ) ) → ∃ 𝑏 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑏 ) = suc ( 𝐹 ‘ 𝑐 ) )
23		suceq	⊢ ( ( 𝐹 ‘ 𝑐 ) = 𝑎 → suc ( 𝐹 ‘ 𝑐 ) = suc 𝑎 )
24	23	eqeq2d	⊢ ( ( 𝐹 ‘ 𝑐 ) = 𝑎 → ( ( 𝐹 ‘ 𝑏 ) = suc ( 𝐹 ‘ 𝑐 ) ↔ ( 𝐹 ‘ 𝑏 ) = suc 𝑎 ) )
25	24	rexbidv	⊢ ( ( 𝐹 ‘ 𝑐 ) = 𝑎 → ( ∃ 𝑏 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑏 ) = suc ( 𝐹 ‘ 𝑐 ) ↔ ∃ 𝑏 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑏 ) = suc 𝑎 ) )
26	22 25	syl5ibcom	⊢ ( ( 𝑎 ∈ ω ∧ 𝑐 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ 𝑐 ) = 𝑎 → ∃ 𝑏 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑏 ) = suc 𝑎 ) )
27	26	rexlimdva	⊢ ( 𝑎 ∈ ω → ( ∃ 𝑐 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑐 ) = 𝑎 → ∃ 𝑏 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑏 ) = suc 𝑎 ) )
28		fvelrnb	⊢ ( 𝐹 Fn ( 𝒫 ω ∩ Fin ) → ( 𝑎 ∈ ran 𝐹 ↔ ∃ 𝑐 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑐 ) = 𝑎 ) )
29	17 28	ax-mp	⊢ ( 𝑎 ∈ ran 𝐹 ↔ ∃ 𝑐 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑐 ) = 𝑎 )
30		fvelrnb	⊢ ( 𝐹 Fn ( 𝒫 ω ∩ Fin ) → ( suc 𝑎 ∈ ran 𝐹 ↔ ∃ 𝑏 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑏 ) = suc 𝑎 ) )
31	17 30	ax-mp	⊢ ( suc 𝑎 ∈ ran 𝐹 ↔ ∃ 𝑏 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑏 ) = suc 𝑎 )
32	27 29 31	3imtr4g	⊢ ( 𝑎 ∈ ω → ( 𝑎 ∈ ran 𝐹 → suc 𝑎 ∈ ran 𝐹 ) )
33	6 7 8 7 20 32	finds	⊢ ( 𝑎 ∈ ω → 𝑎 ∈ ran 𝐹 )
34	33	ssriv	⊢ ω ⊆ ran 𝐹
35	5 34	eqssi	⊢ ran 𝐹 = ω
36		dff1o5	⊢ ( 𝐹 : ( 𝒫 ω ∩ Fin ) –1-1-onto→ ω ↔ ( 𝐹 : ( 𝒫 ω ∩ Fin ) –1-1→ ω ∧ ran 𝐹 = ω ) )
37	2 35 36	mpbir2an	⊢ 𝐹 : ( 𝒫 ω ∩ Fin ) –1-1-onto→ ω