This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ 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→ ω