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 fcdmnn0supp ⊢ ( ( 𝐽 ∈ 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 94 69 95 96 4syl ⊢ ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) → ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) = ( bits ∘ 𝑓 ) )
98 97 mpteq2ia ⊢ ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) ) = ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) )
99 98 eqcomi ⊢ ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) = ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( ( bits ↾ ℕ0 ) ∘ 𝑓 ) )
100 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 } ) )
101 99 100 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 } ) )
102 93 101 mpbird ⊢ ( ⊤ → ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) : ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } )
103 102 mptru ⊢ ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) : ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) –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 ⊢ { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ 𝑓 “ ℕ ) ⊆ 𝐽 } = { 𝑜 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ 𝑜 “ ( ℕ0 ∖ { 0 } ) ) ⊆ 𝐽 }
113 9 112 eqtri ⊢ 𝑇 = { 𝑜 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ 𝑜 “ ( ℕ0 ∖ { 0 } ) ) ⊆ 𝐽 }
114 eqid ⊢ ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) = ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) )
115 113 114 resf1o ⊢ ( ( ( ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ ) ∧ 0 ∈ ℕ0 ) → ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) : 𝑇 –1-1-onto→ ( ℕ0 ↑m 𝐽 ) )
116 106 63 115 mp2an ⊢ ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) : 𝑇 –1-1-onto→ ( ℕ0 ↑m 𝐽 )
117 f1of1 ⊢ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) : 𝑇 –1-1-onto→ ( ℕ0 ↑m 𝐽 ) → ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) : 𝑇 –1-1→ ( ℕ0 ↑m 𝐽 ) )
118 116 117 ax-mp ⊢ ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) : 𝑇 –1-1→ ( ℕ0 ↑m 𝐽 )
119 inss1 ⊢ ( 𝑇 ∩ 𝑅 ) ⊆ 𝑇
120 f1ores ⊢ ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) : 𝑇 –1-1→ ( ℕ0 ↑m 𝐽 ) ∧ ( 𝑇 ∩ 𝑅 ) ⊆ 𝑇 ) → ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) : ( 𝑇 ∩ 𝑅 ) –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 ⊢ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) = ran ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑚 ↾ 𝐽 ) )
132 131 eleq2i ⊢ ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↔ 𝑓 ∈ 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 ⊢ ( ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ‘ 𝑚 ) = 𝑓 ↔ 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
141 126 140 bitri ⊢ ( 𝑓 ∈ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) “ ( 𝑇 ∩ 𝑅 ) ) ↔ 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
142 141 eqriv ⊢ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) “ ( 𝑇 ∩ 𝑅 ) ) = ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 )
143 f1oeq3 ⊢ ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) “ ( 𝑇 ∩ 𝑅 ) ) = ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) → ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) “ ( 𝑇 ∩ 𝑅 ) ) ↔ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ) )
144 142 143 ax-mp ⊢ ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) “ ( 𝑇 ∩ 𝑅 ) ) ↔ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
145 resmpt ⊢ ( ( 𝑇 ∩ 𝑅 ) ⊆ 𝑇 → ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) )
146 f1oeq1 ⊢ ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) → ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↔ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ) )
147 119 145 146 mp2b ⊢ ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↔ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
148 144 147 bitri ⊢ ( ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) ↾ ( 𝑇 ∩ 𝑅 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( 𝑜 ∈ 𝑇 ↦ ( 𝑜 ↾ 𝐽 ) ) “ ( 𝑇 ∩ 𝑅 ) ) ↔ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
149 121 148 mpbi ⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 )
150 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 } )
151 103 149 150 mp2an ⊢ ( ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin }
152 f1of ⊢ ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) → ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) : ( 𝑇 ∩ 𝑅 ) ⟶ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
153 eqid ⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) )
154 153 fmpt ⊢ ( ∀ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ( 𝑜 ↾ 𝐽 ) ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↔ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) : ( 𝑇 ∩ 𝑅 ) ⟶ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
155 154 biimpri ⊢ ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) : ( 𝑇 ∩ 𝑅 ) ⟶ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) → ∀ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ( 𝑜 ↾ 𝐽 ) ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
156 149 152 155 mp2b ⊢ ∀ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ( 𝑜 ↾ 𝐽 ) ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 )
157 156 a1i ⊢ ( ⊤ → ∀ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ( 𝑜 ↾ 𝐽 ) ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) )
158 eqidd ⊢ ( ⊤ → ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) )
159 eqidd ⊢ ( ⊤ → ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) = ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) )
160 coeq2 ⊢ ( 𝑓 = ( 𝑜 ↾ 𝐽 ) → ( bits ∘ 𝑓 ) = ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) )
161 157 158 159 160 fmptcof ⊢ ( ⊤ → ( ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) ) = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) )
162 161 eqcomd ⊢ ( ⊤ → ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) = ( ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( bits ∘ 𝑓 ) ) ∘ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑜 ↾ 𝐽 ) ) ) )
163 eqidd ⊢ ( ⊤ → ( 𝑇 ∩ 𝑅 ) = ( 𝑇 ∩ 𝑅 ) )
164 6 a1i ⊢ ( ⊤ → 𝐻 = { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } )
165 162 163 164 f1oeq123d ⊢ ( ⊤ → ( ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ 𝐻 ↔ ( ( 𝑓 ∈ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) ↦ ( 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 ℕ ) ∩ 𝑅 )