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 ⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ 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 ⊢ 𝑇 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ 𝑓 “ ℕ ) ⊆ 𝐽 }
eulerpart.g ⊢ 𝐺 = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) )
Assertion eulerpartgbij 𝐺 : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 )

Proof

Step Hyp Ref Expression
1 eulerpart.p ⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ 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 ⊢ 𝑇 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ 𝑓 “ ℕ ) ⊆ 𝐽 }
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 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin )
55 54 a1i ⊢ ( ⊤ → ( bits ↾ ℕ0 ) : ℕ0 –1-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 ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐽 ) → 𝑓 : 𝐽 ⟶ ℕ0 )
70 frnnn0supp ⊢ ( ( 𝐽 ∈ V ∧ 𝑓 : 𝐽 ⟶ ℕ0 ) → ( 𝑓 supp 0 ) = ( ◡ 𝑓 “ ℕ ) )
71 56 69 70 sylancr ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐽 ) → ( 𝑓 supp 0 ) = ( ◡ 𝑓 “ ℕ ) )
72 71 eleq1d ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐽 ) → ( ( 𝑓 supp 0 ) ∈ Fin ↔ ( ◡ 𝑓 “ ℕ ) ∈ Fin ) )
73 72 rabbiia ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( 𝑓 supp 0 ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
74 elmapfun ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐽 ) → 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 ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐽 ) → ( 𝑓 finSupp 0 ↔ ( 𝑓 supp 0 ) ∈ Fin ) )
79 78 rabbiia ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐽 ) ∣ 𝑓 finSupp 0 } = { 𝑓 ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( 𝑓 supp 0 ) ∈ Fin }
80 incom ⊢ ( { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∩ ( ℕ0 ↑m 𝐽 ) ) = ( ( ℕ0 ↑m 𝐽 ) ∩ { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
81 dfrab2 ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = ( { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∩ ( ℕ0 ↑m 𝐽 ) )
82 8 ineq2i ⊢ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) = ( ( ℕ0 ↑m 𝐽 ) ∩ { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
83 80 81 82 3eqtr4ri ⊢ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) = { 𝑓 ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
84 73 79 83 3eqtr4ri ⊢ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) = { 𝑓 ∈ ( ℕ0 ↑m 𝐽 ) ∣ 𝑓 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 ⊢ ( ⊤ → ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) ) : ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } )
94 elinel1 ⊢ ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) → 𝑓 ∈ ( ℕ0 ↑m 𝐽 ) )
95 frn ⊢ ( 𝑓 : 𝐽 ⟶ ℕ0 → ran 𝑓 ⊆ ℕ0 )
96 cores ⊢ ( ran 𝑓 ⊆ ℕ0 → ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) = ( bits ∘ 𝑓 ) )
97 69 95 96 3syl ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐽 ) → ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) = ( bits ∘ 𝑓 ) )
98 94 97 syl ⊢ ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) → ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) = ( bits ∘ 𝑓 ) )
99 98 mpteq2ia ⊢ ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) ) = ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) )
100 99 eqcomi ⊢ ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) = ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) )
101 f1oeq1 ⊢ ( ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) = ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) ) → ( ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) : ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↔ ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) ) : ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ) )
102 100 101 mp1i ⊢ ( ⊤ → ( ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) : ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↔ ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) ) : ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ) )
103 93 102 mpbird ⊢ ( ⊤ → ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) : ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } )
104 103 mptru ⊢ ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) : ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin }
105 ssrab2 ⊢ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ⊆ ℕ
106 4 105 eqsstri ⊢ 𝐽 ⊆ ℕ
107 11 58 106 3pm3.2i ⊢ ( ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ )
108 cnveq ⊢ ( 𝑓 = 𝑜 → ◡ 𝑓 = ◡ 𝑜 )
109 dfn2 ⊢ ℕ = ( ℕ0 ∖ { 0 } )
110 109 a1i ⊢ ( 𝑓 = 𝑜 → ℕ = ( ℕ0 ∖ { 0 } ) )
111 108 110 imaeq12d ⊢ ( 𝑓 = 𝑜 → ( ◡ 𝑓 “ ℕ ) = ( ◡ 𝑜 “ ( ℕ0 ∖ { 0 } ) ) )
112 111 sseq1d ⊢ ( 𝑓 = 𝑜 → ( ( ◡ 𝑓 “ ℕ ) ⊆ 𝐽 ↔ ( ◡ 𝑜 “ ( ℕ0 ∖ { 0 } ) ) ⊆ 𝐽 ) )
113 112 cbvrabv ⊢ { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ 𝑓 “ ℕ ) ⊆ 𝐽 } = { 𝑜 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ 𝑜 “ ( ℕ0 ∖ { 0 } ) ) ⊆ 𝐽 }
114 9 113 eqtri ⊢ 𝑇 = { 𝑜 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ 𝑜 “ ( ℕ0 ∖ { 0 } ) ) ⊆ 𝐽 }
115 eqid ⊢ ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) = ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) )
116 114 115 resf1o ⊢ ( ( ( ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ ) ∧ 0 ∈ ℕ0 ) → ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) : 𝑇 –1-1-onto→ ( ℕ0 ↑m 𝐽 ) )
117 107 63 116 mp2an ⊢ ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) : 𝑇 –1-1-onto→ ( ℕ0 ↑m 𝐽 )
118 f1of1 ⊢ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) : 𝑇 –1-1-onto→ ( ℕ0 ↑m 𝐽 ) → ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) : 𝑇 –1-1→ ( ℕ0 ↑m 𝐽 ) )
119 117 118 ax-mp ⊢ ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) : 𝑇 –1-1→ ( ℕ0 ↑m 𝐽 )
120 inss1 ⊢ ( 𝑇 ∩ 𝑅 ) ⊆ 𝑇
121 f1ores ⊢ ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) : 𝑇 –1-1→ ( ℕ0 ↑m 𝐽 ) ∧ ( 𝑇 ∩ 𝑅 ) ⊆ 𝑇 ) → ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) “ ( 𝑇 ∩ 𝑅 ) ) )
122 119 120 121 mp2an ⊢ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) “ ( 𝑇 ∩ 𝑅 ) )
123 vex ⊢ 𝑜 ∈ V
124 123 resex ⊢ ( 𝑜 ↾ 𝐽 ) ∈ V
125 124 115 fnmpti ⊢ ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) Fn 𝑇
126 fvelimab ⊢ ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) Fn 𝑇 ∧ ( 𝑇 ∩ 𝑅 ) ⊆ 𝑇 ) → ( 𝑓 ∈ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) “ ( 𝑇 ∩ 𝑅 ) ) ↔ ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ‘ 𝑚 ) = 𝑓 ) )
127 125 120 126 mp2an ⊢ ( 𝑓 ∈ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) “ ( 𝑇 ∩ 𝑅 ) ) ↔ ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ‘ 𝑚 ) = 𝑓 )
128 eqid ⊢ ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑚 ↾ 𝐽 ) ) = ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑚 ↾ 𝐽 ) )
129 vex ⊢ 𝑚 ∈ V
130 129 resex ⊢ ( 𝑚 ↾ 𝐽 ) ∈ V
131 128 130 elrnmpti ⊢ ( 𝑓 ∈ ran ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑚 ↾ 𝐽 ) ) ↔ ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) 𝑓 = ( 𝑚 ↾ 𝐽 ) )
132 1 2 3 4 5 6 7 8 9 eulerpartlemt ⊢ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) = ran ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑚 ↾ 𝐽 ) )
133 132 eleq2i ⊢ ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↔ 𝑓 ∈ ran ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑚 ↾ 𝐽 ) ) )
134 elinel1 ⊢ ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) → 𝑚 ∈ 𝑇 )
135 115 fvtresfn ⊢ ( 𝑚 ∈ 𝑇 → ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ‘ 𝑚 ) = ( 𝑚 ↾ 𝐽 ) )
136 135 eqeq1d ⊢ ( 𝑚 ∈ 𝑇 → ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ‘ 𝑚 ) = 𝑓 ↔ ( 𝑚 ↾ 𝐽 ) = 𝑓 ) )
137 134 136 syl ⊢ ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ‘ 𝑚 ) = 𝑓 ↔ ( 𝑚 ↾ 𝐽 ) = 𝑓 ) )
138 eqcom ⊢ ( ( 𝑚 ↾ 𝐽 ) = 𝑓 ↔ 𝑓 = ( 𝑚 ↾ 𝐽 ) )
139 137 138 bitrdi ⊢ ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ‘ 𝑚 ) = 𝑓 ↔ 𝑓 = ( 𝑚 ↾ 𝐽 ) ) )
140 139 rexbiia ⊢ ( ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ‘ 𝑚 ) = 𝑓 ↔ ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) 𝑓 = ( 𝑚 ↾ 𝐽 ) )
141 131 133 140 3bitr4ri ⊢ ( ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ‘ 𝑚 ) = 𝑓 ↔ 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
142 127 141 bitri ⊢ ( 𝑓 ∈ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) “ ( 𝑇 ∩ 𝑅 ) ) ↔ 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
143 142 eqriv ⊢ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) “ ( 𝑇 ∩ 𝑅 ) ) = ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 )
144 f1oeq3 ⊢ ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) “ ( 𝑇 ∩ 𝑅 ) ) = ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) → ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) “ ( 𝑇 ∩ 𝑅 ) ) ↔ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ) )
145 143 144 ax-mp ⊢ ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) “ ( 𝑇 ∩ 𝑅 ) ) ↔ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
146 resmpt ⊢ ( ( 𝑇 ∩ 𝑅 ) ⊆ 𝑇 → ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) )
147 f1oeq1 ⊢ ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) → ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↔ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ) )
148 120 146 147 mp2b ⊢ ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↔ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
149 145 148 bitri ⊢ ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) “ ( 𝑇 ∩ 𝑅 ) ) ↔ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
150 122 149 mpbi ⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 )
151 f1oco ⊢ ( ( ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) : ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ∧ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ) → ( ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } )
152 104 150 151 mp2an ⊢ ( ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin }
153 f1of ⊢ ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) → ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) : ( 𝑇 ∩ 𝑅 ) ⟶ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
154 eqid ⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) )
155 154 fmpt ⊢ ( ∀ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ( 𝑜 ↾ 𝐽 ) ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↔ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) : ( 𝑇 ∩ 𝑅 ) ⟶ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
156 155 biimpri ⊢ ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) : ( 𝑇 ∩ 𝑅 ) ⟶ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) → ∀ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ( 𝑜 ↾ 𝐽 ) ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
157 150 153 156 mp2b ⊢ ∀ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ( 𝑜 ↾ 𝐽 ) ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 )
158 157 a1i ⊢ ( ⊤ → ∀ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ( 𝑜 ↾ 𝐽 ) ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
159 eqidd ⊢ ( ⊤ → ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) )
160 eqidd ⊢ ( ⊤ → ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) = ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) )
161 coeq2 ⊢ ( 𝑓 = ( 𝑜 ↾ 𝐽 ) → ( bits ∘ 𝑓 ) = ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) )
162 158 159 160 161 fmptcof ⊢ ( ⊤ → ( ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) )
163 162 eqcomd ⊢ ( ⊤ → ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) = ( ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) ) )
164 eqidd ⊢ ( ⊤ → ( 𝑇 ∩ 𝑅 ) = ( 𝑇 ∩ 𝑅 ) )
165 6 a1i ⊢ ( ⊤ → 𝐻 = { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } )
166 163 164 165 f1oeq123d ⊢ ( ⊤ → ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ 𝐻 ↔ ( ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ) )
167 152 166 mpbiri ⊢ ( ⊤ → ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ 𝐻 )
168 167 mptru ⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ 𝐻
169 f1oco ⊢ ( ( 𝑀 : 𝐻 –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ∧ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ 𝐻 ) → ( 𝑀 ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
170 53 168 169 mp2an ⊢ ( 𝑀 ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin )
171 eqidd ⊢ ( ⊤ → ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) )
172 bitsf ⊢ bits : ℤ ⟶ 𝒫 ℕ0
173 zex ⊢ ℤ ∈ V
174 fex ⊢ ( ( bits : ℤ ⟶ 𝒫 ℕ0 ∧ ℤ ∈ V ) → bits ∈ V )
175 172 173 174 mp2an ⊢ bits ∈ V
176 175 124 coex ⊢ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ∈ V
177 176 a1i ⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ) → ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ∈ V )
178 171 177 fvmpt2d ⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ) → ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ‘ 𝑜 ) = ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) )
179 f1of ⊢ ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ 𝐻 → ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) : ( 𝑇 ∩ 𝑅 ) ⟶ 𝐻 )
180 167 179 syl ⊢ ( ⊤ → ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) : ( 𝑇 ∩ 𝑅 ) ⟶ 𝐻 )
181 180 ffvelrnda ⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ) → ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ‘ 𝑜 ) ∈ 𝐻 )
182 178 181 eqeltrrd ⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ) → ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ∈ 𝐻 )
183 f1ofn ⊢ ( 𝑀 : 𝐻 –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) → 𝑀 Fn 𝐻 )
184 53 183 ax-mp ⊢ 𝑀 Fn 𝐻
185 dffn5 ⊢ ( 𝑀 Fn 𝐻 ↔ 𝑀 = ( 𝑟 ∈ 𝐻 ↦ ( 𝑀 ‘ 𝑟 ) ) )
186 184 185 mpbi ⊢ 𝑀 = ( 𝑟 ∈ 𝐻 ↦ ( 𝑀 ‘ 𝑟 ) )
187 186 a1i ⊢ ( ⊤ → 𝑀 = ( 𝑟 ∈ 𝐻 ↦ ( 𝑀 ‘ 𝑟 ) ) )
188 fveq2 ⊢ ( 𝑟 = ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) → ( 𝑀 ‘ 𝑟 ) = ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) )
189 182 171 187 188 fmptco ⊢ ( ⊤ → ( 𝑀 ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) )
190 189 mptru ⊢ ( 𝑀 ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) )
191 f1oeq1 ⊢ ( ( 𝑀 ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) → ( ( 𝑀 ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↔ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ) )
192 190 191 ax-mp ⊢ ( ( 𝑀 ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↔ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
193 170 192 mpbi ⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin )
194 f1oco ⊢ ( ( ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹 “ 𝑎 ) ) : ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin ) ∧ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ) → ( ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹 “ 𝑎 ) ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin ) )
195 52 193 194 mp2an ⊢ ( ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹 “ 𝑎 ) ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin )
196 simpr ⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ) → 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) )
197 fvex ⊢ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ∈ V
198 eqid ⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) )
199 198 fvmpt2 ⊢ ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ∈ V ) → ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ‘ 𝑜 ) = ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) )
200 196 197 199 sylancl ⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ) → ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ‘ 𝑜 ) = ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) )
201 f1of ⊢ ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) → ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) : ( 𝑇 ∩ 𝑅 ) ⟶ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
202 193 201 mp1i ⊢ ( ⊤ → ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) : ( 𝑇 ∩ 𝑅 ) ⟶ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
203 202 ffvelrnda ⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ) → ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ‘ 𝑜 ) ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
204 200 203 eqeltrrd ⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ) → ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
205 eqidd ⊢ ( ⊤ → ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) )
206 eqidd ⊢ ( ⊤ → ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹 “ 𝑎 ) ) = ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹 “ 𝑎 ) ) )
207 imaeq2 ⊢ ( 𝑎 = ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) → ( 𝐹 “ 𝑎 ) = ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) )
208 204 205 206 207 fmptco ⊢ ( ⊤ → ( ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹 “ 𝑎 ) ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) )
209 208 mptru ⊢ ( ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹 “ 𝑎 ) ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) )
210 f1oeq1 ⊢ ( ( ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹 “ 𝑎 ) ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) → ( ( ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹 “ 𝑎 ) ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin ) ↔ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin ) ) )
211 209 210 ax-mp ⊢ ( ( ( 𝑎 ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↦ ( 𝐹 “ 𝑎 ) ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin ) ↔ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin ) )
212 195 211 mpbi ⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin )
213 f1oco ⊢ ( ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) : ( 𝒫 ℕ ∩ Fin ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin ) ) → ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) )
214 49 212 213 mp2an ⊢ ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 )
215 5 mpoexg ⊢ ( ( 𝐽 ∈ V ∧ ℕ0 ∈ V ) → 𝐹 ∈ V )
216 56 58 215 mp2an ⊢ 𝐹 ∈ V
217 imaexg ⊢ ( 𝐹 ∈ V → ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ∈ V )
218 216 217 ax-mp ⊢ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ∈ V
219 eqid ⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) )
220 219 fvmpt2 ⊢ ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ∈ V ) → ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ‘ 𝑜 ) = ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) )
221 196 218 220 sylancl ⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ) → ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ‘ 𝑜 ) = ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) )
222 f1of ⊢ ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( 𝒫 ℕ ∩ Fin ) → ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) : ( 𝑇 ∩ 𝑅 ) ⟶ ( 𝒫 ℕ ∩ Fin ) )
223 212 222 mp1i ⊢ ( ⊤ → ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) : ( 𝑇 ∩ 𝑅 ) ⟶ ( 𝒫 ℕ ∩ Fin ) )
224 223 ffvelrnda ⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ) → ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ‘ 𝑜 ) ∈ ( 𝒫 ℕ ∩ Fin ) )
225 221 224 eqeltrrd ⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ) → ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ∈ ( 𝒫 ℕ ∩ Fin ) )
226 eqidd ⊢ ( ⊤ → ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) )
227 indf1o ⊢ ( ℕ ∈ V → ( 𝟭 ‘ ℕ ) : 𝒫 ℕ –1-1-onto→ ( { 0 , 1 } ↑m ℕ ) )
228 f1ofn ⊢ ( ( 𝟭 ‘ ℕ ) : 𝒫 ℕ –1-1-onto→ ( { 0 , 1 } ↑m ℕ ) → ( 𝟭 ‘ ℕ ) Fn 𝒫 ℕ )
229 11 227 228 mp2b ⊢ ( 𝟭 ‘ ℕ ) Fn 𝒫 ℕ
230 dffn5 ⊢ ( ( 𝟭 ‘ ℕ ) Fn 𝒫 ℕ ↔ ( 𝟭 ‘ ℕ ) = ( 𝑏 ∈ 𝒫 ℕ ↦ ( ( 𝟭 ‘ ℕ ) ‘ 𝑏 ) ) )
231 229 230 mpbi ⊢ ( 𝟭 ‘ ℕ ) = ( 𝑏 ∈ 𝒫 ℕ ↦ ( ( 𝟭 ‘ ℕ ) ‘ 𝑏 ) )
232 231 reseq1i ⊢ ( ( 𝟭 ‘ ℕ ) ↾ Fin ) = ( ( 𝑏 ∈ 𝒫 ℕ ↦ ( ( 𝟭 ‘ ℕ ) ‘ 𝑏 ) ) ↾ Fin )
233 resmpt3 ⊢ ( ( 𝑏 ∈ 𝒫 ℕ ↦ ( ( 𝟭 ‘ ℕ ) ‘ 𝑏 ) ) ↾ Fin ) = ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ 𝑏 ) )
234 232 233 eqtri ⊢ ( ( 𝟭 ‘ ℕ ) ↾ Fin ) = ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ 𝑏 ) )
235 234 a1i ⊢ ( ⊤ → ( ( 𝟭 ‘ ℕ ) ↾ Fin ) = ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ 𝑏 ) ) )
236 fveq2 ⊢ ( 𝑏 = ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) → ( ( 𝟭 ‘ ℕ ) ‘ 𝑏 ) = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) )
237 225 226 235 236 fmptco ⊢ ( ⊤ → ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) )
238 237 mptru ⊢ ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) )
239 10 238 eqtr4i ⊢ 𝐺 = ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) )
240 f1oeq1 ⊢ ( 𝐺 = ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) → ( 𝐺 : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ↔ ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ) )
241 239 240 ax-mp ⊢ ( 𝐺 : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ↔ ( ( ( 𝟭 ‘ ℕ ) ↾ Fin ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) )
242 214 241 mpbir ⊢ 𝐺 : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 )