Metamath Proof Explorer

Theorem ackbijnn

Description: Translate the Ackermann bijection ackbij1 onto the positive integers. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypothesis ackbijnn.1 ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 2 ↑ 𝑦 ) )
Assertion ackbijnn 𝐹 : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0

Proof

Step Hyp Ref Expression
1 ackbijnn.1 ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 2 ↑ 𝑦 ) )
2 hashgval2 ⊢ ( ♯ ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
3 2 hashgf1o ⊢ ( ♯ ↾ ω ) : ω –1-1-onto→ ℕ0
4 sneq ⊢ ( 𝑤 = 𝑦 → { 𝑤 } = { 𝑦 } )
5 pweq ⊢ ( 𝑤 = 𝑦 → 𝒫 𝑤 = 𝒫 𝑦 )
6 4 5 xpeq12d ⊢ ( 𝑤 = 𝑦 → ( { 𝑤 } × 𝒫 𝑤 ) = ( { 𝑦 } × 𝒫 𝑦 ) )
7 6 cbviunv ⊢ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) = ∪ 𝑦 ∈ 𝑧 ( { 𝑦 } × 𝒫 𝑦 )
8 iuneq1 ⊢ ( 𝑧 = 𝑥 → ∪ 𝑦 ∈ 𝑧 ( { 𝑦 } × 𝒫 𝑦 ) = ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) )
9 7 8 eqtrid ⊢ ( 𝑧 = 𝑥 → ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) = ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) )
10 9 fveq2d ⊢ ( 𝑧 = 𝑥 → ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) = ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
11 10 cbvmptv ⊢ ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
12 11 ackbij1 ⊢ ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) : ( 𝒫 ω ∩ Fin ) –1-1-onto→ ω
13 f1ocnv ⊢ ( ( ♯ ↾ ω ) : ω –1-1-onto→ ℕ0 → ◡ ( ♯ ↾ ω ) : ℕ0 –1-1-onto→ ω )
14 3 13 ax-mp ⊢ ◡ ( ♯ ↾ ω ) : ℕ0 –1-1-onto→ ω
15 f1opwfi ⊢ ( ◡ ( ♯ ↾ ω ) : ℕ0 –1-1-onto→ ω → ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ( 𝒫 ω ∩ Fin ) )
16 14 15 ax-mp ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ( 𝒫 ω ∩ Fin )
17 f1oco ⊢ ( ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) : ( 𝒫 ω ∩ Fin ) –1-1-onto→ ω ∧ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ∘ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ω )
18 12 16 17 mp2an ⊢ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ∘ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ω
19 f1oco ⊢ ( ( ( ♯ ↾ ω ) : ω –1-1-onto→ ℕ0 ∧ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ∘ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ω ) → ( ( ♯ ↾ ω ) ∘ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ∘ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) ) ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 )
20 3 18 19 mp2an ⊢ ( ( ♯ ↾ ω ) ∘ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ∘ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) ) ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0
21 inss2 ⊢ ( 𝒫 ω ∩ Fin ) ⊆ Fin
22 f1of ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ( 𝒫 ω ∩ Fin ) → ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ( 𝒫 ω ∩ Fin ) )
23 16 22 ax-mp ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ( 𝒫 ω ∩ Fin )
24 eqid ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) )
25 24 fmpt ⊢ ( ∀ 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ∈ ( 𝒫 ω ∩ Fin ) ↔ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ( 𝒫 ω ∩ Fin ) )
26 23 25 mpbir ⊢ ∀ 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ∈ ( 𝒫 ω ∩ Fin )
27 26 rspec ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ∈ ( 𝒫 ω ∩ Fin ) )
28 21 27 sselid ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ∈ Fin )
29 snfi ⊢ { 𝑤 } ∈ Fin
30 cnvimass ⊢ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ⊆ dom ( ♯ ↾ ω )
31 dmhashres ⊢ dom ( ♯ ↾ ω ) = ω
32 30 31 sseqtri ⊢ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ⊆ ω
33 onfin2 ⊢ ω = ( On ∩ Fin )
34 inss2 ⊢ ( On ∩ Fin ) ⊆ Fin
35 33 34 eqsstri ⊢ ω ⊆ Fin
36 32 35 sstri ⊢ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ⊆ Fin
37 simpr ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) → 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) )
38 36 37 sselid ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) → 𝑤 ∈ Fin )
39 pwfi ⊢ ( 𝑤 ∈ Fin ↔ 𝒫 𝑤 ∈ Fin )
40 38 39 sylib ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) → 𝒫 𝑤 ∈ Fin )
41 xpfi ⊢ ( ( { 𝑤 } ∈ Fin ∧ 𝒫 𝑤 ∈ Fin ) → ( { 𝑤 } × 𝒫 𝑤 ) ∈ Fin )
42 29 40 41 sylancr ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) → ( { 𝑤 } × 𝒫 𝑤 ) ∈ Fin )
43 42 ralrimiva ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ∀ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ∈ Fin )
44 iunfi ⊢ ( ( ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ∈ Fin ∧ ∀ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ∈ Fin ) → ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ∈ Fin )
45 28 43 44 syl2anc ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ∈ Fin )
46 ficardom ⊢ ( ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ∈ Fin → ( card ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) ∈ ω )
47 45 46 syl ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( card ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) ∈ ω )
48 47 fvresd ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ( ♯ ↾ ω ) ‘ ( card ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) ) = ( ♯ ‘ ( card ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) ) )
49 hashcard ⊢ ( ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ∈ Fin → ( ♯ ‘ ( card ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) ) = ( ♯ ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) )
50 45 49 syl ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ♯ ‘ ( card ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) ) = ( ♯ ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) )
51 xp1st ⊢ ( 𝑧 ∈ ( { 𝑤 } × 𝒫 𝑤 ) → ( 1st ‘ 𝑧 ) ∈ { 𝑤 } )
52 elsni ⊢ ( ( 1st ‘ 𝑧 ) ∈ { 𝑤 } → ( 1st ‘ 𝑧 ) = 𝑤 )
53 51 52 syl ⊢ ( 𝑧 ∈ ( { 𝑤 } × 𝒫 𝑤 ) → ( 1st ‘ 𝑧 ) = 𝑤 )
54 53 rgen ⊢ ∀ 𝑧 ∈ ( { 𝑤 } × 𝒫 𝑤 ) ( 1st ‘ 𝑧 ) = 𝑤
55 54 rgenw ⊢ ∀ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ∀ 𝑧 ∈ ( { 𝑤 } × 𝒫 𝑤 ) ( 1st ‘ 𝑧 ) = 𝑤
56 invdisj ⊢ ( ∀ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ∀ 𝑧 ∈ ( { 𝑤 } × 𝒫 𝑤 ) ( 1st ‘ 𝑧 ) = 𝑤 → Disj 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) )
57 55 56 mp1i ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → Disj 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) )
58 28 42 57 hashiun ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ♯ ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) = Σ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( ♯ ‘ ( { 𝑤 } × 𝒫 𝑤 ) ) )
59 sneq ⊢ ( 𝑤 = ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) → { 𝑤 } = { ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) } )
60 pweq ⊢ ( 𝑤 = ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) → 𝒫 𝑤 = 𝒫 ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) )
61 59 60 xpeq12d ⊢ ( 𝑤 = ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) → ( { 𝑤 } × 𝒫 𝑤 ) = ( { ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) } × 𝒫 ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) )
62 61 fveq2d ⊢ ( 𝑤 = ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) → ( ♯ ‘ ( { 𝑤 } × 𝒫 𝑤 ) ) = ( ♯ ‘ ( { ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) } × 𝒫 ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) ) )
63 elinel2 ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → 𝑥 ∈ Fin )
64 f1of1 ⊢ ( ◡ ( ♯ ↾ ω ) : ℕ0 –1-1-onto→ ω → ◡ ( ♯ ↾ ω ) : ℕ0 –1-1→ ω )
65 14 64 ax-mp ⊢ ◡ ( ♯ ↾ ω ) : ℕ0 –1-1→ ω
66 elinel1 ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → 𝑥 ∈ 𝒫 ℕ0 )
67 66 elpwid ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → 𝑥 ⊆ ℕ0 )
68 f1ores ⊢ ( ( ◡ ( ♯ ↾ ω ) : ℕ0 –1-1→ ω ∧ 𝑥 ⊆ ℕ0 ) → ( ◡ ( ♯ ↾ ω ) ↾ 𝑥 ) : 𝑥 –1-1-onto→ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) )
69 65 67 68 sylancr ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ◡ ( ♯ ↾ ω ) ↾ 𝑥 ) : 𝑥 –1-1-onto→ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) )
70 fvres ⊢ ( 𝑦 ∈ 𝑥 → ( ( ◡ ( ♯ ↾ ω ) ↾ 𝑥 ) ‘ 𝑦 ) = ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) )
71 70 adantl ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( ( ◡ ( ♯ ↾ ω ) ↾ 𝑥 ) ‘ 𝑦 ) = ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) )
72 hashcl ⊢ ( ( { 𝑤 } × 𝒫 𝑤 ) ∈ Fin → ( ♯ ‘ ( { 𝑤 } × 𝒫 𝑤 ) ) ∈ ℕ0 )
73 nn0cn ⊢ ( ( ♯ ‘ ( { 𝑤 } × 𝒫 𝑤 ) ) ∈ ℕ0 → ( ♯ ‘ ( { 𝑤 } × 𝒫 𝑤 ) ) ∈ ℂ )
74 42 72 73 3syl ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) → ( ♯ ‘ ( { 𝑤 } × 𝒫 𝑤 ) ) ∈ ℂ )
75 62 63 69 71 74 fsumf1o ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → Σ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( ♯ ‘ ( { 𝑤 } × 𝒫 𝑤 ) ) = Σ 𝑦 ∈ 𝑥 ( ♯ ‘ ( { ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) } × 𝒫 ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) ) )
76 snfi ⊢ { ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) } ∈ Fin
77 67 sselda ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ ℕ0 )
78 f1of ⊢ ( ◡ ( ♯ ↾ ω ) : ℕ0 –1-1-onto→ ω → ◡ ( ♯ ↾ ω ) : ℕ0 ⟶ ω )
79 14 78 ax-mp ⊢ ◡ ( ♯ ↾ ω ) : ℕ0 ⟶ ω
80 79 ffvelcdmi ⊢ ( 𝑦 ∈ ℕ0 → ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ∈ ω )
81 77 80 syl ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ∈ ω )
82 35 81 sselid ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ∈ Fin )
83 pwfi ⊢ ( ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ∈ Fin ↔ 𝒫 ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ∈ Fin )
84 82 83 sylib ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝒫 ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ∈ Fin )
85 hashxp ⊢ ( ( { ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) } ∈ Fin ∧ 𝒫 ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ∈ Fin ) → ( ♯ ‘ ( { ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) } × 𝒫 ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) ) = ( ( ♯ ‘ { ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) } ) · ( ♯ ‘ 𝒫 ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) ) )
86 76 84 85 sylancr ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( ♯ ‘ ( { ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) } × 𝒫 ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) ) = ( ( ♯ ‘ { ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) } ) · ( ♯ ‘ 𝒫 ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) ) )
87 hashsng ⊢ ( ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ∈ ω → ( ♯ ‘ { ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) } ) = 1 )
88 81 87 syl ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( ♯ ‘ { ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) } ) = 1 )
89 hashpw ⊢ ( ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ∈ Fin → ( ♯ ‘ 𝒫 ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) = ( 2 ↑ ( ♯ ‘ ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) ) )
90 82 89 syl ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( ♯ ‘ 𝒫 ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) = ( 2 ↑ ( ♯ ‘ ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) ) )
91 81 fvresd ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( ( ♯ ↾ ω ) ‘ ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) = ( ♯ ‘ ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) )
92 f1ocnvfv2 ⊢ ( ( ( ♯ ↾ ω ) : ω –1-1-onto→ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( ( ♯ ↾ ω ) ‘ ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) = 𝑦 )
93 3 77 92 sylancr ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( ( ♯ ↾ ω ) ‘ ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) = 𝑦 )
94 91 93 eqtr3d ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( ♯ ‘ ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) = 𝑦 )
95 94 oveq2d ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( 2 ↑ ( ♯ ‘ ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) ) = ( 2 ↑ 𝑦 ) )
96 90 95 eqtrd ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( ♯ ‘ 𝒫 ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) = ( 2 ↑ 𝑦 ) )
97 88 96 oveq12d ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( ( ♯ ‘ { ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) } ) · ( ♯ ‘ 𝒫 ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) ) = ( 1 · ( 2 ↑ 𝑦 ) ) )
98 2cn ⊢ 2 ∈ ℂ
99 expcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑦 ∈ ℕ0 ) → ( 2 ↑ 𝑦 ) ∈ ℂ )
100 98 77 99 sylancr ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( 2 ↑ 𝑦 ) ∈ ℂ )
101 100 mullidd ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( 1 · ( 2 ↑ 𝑦 ) ) = ( 2 ↑ 𝑦 ) )
102 86 97 101 3eqtrd ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( ♯ ‘ ( { ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) } × 𝒫 ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) ) = ( 2 ↑ 𝑦 ) )
103 102 sumeq2dv ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → Σ 𝑦 ∈ 𝑥 ( ♯ ‘ ( { ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) } × 𝒫 ( ◡ ( ♯ ↾ ω ) ‘ 𝑦 ) ) ) = Σ 𝑦 ∈ 𝑥 ( 2 ↑ 𝑦 ) )
104 58 75 103 3eqtrd ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ♯ ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) = Σ 𝑦 ∈ 𝑥 ( 2 ↑ 𝑦 ) )
105 48 50 104 3eqtrd ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ( ♯ ↾ ω ) ‘ ( card ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) ) = Σ 𝑦 ∈ 𝑥 ( 2 ↑ 𝑦 ) )
106 105 mpteq2ia ⊢ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ( ♯ ↾ ω ) ‘ ( card ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) ) ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 2 ↑ 𝑦 ) )
107 47 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ) → ( card ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) ∈ ω )
108 27 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ) → ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ∈ ( 𝒫 ω ∩ Fin ) )
109 eqidd ⊢ ( ⊤ → ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) )
110 eqidd ⊢ ( ⊤ → ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) = ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) )
111 iuneq1 ⊢ ( 𝑧 = ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) → ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) = ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) )
112 111 fveq2d ⊢ ( 𝑧 = ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) → ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) = ( card ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) )
113 108 109 110 112 fmptco ⊢ ( ⊤ → ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ∘ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) ) )
114 f1of ⊢ ( ( ♯ ↾ ω ) : ω –1-1-onto→ ℕ0 → ( ♯ ↾ ω ) : ω ⟶ ℕ0 )
115 3 114 mp1i ⊢ ( ⊤ → ( ♯ ↾ ω ) : ω ⟶ ℕ0 )
116 115 feqmptd ⊢ ( ⊤ → ( ♯ ↾ ω ) = ( 𝑦 ∈ ω ↦ ( ( ♯ ↾ ω ) ‘ 𝑦 ) ) )
117 fveq2 ⊢ ( 𝑦 = ( card ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) → ( ( ♯ ↾ ω ) ‘ 𝑦 ) = ( ( ♯ ↾ ω ) ‘ ( card ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) ) )
118 107 113 116 117 fmptco ⊢ ( ⊤ → ( ( ♯ ↾ ω ) ∘ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ∘ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ( ♯ ↾ ω ) ‘ ( card ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) ) ) )
119 118 mptru ⊢ ( ( ♯ ↾ ω ) ∘ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ∘ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ( ♯ ↾ ω ) ‘ ( card ‘ ∪ 𝑤 ∈ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ( { 𝑤 } × 𝒫 𝑤 ) ) ) )
120 106 119 1 3eqtr4i ⊢ ( ( ♯ ↾ ω ) ∘ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ∘ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) ) ) = 𝐹
121 f1oeq1 ⊢ ( ( ( ♯ ↾ ω ) ∘ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ∘ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) ) ) = 𝐹 → ( ( ( ♯ ↾ ω ) ∘ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ∘ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) ) ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 ↔ 𝐹 : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 ) )
122 120 121 ax-mp ⊢ ( ( ( ♯ ↾ ω ) ∘ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ∘ ( 𝑥 ∈ ( 𝒫 ℕ0 ∩ Fin ) ↦ ( ◡ ( ♯ ↾ ω ) “ 𝑥 ) ) ) ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 ↔ 𝐹 : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 )
123 20 122 mpbi ⊢ 𝐹 : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0