Metamath Proof Explorer

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 ⊢ F = x ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ y ∈ x y × 𝒫 y
Assertion ackbij1 ⊢ F : 𝒫 ω ∩ Fin ⟶ 1-1 onto ω

Proof

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