Metamath Proof Explorer


Theorem eulerpartgbij

Description: Lemma for eulerpart : The G function is a bijection. (Contributed by Thierry Arnoux, 27-Aug-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypotheses eulerpart.p 𝑃 = { 𝑓 ∈ ( ℕ0m ℕ ) ∣ ( ( 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓𝑘 ) · 𝑘 ) = 𝑁 ) }
eulerpart.o 𝑂 = { 𝑔𝑃 ∣ ∀ 𝑛 ∈ ( 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 }
eulerpart.d 𝐷 = { 𝑔𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔𝑛 ) ≤ 1 }
eulerpart.j 𝐽 = { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 }
eulerpart.f 𝐹 = ( 𝑥𝐽 , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
eulerpart.h 𝐻 = { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin }
eulerpart.m 𝑀 = ( 𝑟𝐻 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐽𝑦 ∈ ( 𝑟𝑥 ) ) } )
eulerpart.r 𝑅 = { 𝑓 ∣ ( 𝑓 “ ℕ ) ∈ Fin }
eulerpart.t 𝑇 = { 𝑓 ∈ ( ℕ0m ℕ ) ∣ ( 𝑓 “ ℕ ) ⊆ 𝐽 }
eulerpart.g 𝐺 = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) )
Assertion eulerpartgbij 𝐺 : ( 𝑇𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 )

Proof

Step Hyp Ref Expression
1 eulerpart.p 𝑃 = { 𝑓 ∈ ( ℕ0m ℕ ) ∣ ( ( 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓𝑘 ) · 𝑘 ) = 𝑁 ) }
2 eulerpart.o 𝑂 = { 𝑔𝑃 ∣ ∀ 𝑛 ∈ ( 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 }
3 eulerpart.d 𝐷 = { 𝑔𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔𝑛 ) ≤ 1 }
4 eulerpart.j 𝐽 = { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 }
5 eulerpart.f 𝐹 = ( 𝑥𝐽 , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
6 eulerpart.h 𝐻 = { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin }
7 eulerpart.m 𝑀 = ( 𝑟𝐻 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐽𝑦 ∈ ( 𝑟𝑥 ) ) } )
8 eulerpart.r 𝑅 = { 𝑓 ∣ ( 𝑓 “ ℕ ) ∈ Fin }
9 eulerpart.t 𝑇 = { 𝑓 ∈ ( ℕ0m ℕ ) ∣ ( 𝑓 “ ℕ ) ⊆ 𝐽 }
10 eulerpart.g 𝐺 = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) )
11 nnex ℕ ∈ V
12 indf1ofs ( ℕ ∈ V → ( ( 𝟭 ‘ ℕ ) ↾ Fin ) : ( 𝒫 ℕ ∩ Fin ) –1-1-onto→ { 𝑓 ∈ ( { 0 , 1 } ↑m ℕ ) ∣ ( 𝑓 “ { 1 } ) ∈ Fin } )
13 11 12 ax-mp ( ( 𝟭 ‘ ℕ ) ↾ Fin ) : ( 𝒫 ℕ ∩ Fin ) –1-1-onto→ { 𝑓 ∈ ( { 0 , 1 } ↑m ℕ ) ∣ ( 𝑓 “ { 1 } ) ∈ Fin }
14 incom ( ( { 0 , 1 } ↑m ℕ ) ∩ { 𝑓 ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) = ( { 𝑓 ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∩ ( { 0 , 1 } ↑m ℕ ) )
15 8 ineq2i ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) = ( ( { 0 , 1 } ↑m ℕ ) ∩ { 𝑓 ∣ ( 𝑓 “ ℕ ) ∈ Fin } )
16 dfrab2 { 𝑓 ∈ ( { 0 , 1 } ↑m ℕ ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } = ( { 𝑓 ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∩ ( { 0 , 1 } ↑m ℕ ) )
17 14 15 16 3eqtr4i ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) = { 𝑓 ∈ ( { 0 , 1 } ↑m ℕ ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
18 elmapfun ( 𝑓 ∈ ( { 0 , 1 } ↑m ℕ ) → Fun 𝑓 )
19 elmapi ( 𝑓 ∈ ( { 0 , 1 } ↑m ℕ ) → 𝑓 : ℕ ⟶ { 0 , 1 } )
20 19 frnd ( 𝑓 ∈ ( { 0 , 1 } ↑m ℕ ) → ran 𝑓 ⊆ { 0 , 1 } )
21 fimacnvinrn2 ( ( Fun 𝑓 ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ( 𝑓 “ ℕ ) = ( 𝑓 “ ( ℕ ∩ { 0 , 1 } ) ) )
22 df-pr { 0 , 1 } = ( { 0 } ∪ { 1 } )
23 22 ineq2i ( ℕ ∩ { 0 , 1 } ) = ( ℕ ∩ ( { 0 } ∪ { 1 } ) )
24 indi ( ℕ ∩ ( { 0 } ∪ { 1 } ) ) = ( ( ℕ ∩ { 0 } ) ∪ ( ℕ ∩ { 1 } ) )
25 0nnn ¬ 0 ∈ ℕ
26 disjsn ( ( ℕ ∩ { 0 } ) = ∅ ↔ ¬ 0 ∈ ℕ )
27 25 26 mpbir ( ℕ ∩ { 0 } ) = ∅
28 1nn 1 ∈ ℕ
29 1ex 1 ∈ V
30 29 snss ( 1 ∈ ℕ ↔ { 1 } ⊆ ℕ )
31 28 30 mpbi { 1 } ⊆ ℕ
32 dfss ( { 1 } ⊆ ℕ ↔ { 1 } = ( { 1 } ∩ ℕ ) )
33 31 32 mpbi { 1 } = ( { 1 } ∩ ℕ )
34 incom ( { 1 } ∩ ℕ ) = ( ℕ ∩ { 1 } )
35 33 34 eqtr2i ( ℕ ∩ { 1 } ) = { 1 }
36 27 35 uneq12i ( ( ℕ ∩ { 0 } ) ∪ ( ℕ ∩ { 1 } ) ) = ( ∅ ∪ { 1 } )
37 23 24 36 3eqtri ( ℕ ∩ { 0 , 1 } ) = ( ∅ ∪ { 1 } )
38 uncom ( ∅ ∪ { 1 } ) = ( { 1 } ∪ ∅ )
39 un0 ( { 1 } ∪ ∅ ) = { 1 }
40 37 38 39 3eqtri ( ℕ ∩ { 0 , 1 } ) = { 1 }
41 40 imaeq2i ( 𝑓 “ ( ℕ ∩ { 0 , 1 } ) ) = ( 𝑓 “ { 1 } )
42 21 41 eqtrdi ( ( Fun 𝑓 ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ( 𝑓 “ ℕ ) = ( 𝑓 “ { 1 } ) )
43 18 20 42 syl2anc ( 𝑓 ∈ ( { 0 , 1 } ↑m ℕ ) → ( 𝑓 “ ℕ ) = ( 𝑓 “ { 1 } ) )
44 43 eleq1d ( 𝑓 ∈ ( { 0 , 1 } ↑m ℕ ) → ( ( 𝑓 “ ℕ ) ∈ Fin ↔ ( 𝑓 “ { 1 } ) ∈ Fin ) )
45 44 rabbiia { 𝑓 ∈ ( { 0 , 1 } ↑m ℕ ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( { 0 , 1 } ↑m ℕ ) ∣ ( 𝑓 “ { 1 } ) ∈ Fin }
46 17 45 eqtr2i { 𝑓 ∈ ( { 0 , 1 } ↑m ℕ ) ∣ ( 𝑓 “ { 1 } ) ∈ Fin } = ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 )
47 f1oeq3 ( { 𝑓 ∈ ( { 0 , 1 } ↑m ℕ ) ∣ ( 𝑓 “ { 1 } ) ∈ Fin } = ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) → ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) : ( 𝒫 ℕ ∩ Fin ) –1-1-onto→ { 𝑓 ∈ ( { 0 , 1 } ↑m ℕ ) ∣ ( 𝑓 “ { 1 } ) ∈ Fin } ↔ ( ( 𝟭 ‘ ℕ ) ↾ Fin ) : ( 𝒫 ℕ ∩ Fin ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ) )
48 46 47 ax-mp ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) : ( 𝒫 ℕ ∩ Fin ) –1-1-onto→ { 𝑓 ∈ ( { 0 , 1 } ↑m ℕ ) ∣ ( 𝑓 “ { 1 } ) ∈ Fin } ↔ ( ( 𝟭 ‘ ℕ ) ↾ Fin ) : ( 𝒫 ℕ ∩ Fin ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) )
49 13 48 mpbi ( ( 𝟭 ‘ ℕ ) ↾ Fin ) : ( 𝒫 ℕ ∩ Fin ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 )
50 4 5 oddpwdc 𝐹 : ( 𝐽 × ℕ0 ) –1-1-onto→ ℕ
51 f1opwfi ( 𝐹 : ( 𝐽 × ℕ0 ) –1-1-onto→ ℕ → ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹𝑎 ) ) : ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin ) )
52 50 51 ax-mp ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹𝑎 ) ) : ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin )
53 1 2 3 4 5 6 7 eulerpartlem1 𝑀 : 𝐻1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin )
54 bitsf1o ( bits ↾ ℕ0 ) : ℕ01-1-onto→ ( 𝒫 ℕ0 ∩ Fin )
55 54 a1i ( ⊤ → ( bits ↾ ℕ0 ) : ℕ01-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) )
56 4 11 rabex2 𝐽 ∈ V
57 56 a1i ( ⊤ → 𝐽 ∈ V )
58 nn0ex 0 ∈ V
59 58 a1i ( ⊤ → ℕ0 ∈ V )
60 58 pwex 𝒫 ℕ0 ∈ V
61 60 inex1 ( 𝒫 ℕ0 ∩ Fin ) ∈ V
62 61 a1i ( ⊤ → ( 𝒫 ℕ0 ∩ Fin ) ∈ V )
63 0nn0 0 ∈ ℕ0
64 63 a1i ( ⊤ → 0 ∈ ℕ0 )
65 fvres ( 0 ∈ ℕ0 → ( ( bits ↾ ℕ0 ) ‘ 0 ) = ( bits ‘ 0 ) )
66 63 65 ax-mp ( ( bits ↾ ℕ0 ) ‘ 0 ) = ( bits ‘ 0 )
67 0bits ( bits ‘ 0 ) = ∅
68 66 67 eqtr2i ∅ = ( ( bits ↾ ℕ0 ) ‘ 0 )
69 elmapi ( 𝑓 ∈ ( ℕ0m 𝐽 ) → 𝑓 : 𝐽 ⟶ ℕ0 )
70 fcdmnn0supp ( ( 𝐽 ∈ V ∧ 𝑓 : 𝐽 ⟶ ℕ0 ) → ( 𝑓 supp 0 ) = ( 𝑓 “ ℕ ) )
71 56 69 70 sylancr ( 𝑓 ∈ ( ℕ0m 𝐽 ) → ( 𝑓 supp 0 ) = ( 𝑓 “ ℕ ) )
72 71 eleq1d ( 𝑓 ∈ ( ℕ0m 𝐽 ) → ( ( 𝑓 supp 0 ) ∈ Fin ↔ ( 𝑓 “ ℕ ) ∈ Fin ) )
73 72 rabbiia { 𝑓 ∈ ( ℕ0m 𝐽 ) ∣ ( 𝑓 supp 0 ) ∈ Fin } = { 𝑓 ∈ ( ℕ0m 𝐽 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
74 elmapfun ( 𝑓 ∈ ( ℕ0m 𝐽 ) → Fun 𝑓 )
75 vex 𝑓 ∈ V
76 funisfsupp ( ( Fun 𝑓𝑓 ∈ V ∧ 0 ∈ ℕ0 ) → ( 𝑓 finSupp 0 ↔ ( 𝑓 supp 0 ) ∈ Fin ) )
77 75 63 76 mp3an23 ( Fun 𝑓 → ( 𝑓 finSupp 0 ↔ ( 𝑓 supp 0 ) ∈ Fin ) )
78 74 77 syl ( 𝑓 ∈ ( ℕ0m 𝐽 ) → ( 𝑓 finSupp 0 ↔ ( 𝑓 supp 0 ) ∈ Fin ) )
79 78 rabbiia { 𝑓 ∈ ( ℕ0m 𝐽 ) ∣ 𝑓 finSupp 0 } = { 𝑓 ∈ ( ℕ0m 𝐽 ) ∣ ( 𝑓 supp 0 ) ∈ Fin }
80 incom ( { 𝑓 ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∩ ( ℕ0m 𝐽 ) ) = ( ( ℕ0m 𝐽 ) ∩ { 𝑓 ∣ ( 𝑓 “ ℕ ) ∈ Fin } )
81 dfrab2 { 𝑓 ∈ ( ℕ0m 𝐽 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } = ( { 𝑓 ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∩ ( ℕ0m 𝐽 ) )
82 8 ineq2i ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) = ( ( ℕ0m 𝐽 ) ∩ { 𝑓 ∣ ( 𝑓 “ ℕ ) ∈ Fin } )
83 80 81 82 3eqtr4ri ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) = { 𝑓 ∈ ( ℕ0m 𝐽 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
84 73 79 83 3eqtr4ri ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) = { 𝑓 ∈ ( ℕ0m 𝐽 ) ∣ 𝑓 finSupp 0 }
85 elmapfun ( 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) → Fun 𝑟 )
86 vex 𝑟 ∈ V
87 0ex ∅ ∈ V
88 funisfsupp ( ( Fun 𝑟𝑟 ∈ V ∧ ∅ ∈ V ) → ( 𝑟 finSupp ∅ ↔ ( 𝑟 supp ∅ ) ∈ Fin ) )
89 86 87 88 mp3an23 ( Fun 𝑟 → ( 𝑟 finSupp ∅ ↔ ( 𝑟 supp ∅ ) ∈ Fin ) )
90 89 bicomd ( Fun 𝑟 → ( ( 𝑟 supp ∅ ) ∈ Fin ↔ 𝑟 finSupp ∅ ) )
91 85 90 syl ( 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) → ( ( 𝑟 supp ∅ ) ∈ Fin ↔ 𝑟 finSupp ∅ ) )
92 91 rabbiia { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } = { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ 𝑟 finSupp ∅ }
93 55 57 59 62 64 68 84 92 fcobijfs ( ⊤ → ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) ) : ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } )
94 elinel1 ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) → 𝑓 ∈ ( ℕ0m 𝐽 ) )
95 frn ( 𝑓 : 𝐽 ⟶ ℕ0 → ran 𝑓 ⊆ ℕ0 )
96 cores ( ran 𝑓 ⊆ ℕ0 → ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) = ( bits ∘ 𝑓 ) )
97 94 69 95 96 4syl ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) → ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) = ( bits ∘ 𝑓 ) )
98 97 mpteq2ia ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) ) = ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) )
99 98 eqcomi ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) = ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) )
100 f1oeq1 ( ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) = ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) ) → ( ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) : ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↔ ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) ) : ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ) )
101 99 100 mp1i ( ⊤ → ( ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) : ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↔ ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) ) : ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ) )
102 93 101 mpbird ( ⊤ → ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) : ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } )
103 102 mptru ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) : ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin }
104 ssrab2 { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ⊆ ℕ
105 4 104 eqsstri 𝐽 ⊆ ℕ
106 11 58 105 3pm3.2i ( ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ )
107 cnveq ( 𝑓 = 𝑜 𝑓 = 𝑜 )
108 dfn2 ℕ = ( ℕ0 ∖ { 0 } )
109 108 a1i ( 𝑓 = 𝑜 → ℕ = ( ℕ0 ∖ { 0 } ) )
110 107 109 imaeq12d ( 𝑓 = 𝑜 → ( 𝑓 “ ℕ ) = ( 𝑜 “ ( ℕ0 ∖ { 0 } ) ) )
111 110 sseq1d ( 𝑓 = 𝑜 → ( ( 𝑓 “ ℕ ) ⊆ 𝐽 ↔ ( 𝑜 “ ( ℕ0 ∖ { 0 } ) ) ⊆ 𝐽 ) )
112 111 cbvrabv { 𝑓 ∈ ( ℕ0m ℕ ) ∣ ( 𝑓 “ ℕ ) ⊆ 𝐽 } = { 𝑜 ∈ ( ℕ0m ℕ ) ∣ ( 𝑜 “ ( ℕ0 ∖ { 0 } ) ) ⊆ 𝐽 }
113 9 112 eqtri 𝑇 = { 𝑜 ∈ ( ℕ0m ℕ ) ∣ ( 𝑜 “ ( ℕ0 ∖ { 0 } ) ) ⊆ 𝐽 }
114 eqid ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) = ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) )
115 113 114 resf1o ( ( ( ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ ) ∧ 0 ∈ ℕ0 ) → ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) : 𝑇1-1-onto→ ( ℕ0m 𝐽 ) )
116 106 63 115 mp2an ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) : 𝑇1-1-onto→ ( ℕ0m 𝐽 )
117 f1of1 ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) : 𝑇1-1-onto→ ( ℕ0m 𝐽 ) → ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) : 𝑇1-1→ ( ℕ0m 𝐽 ) )
118 116 117 ax-mp ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) : 𝑇1-1→ ( ℕ0m 𝐽 )
119 inss1 ( 𝑇𝑅 ) ⊆ 𝑇
120 f1ores ( ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) : 𝑇1-1→ ( ℕ0m 𝐽 ) ∧ ( 𝑇𝑅 ) ⊆ 𝑇 ) → ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ↾ ( 𝑇𝑅 ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) “ ( 𝑇𝑅 ) ) )
121 118 119 120 mp2an ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ↾ ( 𝑇𝑅 ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) “ ( 𝑇𝑅 ) )
122 vex 𝑜 ∈ V
123 122 resex ( 𝑜𝐽 ) ∈ V
124 123 114 fnmpti ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) Fn 𝑇
125 fvelimab ( ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) Fn 𝑇 ∧ ( 𝑇𝑅 ) ⊆ 𝑇 ) → ( 𝑓 ∈ ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) “ ( 𝑇𝑅 ) ) ↔ ∃ 𝑚 ∈ ( 𝑇𝑅 ) ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ‘ 𝑚 ) = 𝑓 ) )
126 124 119 125 mp2an ( 𝑓 ∈ ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) “ ( 𝑇𝑅 ) ) ↔ ∃ 𝑚 ∈ ( 𝑇𝑅 ) ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ‘ 𝑚 ) = 𝑓 )
127 eqid ( 𝑚 ∈ ( 𝑇𝑅 ) ↦ ( 𝑚𝐽 ) ) = ( 𝑚 ∈ ( 𝑇𝑅 ) ↦ ( 𝑚𝐽 ) )
128 vex 𝑚 ∈ V
129 128 resex ( 𝑚𝐽 ) ∈ V
130 127 129 elrnmpti ( 𝑓 ∈ ran ( 𝑚 ∈ ( 𝑇𝑅 ) ↦ ( 𝑚𝐽 ) ) ↔ ∃ 𝑚 ∈ ( 𝑇𝑅 ) 𝑓 = ( 𝑚𝐽 ) )
131 1 2 3 4 5 6 7 8 9 eulerpartlemt ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) = ran ( 𝑚 ∈ ( 𝑇𝑅 ) ↦ ( 𝑚𝐽 ) )
132 131 eleq2i ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↔ 𝑓 ∈ ran ( 𝑚 ∈ ( 𝑇𝑅 ) ↦ ( 𝑚𝐽 ) ) )
133 elinel1 ( 𝑚 ∈ ( 𝑇𝑅 ) → 𝑚𝑇 )
134 114 fvtresfn ( 𝑚𝑇 → ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ‘ 𝑚 ) = ( 𝑚𝐽 ) )
135 134 eqeq1d ( 𝑚𝑇 → ( ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ‘ 𝑚 ) = 𝑓 ↔ ( 𝑚𝐽 ) = 𝑓 ) )
136 133 135 syl ( 𝑚 ∈ ( 𝑇𝑅 ) → ( ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ‘ 𝑚 ) = 𝑓 ↔ ( 𝑚𝐽 ) = 𝑓 ) )
137 eqcom ( ( 𝑚𝐽 ) = 𝑓𝑓 = ( 𝑚𝐽 ) )
138 136 137 bitrdi ( 𝑚 ∈ ( 𝑇𝑅 ) → ( ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ‘ 𝑚 ) = 𝑓𝑓 = ( 𝑚𝐽 ) ) )
139 138 rexbiia ( ∃ 𝑚 ∈ ( 𝑇𝑅 ) ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ‘ 𝑚 ) = 𝑓 ↔ ∃ 𝑚 ∈ ( 𝑇𝑅 ) 𝑓 = ( 𝑚𝐽 ) )
140 130 132 139 3bitr4ri ( ∃ 𝑚 ∈ ( 𝑇𝑅 ) ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ‘ 𝑚 ) = 𝑓𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) )
141 126 140 bitri ( 𝑓 ∈ ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) “ ( 𝑇𝑅 ) ) ↔ 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) )
142 141 eqriv ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) “ ( 𝑇𝑅 ) ) = ( ( ℕ0m 𝐽 ) ∩ 𝑅 )
143 f1oeq3 ( ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) “ ( 𝑇𝑅 ) ) = ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) → ( ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ↾ ( 𝑇𝑅 ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) “ ( 𝑇𝑅 ) ) ↔ ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ↾ ( 𝑇𝑅 ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ) )
144 142 143 ax-mp ( ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ↾ ( 𝑇𝑅 ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) “ ( 𝑇𝑅 ) ) ↔ ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ↾ ( 𝑇𝑅 ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) )
145 resmpt ( ( 𝑇𝑅 ) ⊆ 𝑇 → ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ↾ ( 𝑇𝑅 ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) )
146 f1oeq1 ( ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ↾ ( 𝑇𝑅 ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) → ( ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ↾ ( 𝑇𝑅 ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↔ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ) )
147 119 145 146 mp2b ( ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ↾ ( 𝑇𝑅 ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↔ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) )
148 144 147 bitri ( ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) ↾ ( 𝑇𝑅 ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( 𝑜𝑇 ↦ ( 𝑜𝐽 ) ) “ ( 𝑇𝑅 ) ) ↔ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) )
149 121 148 mpbi ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( ℕ0m 𝐽 ) ∩ 𝑅 )
150 f1oco ( ( ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) : ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ∧ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ) → ( ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } )
151 103 149 150 mp2an ( ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin }
152 f1of ( ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) → ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) : ( 𝑇𝑅 ) ⟶ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) )
153 eqid ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) )
154 153 fmpt ( ∀ 𝑜 ∈ ( 𝑇𝑅 ) ( 𝑜𝐽 ) ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↔ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) : ( 𝑇𝑅 ) ⟶ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) )
155 154 biimpri ( ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) : ( 𝑇𝑅 ) ⟶ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) → ∀ 𝑜 ∈ ( 𝑇𝑅 ) ( 𝑜𝐽 ) ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) )
156 149 152 155 mp2b 𝑜 ∈ ( 𝑇𝑅 ) ( 𝑜𝐽 ) ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 )
157 156 a1i ( ⊤ → ∀ 𝑜 ∈ ( 𝑇𝑅 ) ( 𝑜𝐽 ) ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) )
158 eqidd ( ⊤ → ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) )
159 eqidd ( ⊤ → ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) = ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) )
160 coeq2 ( 𝑓 = ( 𝑜𝐽 ) → ( bits ∘ 𝑓 ) = ( bits ∘ ( 𝑜𝐽 ) ) )
161 157 158 159 160 fmptcof ( ⊤ → ( ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) )
162 161 eqcomd ( ⊤ → ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) = ( ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) ) )
163 eqidd ( ⊤ → ( 𝑇𝑅 ) = ( 𝑇𝑅 ) )
164 6 a1i ( ⊤ → 𝐻 = { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } )
165 162 163 164 f1oeq123d ( ⊤ → ( ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) : ( 𝑇𝑅 ) –1-1-onto𝐻 ↔ ( ( 𝑓 ∈ ( ( ℕ0m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑜𝐽 ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ) )
166 151 165 mpbiri ( ⊤ → ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) : ( 𝑇𝑅 ) –1-1-onto𝐻 )
167 166 mptru ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) : ( 𝑇𝑅 ) –1-1-onto𝐻
168 f1oco ( ( 𝑀 : 𝐻1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ∧ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) : ( 𝑇𝑅 ) –1-1-onto𝐻 ) → ( 𝑀 ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
169 53 167 168 mp2an ( 𝑀 ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin )
170 eqidd ( ⊤ → ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) )
171 bitsf bits : ℤ ⟶ 𝒫 ℕ0
172 zex ℤ ∈ V
173 fex ( ( bits : ℤ ⟶ 𝒫 ℕ0 ∧ ℤ ∈ V ) → bits ∈ V )
174 171 172 173 mp2an bits ∈ V
175 174 123 coex ( bits ∘ ( 𝑜𝐽 ) ) ∈ V
176 175 a1i ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇𝑅 ) ) → ( bits ∘ ( 𝑜𝐽 ) ) ∈ V )
177 170 176 fvmpt2d ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇𝑅 ) ) → ( ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) ‘ 𝑜 ) = ( bits ∘ ( 𝑜𝐽 ) ) )
178 f1of ( ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) : ( 𝑇𝑅 ) –1-1-onto𝐻 → ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) : ( 𝑇𝑅 ) ⟶ 𝐻 )
179 166 178 syl ( ⊤ → ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) : ( 𝑇𝑅 ) ⟶ 𝐻 )
180 179 ffvelcdmda ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇𝑅 ) ) → ( ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) ‘ 𝑜 ) ∈ 𝐻 )
181 177 180 eqeltrrd ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇𝑅 ) ) → ( bits ∘ ( 𝑜𝐽 ) ) ∈ 𝐻 )
182 f1ofn ( 𝑀 : 𝐻1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) → 𝑀 Fn 𝐻 )
183 53 182 ax-mp 𝑀 Fn 𝐻
184 dffn5 ( 𝑀 Fn 𝐻𝑀 = ( 𝑟𝐻 ↦ ( 𝑀𝑟 ) ) )
185 183 184 mpbi 𝑀 = ( 𝑟𝐻 ↦ ( 𝑀𝑟 ) )
186 185 a1i ( ⊤ → 𝑀 = ( 𝑟𝐻 ↦ ( 𝑀𝑟 ) ) )
187 fveq2 ( 𝑟 = ( bits ∘ ( 𝑜𝐽 ) ) → ( 𝑀𝑟 ) = ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) )
188 181 170 186 187 fmptco ( ⊤ → ( 𝑀 ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) )
189 188 mptru ( 𝑀 ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) )
190 f1oeq1 ( ( 𝑀 ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) → ( ( 𝑀 ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↔ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ) )
191 189 190 ax-mp ( ( 𝑀 ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( bits ∘ ( 𝑜𝐽 ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↔ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
192 169 191 mpbi ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin )
193 f1oco ( ( ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹𝑎 ) ) : ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin ) ∧ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ) → ( ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹𝑎 ) ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin ) )
194 52 192 193 mp2an ( ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹𝑎 ) ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin )
195 simpr ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇𝑅 ) ) → 𝑜 ∈ ( 𝑇𝑅 ) )
196 fvex ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ∈ V
197 eqid ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) )
198 197 fvmpt2 ( ( 𝑜 ∈ ( 𝑇𝑅 ) ∧ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ∈ V ) → ( ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ‘ 𝑜 ) = ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) )
199 195 196 198 sylancl ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇𝑅 ) ) → ( ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ‘ 𝑜 ) = ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) )
200 f1of ( ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) → ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) : ( 𝑇𝑅 ) ⟶ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
201 192 200 mp1i ( ⊤ → ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) : ( 𝑇𝑅 ) ⟶ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
202 201 ffvelcdmda ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇𝑅 ) ) → ( ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ‘ 𝑜 ) ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
203 199 202 eqeltrrd ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇𝑅 ) ) → ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
204 eqidd ( ⊤ → ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) )
205 eqidd ( ⊤ → ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹𝑎 ) ) = ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹𝑎 ) ) )
206 imaeq2 ( 𝑎 = ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) → ( 𝐹𝑎 ) = ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) )
207 203 204 205 206 fmptco ( ⊤ → ( ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹𝑎 ) ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) )
208 207 mptru ( ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹𝑎 ) ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) )
209 f1oeq1 ( ( ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹𝑎 ) ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) → ( ( ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹𝑎 ) ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin ) ↔ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin ) ) )
210 208 209 ax-mp ( ( ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹𝑎 ) ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin ) ↔ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin ) )
211 194 210 mpbi ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin )
212 f1oco ( ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) : ( 𝒫 ℕ ∩ Fin ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin ) ) → ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) )
213 49 211 212 mp2an ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 )
214 5 mpoexg ( ( 𝐽 ∈ V ∧ ℕ0 ∈ V ) → 𝐹 ∈ V )
215 56 58 214 mp2an 𝐹 ∈ V
216 imaexg ( 𝐹 ∈ V → ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ∈ V )
217 215 216 ax-mp ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ∈ V
218 eqid ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) )
219 218 fvmpt2 ( ( 𝑜 ∈ ( 𝑇𝑅 ) ∧ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ∈ V ) → ( ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) ‘ 𝑜 ) = ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) )
220 195 217 219 sylancl ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇𝑅 ) ) → ( ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) ‘ 𝑜 ) = ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) )
221 f1of ( ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin ) → ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) : ( 𝑇𝑅 ) ⟶ ( 𝒫 ℕ ∩ Fin ) )
222 211 221 mp1i ( ⊤ → ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) : ( 𝑇𝑅 ) ⟶ ( 𝒫 ℕ ∩ Fin ) )
223 222 ffvelcdmda ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇𝑅 ) ) → ( ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) ‘ 𝑜 ) ∈ ( 𝒫 ℕ ∩ Fin ) )
224 220 223 eqeltrrd ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇𝑅 ) ) → ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ∈ ( 𝒫 ℕ ∩ Fin ) )
225 eqidd ( ⊤ → ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) )
226 indf1o ( ℕ ∈ V → ( 𝟭 ‘ ℕ ) : 𝒫 ℕ –1-1-onto→ ( { 0 , 1 } ↑m ℕ ) )
227 f1ofn ( ( 𝟭 ‘ ℕ ) : 𝒫 ℕ –1-1-onto→ ( { 0 , 1 } ↑m ℕ ) → ( 𝟭 ‘ ℕ ) Fn 𝒫 ℕ )
228 11 226 227 mp2b ( 𝟭 ‘ ℕ ) Fn 𝒫 ℕ
229 dffn5 ( ( 𝟭 ‘ ℕ ) Fn 𝒫 ℕ ↔ ( 𝟭 ‘ ℕ ) = ( 𝑏 ∈ 𝒫 ℕ ↦ ( ( 𝟭 ‘ ℕ ) ‘ 𝑏 ) ) )
230 228 229 mpbi ( 𝟭 ‘ ℕ ) = ( 𝑏 ∈ 𝒫 ℕ ↦ ( ( 𝟭 ‘ ℕ ) ‘ 𝑏 ) )
231 230 reseq1i ( ( 𝟭 ‘ ℕ ) ↾ Fin ) = ( ( 𝑏 ∈ 𝒫 ℕ ↦ ( ( 𝟭 ‘ ℕ ) ‘ 𝑏 ) ) ↾ Fin )
232 resmpt3 ( ( 𝑏 ∈ 𝒫 ℕ ↦ ( ( 𝟭 ‘ ℕ ) ‘ 𝑏 ) ) ↾ Fin ) = ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ 𝑏 ) )
233 231 232 eqtri ( ( 𝟭 ‘ ℕ ) ↾ Fin ) = ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ 𝑏 ) )
234 233 a1i ( ⊤ → ( ( 𝟭 ‘ ℕ ) ↾ Fin ) = ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ 𝑏 ) ) )
235 fveq2 ( 𝑏 = ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) → ( ( 𝟭 ‘ ℕ ) ‘ 𝑏 ) = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) )
236 224 225 234 235 fmptco ( ⊤ → ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) ) )
237 236 mptru ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) ) = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) )
238 10 237 eqtr4i 𝐺 = ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) )
239 f1oeq1 ( 𝐺 = ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) ) → ( 𝐺 : ( 𝑇𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ↔ ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ) )
240 238 239 ax-mp ( 𝐺 : ( 𝑇𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ↔ ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) ∘ ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) ) : ( 𝑇𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) )
241 213 240 mpbir 𝐺 : ( 𝑇𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 )