Metamath Proof Explorer

Theorem eulerpartlemgvv

Description: Lemma for eulerpart : value of the function G evaluated. (Contributed by Thierry Arnoux, 10-Aug-2018)

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 eulerpartlemgvv ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) → ( ( 𝐺 ‘ 𝐴 ) ‘ 𝐵 ) = if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 , 1 , 0 ) )

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 1 2 3 4 5 6 7 8 9 10 eulerpartlemgv ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐺 ‘ 𝐴 ) = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ) )
12 11 fveq1d ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( 𝐺 ‘ 𝐴 ) ‘ 𝐵 ) = ( ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ) ‘ 𝐵 ) )
13 12 adantr ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) → ( ( 𝐺 ‘ 𝐴 ) ‘ 𝐵 ) = ( ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ) ‘ 𝐵 ) )
14 nnex ⊢ ℕ ∈ V
15 imassrn ⊢ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ⊆ ran 𝐹
16 4 5 oddpwdc ⊢ 𝐹 : ( 𝐽 × ℕ0 ) –1-1-onto→ ℕ
17 f1of ⊢ ( 𝐹 : ( 𝐽 × ℕ0 ) –1-1-onto→ ℕ → 𝐹 : ( 𝐽 × ℕ0 ) ⟶ ℕ )
18 frn ⊢ ( 𝐹 : ( 𝐽 × ℕ0 ) ⟶ ℕ → ran 𝐹 ⊆ ℕ )
19 16 17 18 mp2b ⊢ ran 𝐹 ⊆ ℕ
20 15 19 sstri ⊢ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ⊆ ℕ
21 simpr ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℕ )
22 indfval ⊢ ( ( ℕ ∈ V ∧ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ) ‘ 𝐵 ) = if ( 𝐵 ∈ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) , 1 , 0 ) )
23 14 20 21 22 mp3an12i ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) → ( ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ) ‘ 𝐵 ) = if ( 𝐵 ∈ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) , 1 , 0 ) )
24 ffn ⊢ ( 𝐹 : ( 𝐽 × ℕ0 ) ⟶ ℕ → 𝐹 Fn ( 𝐽 × ℕ0 ) )
25 16 17 24 mp2b ⊢ 𝐹 Fn ( 𝐽 × ℕ0 )
26 1 2 3 4 5 6 7 8 9 10 eulerpartlemmf ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ 𝐻 )
27 1 2 3 4 5 6 7 eulerpartlem1 ⊢ 𝑀 : 𝐻 –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin )
28 f1of ⊢ ( 𝑀 : 𝐻 –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) → 𝑀 : 𝐻 ⟶ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
29 27 28 ax-mp ⊢ 𝑀 : 𝐻 ⟶ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin )
30 29 ffvelrni ⊢ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ 𝐻 → ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
31 26 30 syl ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
32 31 elin1d ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ∈ 𝒫 ( 𝐽 × ℕ0 ) )
33 32 adantr ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) → ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ∈ 𝒫 ( 𝐽 × ℕ0 ) )
34 33 elpwid ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) → ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ⊆ ( 𝐽 × ℕ0 ) )
35 fvelimab ⊢ ( ( 𝐹 Fn ( 𝐽 × ℕ0 ) ∧ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ⊆ ( 𝐽 × ℕ0 ) ) → ( 𝐵 ∈ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ↔ ∃ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ( 𝐹 ‘ 𝑤 ) = 𝐵 ) )
36 25 34 35 sylancr ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) → ( 𝐵 ∈ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ↔ ∃ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ( 𝐹 ‘ 𝑤 ) = 𝐵 ) )
37 4 ssrab3 ⊢ 𝐽 ⊆ ℕ
38 fveq1 ⊢ ( 𝑟 = ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) → ( 𝑟 ‘ 𝑥 ) = ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) )
39 38 eleq2d ⊢ ( 𝑟 = ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) → ( 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ↔ 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) ) )
40 39 anbi2d ⊢ ( 𝑟 = ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) → ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) ) ) )
41 40 opabbidv ⊢ ( 𝑟 = ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) ) } )
42 14 37 ssexi ⊢ 𝐽 ∈ V
43 abid2 ⊢ { 𝑦 ∣ 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) } = ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 )
44 43 fvexi ⊢ { 𝑦 ∣ 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) } ∈ V
45 44 a1i ⊢ ( 𝑥 ∈ 𝐽 → { 𝑦 ∣ 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) } ∈ V )
46 42 45 opabex3 ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) ) } ∈ V
47 46 a1i ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) ) } ∈ V )
48 7 41 26 47 fvmptd3 ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) ) } )
49 simpl ⊢ ( ( 𝑥 = 𝑡 ∧ 𝑦 = 𝑛 ) → 𝑥 = 𝑡 )
50 49 eleq1d ⊢ ( ( 𝑥 = 𝑡 ∧ 𝑦 = 𝑛 ) → ( 𝑥 ∈ 𝐽 ↔ 𝑡 ∈ 𝐽 ) )
51 simpr ⊢ ( ( 𝑥 = 𝑡 ∧ 𝑦 = 𝑛 ) → 𝑦 = 𝑛 )
52 49 fveq2d ⊢ ( ( 𝑥 = 𝑡 ∧ 𝑦 = 𝑛 ) → ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) = ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑡 ) )
53 51 52 eleq12d ⊢ ( ( 𝑥 = 𝑡 ∧ 𝑦 = 𝑛 ) → ( 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) ↔ 𝑛 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑡 ) ) )
54 50 53 anbi12d ⊢ ( ( 𝑥 = 𝑡 ∧ 𝑦 = 𝑛 ) → ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) ) ↔ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑡 ) ) ) )
55 54 cbvopabv ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) ) } = { ⟨ 𝑡 , 𝑛 ⟩ ∣ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑡 ) ) }
56 48 55 eqtrdi ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) = { ⟨ 𝑡 , 𝑛 ⟩ ∣ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑡 ) ) } )
57 56 eleq2d ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ↔ 𝑤 ∈ { ⟨ 𝑡 , 𝑛 ⟩ ∣ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑡 ) ) } ) )
58 1 2 3 4 5 6 7 8 9 eulerpartlemt0 ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ↔ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 ) )
59 58 simp1bi ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝐴 ∈ ( ℕ0 ↑m ℕ ) )
60 nn0ex ⊢ ℕ0 ∈ V
61 60 14 elmap ⊢ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) ↔ 𝐴 : ℕ ⟶ ℕ0 )
62 59 61 sylib ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝐴 : ℕ ⟶ ℕ0 )
63 ffun ⊢ ( 𝐴 : ℕ ⟶ ℕ0 → Fun 𝐴 )
64 funres ⊢ ( Fun 𝐴 → Fun ( 𝐴 ↾ 𝐽 ) )
65 62 63 64 3syl ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → Fun ( 𝐴 ↾ 𝐽 ) )
66 fssres ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝐽 ⊆ ℕ ) → ( 𝐴 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 )
67 62 37 66 sylancl ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐴 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 )
68 fdm ⊢ ( ( 𝐴 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 → dom ( 𝐴 ↾ 𝐽 ) = 𝐽 )
69 68 eleq2d ⊢ ( ( 𝐴 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 → ( 𝑡 ∈ dom ( 𝐴 ↾ 𝐽 ) ↔ 𝑡 ∈ 𝐽 ) )
70 67 69 syl ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑡 ∈ dom ( 𝐴 ↾ 𝐽 ) ↔ 𝑡 ∈ 𝐽 ) )
71 70 biimpar ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ 𝐽 ) → 𝑡 ∈ dom ( 𝐴 ↾ 𝐽 ) )
72 fvco ⊢ ( ( Fun ( 𝐴 ↾ 𝐽 ) ∧ 𝑡 ∈ dom ( 𝐴 ↾ 𝐽 ) ) → ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑡 ) = ( bits ‘ ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑡 ) ) )
73 65 71 72 syl2an2r ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ 𝐽 ) → ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑡 ) = ( bits ‘ ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑡 ) ) )
74 fvres ⊢ ( 𝑡 ∈ 𝐽 → ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑡 ) = ( 𝐴 ‘ 𝑡 ) )
75 74 fveq2d ⊢ ( 𝑡 ∈ 𝐽 → ( bits ‘ ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑡 ) ) = ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) )
76 75 adantl ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ 𝐽 ) → ( bits ‘ ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑡 ) ) = ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) )
77 73 76 eqtrd ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ 𝐽 ) → ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑡 ) = ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) )
78 77 eleq2d ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ 𝐽 ) → ( 𝑛 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑡 ) ↔ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) )
79 78 pm5.32da ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑡 ) ) ↔ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) )
80 79 opabbidv ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → { ⟨ 𝑡 , 𝑛 ⟩ ∣ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑡 ) ) } = { ⟨ 𝑡 , 𝑛 ⟩ ∣ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) } )
81 80 eleq2d ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑤 ∈ { ⟨ 𝑡 , 𝑛 ⟩ ∣ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑡 ) ) } ↔ 𝑤 ∈ { ⟨ 𝑡 , 𝑛 ⟩ ∣ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) } ) )
82 elopab ⊢ ( 𝑤 ∈ { ⟨ 𝑡 , 𝑛 ⟩ ∣ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) } ↔ ∃ 𝑡 ∃ 𝑛 ( 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ∧ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) )
83 81 82 bitrdi ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑤 ∈ { ⟨ 𝑡 , 𝑛 ⟩ ∣ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑡 ) ) } ↔ ∃ 𝑡 ∃ 𝑛 ( 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ∧ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ) )
84 ancom ⊢ ( ( 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ∧ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ↔ ( ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ∧ 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) )
85 anass ⊢ ( ( ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ∧ 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) ↔ ( 𝑡 ∈ 𝐽 ∧ ( 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ∧ 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) ) )
86 84 85 bitri ⊢ ( ( 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ∧ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ↔ ( 𝑡 ∈ 𝐽 ∧ ( 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ∧ 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) ) )
87 86 2exbii ⊢ ( ∃ 𝑡 ∃ 𝑛 ( 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ∧ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ↔ ∃ 𝑡 ∃ 𝑛 ( 𝑡 ∈ 𝐽 ∧ ( 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ∧ 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) ) )
88 df-rex ⊢ ( ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ↔ ∃ 𝑛 ( 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ∧ 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) )
89 88 anbi2i ⊢ ( ( 𝑡 ∈ 𝐽 ∧ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) ↔ ( 𝑡 ∈ 𝐽 ∧ ∃ 𝑛 ( 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ∧ 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) ) )
90 89 exbii ⊢ ( ∃ 𝑡 ( 𝑡 ∈ 𝐽 ∧ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) ↔ ∃ 𝑡 ( 𝑡 ∈ 𝐽 ∧ ∃ 𝑛 ( 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ∧ 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) ) )
91 df-rex ⊢ ( ∃ 𝑡 ∈ 𝐽 ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ↔ ∃ 𝑡 ( 𝑡 ∈ 𝐽 ∧ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) )
92 exdistr ⊢ ( ∃ 𝑡 ∃ 𝑛 ( 𝑡 ∈ 𝐽 ∧ ( 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ∧ 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) ) ↔ ∃ 𝑡 ( 𝑡 ∈ 𝐽 ∧ ∃ 𝑛 ( 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ∧ 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) ) )
93 90 91 92 3bitr4i ⊢ ( ∃ 𝑡 ∈ 𝐽 ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ↔ ∃ 𝑡 ∃ 𝑛 ( 𝑡 ∈ 𝐽 ∧ ( 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ∧ 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) ) )
94 87 93 bitr4i ⊢ ( ∃ 𝑡 ∃ 𝑛 ( 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ∧ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ↔ ∃ 𝑡 ∈ 𝐽 ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ )
95 83 94 bitrdi ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑤 ∈ { ⟨ 𝑡 , 𝑛 ⟩ ∣ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑡 ) ) } ↔ ∃ 𝑡 ∈ 𝐽 ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) )
96 57 95 bitrd ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ↔ ∃ 𝑡 ∈ 𝐽 ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) )
97 96 biimpa ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) → ∃ 𝑡 ∈ 𝐽 ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ )
98 97 adantlr ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) → ∃ 𝑡 ∈ 𝐽 ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ )
99 fveq2 ⊢ ( 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ ⟨ 𝑡 , 𝑛 ⟩ ) )
100 99 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ∧ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ∧ 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ ⟨ 𝑡 , 𝑛 ⟩ ) )
101 bitsss ⊢ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ⊆ ℕ0
102 101 sseli ⊢ ( 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) → 𝑛 ∈ ℕ0 )
103 102 anim2i ⊢ ( ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) → ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0 ) )
104 103 ad2antlr ⊢ ( ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ∧ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ∧ 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) → ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0 ) )
105 opelxp ⊢ ( ⟨ 𝑡 , 𝑛 ⟩ ∈ ( 𝐽 × ℕ0 ) ↔ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0 ) )
106 4 5 oddpwdcv ⊢ ( ⟨ 𝑡 , 𝑛 ⟩ ∈ ( 𝐽 × ℕ0 ) → ( 𝐹 ‘ ⟨ 𝑡 , 𝑛 ⟩ ) = ( ( 2 ↑ ( 2nd ‘ ⟨ 𝑡 , 𝑛 ⟩ ) ) · ( 1st ‘ ⟨ 𝑡 , 𝑛 ⟩ ) ) )
107 vex ⊢ 𝑡 ∈ V
108 vex ⊢ 𝑛 ∈ V
109 107 108 op2nd ⊢ ( 2nd ‘ ⟨ 𝑡 , 𝑛 ⟩ ) = 𝑛
110 109 oveq2i ⊢ ( 2 ↑ ( 2nd ‘ ⟨ 𝑡 , 𝑛 ⟩ ) ) = ( 2 ↑ 𝑛 )
111 107 108 op1st ⊢ ( 1st ‘ ⟨ 𝑡 , 𝑛 ⟩ ) = 𝑡
112 110 111 oveq12i ⊢ ( ( 2 ↑ ( 2nd ‘ ⟨ 𝑡 , 𝑛 ⟩ ) ) · ( 1st ‘ ⟨ 𝑡 , 𝑛 ⟩ ) ) = ( ( 2 ↑ 𝑛 ) · 𝑡 )
113 106 112 eqtrdi ⊢ ( ⟨ 𝑡 , 𝑛 ⟩ ∈ ( 𝐽 × ℕ0 ) → ( 𝐹 ‘ ⟨ 𝑡 , 𝑛 ⟩ ) = ( ( 2 ↑ 𝑛 ) · 𝑡 ) )
114 105 113 sylbir ⊢ ( ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ‘ ⟨ 𝑡 , 𝑛 ⟩ ) = ( ( 2 ↑ 𝑛 ) · 𝑡 ) )
115 104 114 syl ⊢ ( ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ∧ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ∧ 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) → ( 𝐹 ‘ ⟨ 𝑡 , 𝑛 ⟩ ) = ( ( 2 ↑ 𝑛 ) · 𝑡 ) )
116 100 115 eqtr2d ⊢ ( ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ∧ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ∧ 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ ) → ( ( 2 ↑ 𝑛 ) · 𝑡 ) = ( 𝐹 ‘ 𝑤 ) )
117 116 ex ⊢ ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ∧ ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ → ( ( 2 ↑ 𝑛 ) · 𝑡 ) = ( 𝐹 ‘ 𝑤 ) ) )
118 117 reximdvva ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) → ( ∃ 𝑡 ∈ 𝐽 ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ → ∃ 𝑡 ∈ 𝐽 ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = ( 𝐹 ‘ 𝑤 ) ) )
119 98 118 mpd ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) → ∃ 𝑡 ∈ 𝐽 ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = ( 𝐹 ‘ 𝑤 ) )
120 ssrexv ⊢ ( 𝐽 ⊆ ℕ → ( ∃ 𝑡 ∈ 𝐽 ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = ( 𝐹 ‘ 𝑤 ) → ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = ( 𝐹 ‘ 𝑤 ) ) )
121 37 119 120 mpsyl ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) → ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = ( 𝐹 ‘ 𝑤 ) )
122 121 adantr ⊢ ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ∧ ( 𝐹 ‘ 𝑤 ) = 𝐵 ) → ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = ( 𝐹 ‘ 𝑤 ) )
123 eqeq2 ⊢ ( ( 𝐹 ‘ 𝑤 ) = 𝐵 → ( ( ( 2 ↑ 𝑛 ) · 𝑡 ) = ( 𝐹 ‘ 𝑤 ) ↔ ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) )
124 123 rexbidv ⊢ ( ( 𝐹 ‘ 𝑤 ) = 𝐵 → ( ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = ( 𝐹 ‘ 𝑤 ) ↔ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) )
125 124 adantl ⊢ ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ∧ ( 𝐹 ‘ 𝑤 ) = 𝐵 ) → ( ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = ( 𝐹 ‘ 𝑤 ) ↔ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) )
126 125 rexbidv ⊢ ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ∧ ( 𝐹 ‘ 𝑤 ) = 𝐵 ) → ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = ( 𝐹 ‘ 𝑤 ) ↔ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) )
127 122 126 mpbid ⊢ ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ∧ ( 𝐹 ‘ 𝑤 ) = 𝐵 ) → ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 )
128 127 r19.29an ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ ∃ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ( 𝐹 ‘ 𝑤 ) = 𝐵 ) → ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 )
129 simp-5l ⊢ ( ( ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) ∧ ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) → 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) )
130 simpllr ⊢ ( ( ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) ∧ ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) → 𝑥 ∈ 𝐽 )
131 simplr ⊢ ( ( ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) ∧ ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) → 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) )
132 68 eleq2d ⊢ ( ( 𝐴 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 → ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐽 ) ↔ 𝑥 ∈ 𝐽 ) )
133 67 132 syl ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐽 ) ↔ 𝑥 ∈ 𝐽 ) )
134 133 biimpar ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ dom ( 𝐴 ↾ 𝐽 ) )
135 fvco ⊢ ( ( Fun ( 𝐴 ↾ 𝐽 ) ∧ 𝑥 ∈ dom ( 𝐴 ↾ 𝐽 ) ) → ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) = ( bits ‘ ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑥 ) ) )
136 65 134 135 syl2an2r ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑥 ∈ 𝐽 ) → ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) = ( bits ‘ ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑥 ) ) )
137 fvres ⊢ ( 𝑥 ∈ 𝐽 → ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
138 137 fveq2d ⊢ ( 𝑥 ∈ 𝐽 → ( bits ‘ ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑥 ) ) = ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) )
139 138 adantl ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑥 ∈ 𝐽 ) → ( bits ‘ ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑥 ) ) = ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) )
140 136 139 eqtrd ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑥 ∈ 𝐽 ) → ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) = ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) )
141 129 130 140 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) ∧ ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) → ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) = ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) )
142 131 141 eleqtrrd ⊢ ( ( ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) ∧ ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) → 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) )
143 48 eleq2d ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) ) } ) )
144 opabidw ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) ) } ↔ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) ) )
145 143 144 bitrdi ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ↔ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) ) ) )
146 145 biimpar ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ‘ 𝑥 ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) )
147 129 130 142 146 syl12anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) ∧ ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) )
148 simpr ⊢ ( ( ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) ∧ ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) → ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 )
149 34 ad4antr ⊢ ( ( ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) ∧ ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) → ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ⊆ ( 𝐽 × ℕ0 ) )
150 149 147 sseldd ⊢ ( ( ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) ∧ ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐽 × ℕ0 ) )
151 opeq1 ⊢ ( 𝑡 = 𝑥 → ⟨ 𝑡 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
152 151 eleq1d ⊢ ( 𝑡 = 𝑥 → ( ⟨ 𝑡 , 𝑦 ⟩ ∈ ( 𝐽 × ℕ0 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐽 × ℕ0 ) ) )
153 151 fveq2d ⊢ ( 𝑡 = 𝑥 → ( 𝐹 ‘ ⟨ 𝑡 , 𝑦 ⟩ ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
154 oveq2 ⊢ ( 𝑡 = 𝑥 → ( ( 2 ↑ 𝑦 ) · 𝑡 ) = ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
155 153 154 eqeq12d ⊢ ( 𝑡 = 𝑥 → ( ( 𝐹 ‘ ⟨ 𝑡 , 𝑦 ⟩ ) = ( ( 2 ↑ 𝑦 ) · 𝑡 ) ↔ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) )
156 152 155 imbi12d ⊢ ( 𝑡 = 𝑥 → ( ( ⟨ 𝑡 , 𝑦 ⟩ ∈ ( 𝐽 × ℕ0 ) → ( 𝐹 ‘ ⟨ 𝑡 , 𝑦 ⟩ ) = ( ( 2 ↑ 𝑦 ) · 𝑡 ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐽 × ℕ0 ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ) )
157 opeq2 ⊢ ( 𝑛 = 𝑦 → ⟨ 𝑡 , 𝑛 ⟩ = ⟨ 𝑡 , 𝑦 ⟩ )
158 157 eleq1d ⊢ ( 𝑛 = 𝑦 → ( ⟨ 𝑡 , 𝑛 ⟩ ∈ ( 𝐽 × ℕ0 ) ↔ ⟨ 𝑡 , 𝑦 ⟩ ∈ ( 𝐽 × ℕ0 ) ) )
159 157 fveq2d ⊢ ( 𝑛 = 𝑦 → ( 𝐹 ‘ ⟨ 𝑡 , 𝑛 ⟩ ) = ( 𝐹 ‘ ⟨ 𝑡 , 𝑦 ⟩ ) )
160 oveq2 ⊢ ( 𝑛 = 𝑦 → ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑦 ) )
161 160 oveq1d ⊢ ( 𝑛 = 𝑦 → ( ( 2 ↑ 𝑛 ) · 𝑡 ) = ( ( 2 ↑ 𝑦 ) · 𝑡 ) )
162 159 161 eqeq12d ⊢ ( 𝑛 = 𝑦 → ( ( 𝐹 ‘ ⟨ 𝑡 , 𝑛 ⟩ ) = ( ( 2 ↑ 𝑛 ) · 𝑡 ) ↔ ( 𝐹 ‘ ⟨ 𝑡 , 𝑦 ⟩ ) = ( ( 2 ↑ 𝑦 ) · 𝑡 ) ) )
163 158 162 imbi12d ⊢ ( 𝑛 = 𝑦 → ( ( ⟨ 𝑡 , 𝑛 ⟩ ∈ ( 𝐽 × ℕ0 ) → ( 𝐹 ‘ ⟨ 𝑡 , 𝑛 ⟩ ) = ( ( 2 ↑ 𝑛 ) · 𝑡 ) ) ↔ ( ⟨ 𝑡 , 𝑦 ⟩ ∈ ( 𝐽 × ℕ0 ) → ( 𝐹 ‘ ⟨ 𝑡 , 𝑦 ⟩ ) = ( ( 2 ↑ 𝑦 ) · 𝑡 ) ) ) )
164 163 113 chvarvv ⊢ ( ⟨ 𝑡 , 𝑦 ⟩ ∈ ( 𝐽 × ℕ0 ) → ( 𝐹 ‘ ⟨ 𝑡 , 𝑦 ⟩ ) = ( ( 2 ↑ 𝑦 ) · 𝑡 ) )
165 156 164 chvarvv ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐽 × ℕ0 ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
166 eqeq2 ⊢ ( ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 → ( ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ↔ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝐵 ) )
167 166 biimpa ⊢ ( ( ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝐵 )
168 165 167 sylan2 ⊢ ( ( ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐽 × ℕ0 ) ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝐵 )
169 148 150 168 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) ∧ ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝐵 )
170 fveqeq2 ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐹 ‘ 𝑤 ) = 𝐵 ↔ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝐵 ) )
171 170 rspcev ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝐵 ) → ∃ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ( 𝐹 ‘ 𝑤 ) = 𝐵 )
172 147 169 171 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) ∧ ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) → ∃ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ( 𝐹 ‘ 𝑤 ) = 𝐵 )
173 oveq2 ⊢ ( 𝑡 = 𝑥 → ( ( 2 ↑ 𝑛 ) · 𝑡 ) = ( ( 2 ↑ 𝑛 ) · 𝑥 ) )
174 173 eqeq1d ⊢ ( 𝑡 = 𝑥 → ( ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ↔ ( ( 2 ↑ 𝑛 ) · 𝑥 ) = 𝐵 ) )
175 160 oveq1d ⊢ ( 𝑛 = 𝑦 → ( ( 2 ↑ 𝑛 ) · 𝑥 ) = ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
176 175 eqeq1d ⊢ ( 𝑛 = 𝑦 → ( ( ( 2 ↑ 𝑛 ) · 𝑥 ) = 𝐵 ↔ ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) )
177 174 176 sylan9bb ⊢ ( ( 𝑡 = 𝑥 ∧ 𝑛 = 𝑦 ) → ( ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ↔ ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) )
178 simpl ⊢ ( ( 𝑡 = 𝑥 ∧ 𝑛 = 𝑦 ) → 𝑡 = 𝑥 )
179 178 fveq2d ⊢ ( ( 𝑡 = 𝑥 ∧ 𝑛 = 𝑦 ) → ( 𝐴 ‘ 𝑡 ) = ( 𝐴 ‘ 𝑥 ) )
180 179 fveq2d ⊢ ( ( 𝑡 = 𝑥 ∧ 𝑛 = 𝑦 ) → ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) = ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) )
181 177 180 cbvrexdva2 ⊢ ( 𝑡 = 𝑥 → ( ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ↔ ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) )
182 181 cbvrexvw ⊢ ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ↔ ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 )
183 nfv ⊢ Ⅎ 𝑦 𝐴 ∈ ( 𝑇 ∩ 𝑅 )
184 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ ℕ
185 nfre1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵
186 184 185 nfan ⊢ Ⅎ 𝑦 ( 𝑥 ∈ ℕ ∧ ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 )
187 183 186 nfan ⊢ Ⅎ 𝑦 ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑥 ∈ ℕ ∧ ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) )
188 simplr ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) → 𝑥 ∈ ℕ )
189 62 ffvelrnda ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑥 ∈ ℕ ) → ( 𝐴 ‘ 𝑥 ) ∈ ℕ0 )
190 189 adantr ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) → ( 𝐴 ‘ 𝑥 ) ∈ ℕ0 )
191 elnn0 ⊢ ( ( 𝐴 ‘ 𝑥 ) ∈ ℕ0 ↔ ( ( 𝐴 ‘ 𝑥 ) ∈ ℕ ∨ ( 𝐴 ‘ 𝑥 ) = 0 ) )
192 190 191 sylib ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) → ( ( 𝐴 ‘ 𝑥 ) ∈ ℕ ∨ ( 𝐴 ‘ 𝑥 ) = 0 ) )
193 n0i ⊢ ( 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) → ¬ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) = ∅ )
194 193 adantl ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) → ¬ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) = ∅ )
195 fveq2 ⊢ ( ( 𝐴 ‘ 𝑥 ) = 0 → ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) = ( bits ‘ 0 ) )
196 0bits ⊢ ( bits ‘ 0 ) = ∅
197 195 196 eqtrdi ⊢ ( ( 𝐴 ‘ 𝑥 ) = 0 → ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) = ∅ )
198 194 197 nsyl ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) → ¬ ( 𝐴 ‘ 𝑥 ) = 0 )
199 192 198 olcnd ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) → ( 𝐴 ‘ 𝑥 ) ∈ ℕ )
200 58 simp3bi ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 )
201 200 sselda ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑛 ∈ ( ◡ 𝐴 “ ℕ ) ) → 𝑛 ∈ 𝐽 )
202 breq2 ⊢ ( 𝑧 = 𝑛 → ( 2 ∥ 𝑧 ↔ 2 ∥ 𝑛 ) )
203 202 notbid ⊢ ( 𝑧 = 𝑛 → ( ¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑛 ) )
204 203 4 elrab2 ⊢ ( 𝑛 ∈ 𝐽 ↔ ( 𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛 ) )
205 204 simprbi ⊢ ( 𝑛 ∈ 𝐽 → ¬ 2 ∥ 𝑛 )
206 201 205 syl ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑛 ∈ ( ◡ 𝐴 “ ℕ ) ) → ¬ 2 ∥ 𝑛 )
207 206 ralrimiva ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ∀ 𝑛 ∈ ( ◡ 𝐴 “ ℕ ) ¬ 2 ∥ 𝑛 )
208 ffn ⊢ ( 𝐴 : ℕ ⟶ ℕ0 → 𝐴 Fn ℕ )
209 elpreima ⊢ ( 𝐴 Fn ℕ → ( 𝑛 ∈ ( ◡ 𝐴 “ ℕ ) ↔ ( 𝑛 ∈ ℕ ∧ ( 𝐴 ‘ 𝑛 ) ∈ ℕ ) ) )
210 62 208 209 3syl ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑛 ∈ ( ◡ 𝐴 “ ℕ ) ↔ ( 𝑛 ∈ ℕ ∧ ( 𝐴 ‘ 𝑛 ) ∈ ℕ ) ) )
211 210 imbi1d ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( 𝑛 ∈ ( ◡ 𝐴 “ ℕ ) → ¬ 2 ∥ 𝑛 ) ↔ ( ( 𝑛 ∈ ℕ ∧ ( 𝐴 ‘ 𝑛 ) ∈ ℕ ) → ¬ 2 ∥ 𝑛 ) ) )
212 impexp ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ( 𝐴 ‘ 𝑛 ) ∈ ℕ ) → ¬ 2 ∥ 𝑛 ) ↔ ( 𝑛 ∈ ℕ → ( ( 𝐴 ‘ 𝑛 ) ∈ ℕ → ¬ 2 ∥ 𝑛 ) ) )
213 211 212 bitrdi ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( 𝑛 ∈ ( ◡ 𝐴 “ ℕ ) → ¬ 2 ∥ 𝑛 ) ↔ ( 𝑛 ∈ ℕ → ( ( 𝐴 ‘ 𝑛 ) ∈ ℕ → ¬ 2 ∥ 𝑛 ) ) ) )
214 213 ralbidv2 ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ∀ 𝑛 ∈ ( ◡ 𝐴 “ ℕ ) ¬ 2 ∥ 𝑛 ↔ ∀ 𝑛 ∈ ℕ ( ( 𝐴 ‘ 𝑛 ) ∈ ℕ → ¬ 2 ∥ 𝑛 ) ) )
215 207 214 mpbid ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ∀ 𝑛 ∈ ℕ ( ( 𝐴 ‘ 𝑛 ) ∈ ℕ → ¬ 2 ∥ 𝑛 ) )
216 fveq2 ⊢ ( 𝑥 = 𝑛 → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑛 ) )
217 216 eleq1d ⊢ ( 𝑥 = 𝑛 → ( ( 𝐴 ‘ 𝑥 ) ∈ ℕ ↔ ( 𝐴 ‘ 𝑛 ) ∈ ℕ ) )
218 breq2 ⊢ ( 𝑥 = 𝑛 → ( 2 ∥ 𝑥 ↔ 2 ∥ 𝑛 ) )
219 218 notbid ⊢ ( 𝑥 = 𝑛 → ( ¬ 2 ∥ 𝑥 ↔ ¬ 2 ∥ 𝑛 ) )
220 217 219 imbi12d ⊢ ( 𝑥 = 𝑛 → ( ( ( 𝐴 ‘ 𝑥 ) ∈ ℕ → ¬ 2 ∥ 𝑥 ) ↔ ( ( 𝐴 ‘ 𝑛 ) ∈ ℕ → ¬ 2 ∥ 𝑛 ) ) )
221 220 cbvralvw ⊢ ( ∀ 𝑥 ∈ ℕ ( ( 𝐴 ‘ 𝑥 ) ∈ ℕ → ¬ 2 ∥ 𝑥 ) ↔ ∀ 𝑛 ∈ ℕ ( ( 𝐴 ‘ 𝑛 ) ∈ ℕ → ¬ 2 ∥ 𝑛 ) )
222 215 221 sylibr ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ∀ 𝑥 ∈ ℕ ( ( 𝐴 ‘ 𝑥 ) ∈ ℕ → ¬ 2 ∥ 𝑥 ) )
223 222 r19.21bi ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝐴 ‘ 𝑥 ) ∈ ℕ → ¬ 2 ∥ 𝑥 ) )
224 223 imp ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑥 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑥 ) ∈ ℕ ) → ¬ 2 ∥ 𝑥 )
225 199 224 syldan ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) → ¬ 2 ∥ 𝑥 )
226 breq2 ⊢ ( 𝑧 = 𝑥 → ( 2 ∥ 𝑧 ↔ 2 ∥ 𝑥 ) )
227 226 notbid ⊢ ( 𝑧 = 𝑥 → ( ¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑥 ) )
228 227 4 elrab2 ⊢ ( 𝑥 ∈ 𝐽 ↔ ( 𝑥 ∈ ℕ ∧ ¬ 2 ∥ 𝑥 ) )
229 188 225 228 sylanbrc ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) → 𝑥 ∈ 𝐽 )
230 229 adantlrr ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑥 ∈ ℕ ∧ ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) → 𝑥 ∈ 𝐽 )
231 230 adantr ⊢ ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑥 ∈ ℕ ∧ ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) ) ∧ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ) ∧ ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) → 𝑥 ∈ 𝐽 )
232 simprr ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑥 ∈ ℕ ∧ ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) ) → ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 )
233 187 231 232 r19.29af ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑥 ∈ ℕ ∧ ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) ) → 𝑥 ∈ 𝐽 )
234 233 232 jca ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑥 ∈ ℕ ∧ ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) ) → ( 𝑥 ∈ 𝐽 ∧ ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) )
235 234 ex ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( 𝑥 ∈ ℕ ∧ ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) → ( 𝑥 ∈ 𝐽 ∧ ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) ) )
236 235 reximdv2 ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) )
237 236 imp ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 )
238 237 adantlr ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 ) → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 )
239 182 238 sylan2b ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ ( bits ‘ ( 𝐴 ‘ 𝑥 ) ) ( ( 2 ↑ 𝑦 ) · 𝑥 ) = 𝐵 )
240 172 239 r19.29vva ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) → ∃ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ( 𝐹 ‘ 𝑤 ) = 𝐵 )
241 128 240 impbida ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑤 ∈ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ( 𝐹 ‘ 𝑤 ) = 𝐵 ↔ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) )
242 36 241 bitrd ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) → ( 𝐵 ∈ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ↔ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 ) )
243 242 ifbid ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) → if ( 𝐵 ∈ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) , 1 , 0 ) = if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 , 1 , 0 ) )
244 13 23 243 3eqtrd ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝐵 ∈ ℕ ) → ( ( 𝐺 ‘ 𝐴 ) ‘ 𝐵 ) = if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝐵 , 1 , 0 ) )