Metamath Proof Explorer

Theorem eulerpartlemgh

Description: Lemma for eulerpart : The F function is a bijection on the U subsets. (Contributed by Thierry Arnoux, 15-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 ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) )
eulerpartlemgh.1 ⊢ 𝑈 = ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) )
Assertion eulerpartlemgh ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐹 ↾ 𝑈 ) : 𝑈 –1-1-onto→ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } )

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 eulerpartlemgh.1 ⊢ 𝑈 = ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) )
12 4 5 oddpwdc ⊢ 𝐹 : ( 𝐽 × ℕ0 ) –1-1-onto→ ℕ
13 f1of1 ⊢ ( 𝐹 : ( 𝐽 × ℕ0 ) –1-1-onto→ ℕ → 𝐹 : ( 𝐽 × ℕ0 ) –1-1→ ℕ )
14 12 13 ax-mp ⊢ 𝐹 : ( 𝐽 × ℕ0 ) –1-1→ ℕ
15 iunss ⊢ ( ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) ↔ ∀ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) )
16 inss2 ⊢ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ⊆ 𝐽
17 16 sseli ⊢ ( 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) → 𝑡 ∈ 𝐽 )
18 17 snssd ⊢ ( 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) → { 𝑡 } ⊆ 𝐽 )
19 bitsss ⊢ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ⊆ ℕ0
20 xpss12 ⊢ ( ( { 𝑡 } ⊆ 𝐽 ∧ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ⊆ ℕ0 ) → ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) )
21 18 19 20 sylancl ⊢ ( 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) → ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) )
22 15 21 mprgbir ⊢ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 )
23 11 22 eqsstri ⊢ 𝑈 ⊆ ( 𝐽 × ℕ0 )
24 f1ores ⊢ ( ( 𝐹 : ( 𝐽 × ℕ0 ) –1-1→ ℕ ∧ 𝑈 ⊆ ( 𝐽 × ℕ0 ) ) → ( 𝐹 ↾ 𝑈 ) : 𝑈 –1-1-onto→ ( 𝐹 “ 𝑈 ) )
25 14 23 24 mp2an ⊢ ( 𝐹 ↾ 𝑈 ) : 𝑈 –1-1-onto→ ( 𝐹 “ 𝑈 )
26 simpr ⊢ ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ∧ ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) → ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 )
27 2nn ⊢ 2 ∈ ℕ
28 27 a1i ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) → 2 ∈ ℕ )
29 19 sseli ⊢ ( 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) → 𝑛 ∈ ℕ0 )
30 29 adantl ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) → 𝑛 ∈ ℕ0 )
31 28 30 nnexpcld ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
32 simplr ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) → 𝑡 ∈ ℕ )
33 31 32 nnmulcld ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) → ( ( 2 ↑ 𝑛 ) · 𝑡 ) ∈ ℕ )
34 33 adantr ⊢ ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ∧ ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) → ( ( 2 ↑ 𝑛 ) · 𝑡 ) ∈ ℕ )
35 26 34 eqeltrrd ⊢ ( ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ∧ ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) → 𝑝 ∈ ℕ )
36 35 rexlimdva2 ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) → ( ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 → 𝑝 ∈ ℕ ) )
37 36 rexlimdva ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 → 𝑝 ∈ ℕ ) )
38 37 pm4.71rd ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ↔ ( 𝑝 ∈ ℕ ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) ) )
39 rex0 ⊢ ¬ ∃ 𝑛 ∈ ∅ ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝
40 simplr ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) → 𝑡 ∈ ℕ )
41 simpr ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) → ¬ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) )
42 1 2 3 4 5 6 7 8 9 eulerpartlemt0 ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ↔ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 ) )
43 42 simp1bi ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝐴 ∈ ( ℕ0 ↑m ℕ ) )
44 elmapi ⊢ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) → 𝐴 : ℕ ⟶ ℕ0 )
45 43 44 syl ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝐴 : ℕ ⟶ ℕ0 )
46 45 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) → 𝐴 : ℕ ⟶ ℕ0 )
47 ffn ⊢ ( 𝐴 : ℕ ⟶ ℕ0 → 𝐴 Fn ℕ )
48 elpreima ⊢ ( 𝐴 Fn ℕ → ( 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ↔ ( 𝑡 ∈ ℕ ∧ ( 𝐴 ‘ 𝑡 ) ∈ ℕ ) ) )
49 46 47 48 3syl ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) → ( 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ↔ ( 𝑡 ∈ ℕ ∧ ( 𝐴 ‘ 𝑡 ) ∈ ℕ ) ) )
50 41 49 mtbid ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) → ¬ ( 𝑡 ∈ ℕ ∧ ( 𝐴 ‘ 𝑡 ) ∈ ℕ ) )
51 imnan ⊢ ( ( 𝑡 ∈ ℕ → ¬ ( 𝐴 ‘ 𝑡 ) ∈ ℕ ) ↔ ¬ ( 𝑡 ∈ ℕ ∧ ( 𝐴 ‘ 𝑡 ) ∈ ℕ ) )
52 50 51 sylibr ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) → ( 𝑡 ∈ ℕ → ¬ ( 𝐴 ‘ 𝑡 ) ∈ ℕ ) )
53 40 52 mpd ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) → ¬ ( 𝐴 ‘ 𝑡 ) ∈ ℕ )
54 46 40 ffvelcdmd ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) → ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 )
55 elnn0 ⊢ ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 ↔ ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ ∨ ( 𝐴 ‘ 𝑡 ) = 0 ) )
56 54 55 sylib ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) → ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ ∨ ( 𝐴 ‘ 𝑡 ) = 0 ) )
57 orel1 ⊢ ( ¬ ( 𝐴 ‘ 𝑡 ) ∈ ℕ → ( ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ ∨ ( 𝐴 ‘ 𝑡 ) = 0 ) → ( 𝐴 ‘ 𝑡 ) = 0 ) )
58 53 56 57 sylc ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) → ( 𝐴 ‘ 𝑡 ) = 0 )
59 58 fveq2d ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) → ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) = ( bits ‘ 0 ) )
60 0bits ⊢ ( bits ‘ 0 ) = ∅
61 59 60 eqtrdi ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) → ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) = ∅ )
62 61 rexeqdv ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) → ( ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ↔ ∃ 𝑛 ∈ ∅ ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
63 39 62 mtbiri ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) → ¬ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 )
64 63 ex ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) → ( ¬ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) → ¬ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
65 64 con4d ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) → ( ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 → 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) )
66 65 impr ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) ) → 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) )
67 eldif ⊢ ( 𝑡 ∈ ( ℕ ∖ 𝐽 ) ↔ ( 𝑡 ∈ ℕ ∧ ¬ 𝑡 ∈ 𝐽 ) )
68 1 2 3 4 5 6 7 8 9 eulerpartlemf ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ 𝐽 ) ) → ( 𝐴 ‘ 𝑡 ) = 0 )
69 67 68 sylan2br ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ ¬ 𝑡 ∈ 𝐽 ) ) → ( 𝐴 ‘ 𝑡 ) = 0 )
70 69 anassrs ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ 𝐽 ) → ( 𝐴 ‘ 𝑡 ) = 0 )
71 70 fveq2d ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ 𝐽 ) → ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) = ( bits ‘ 0 ) )
72 71 60 eqtrdi ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ 𝐽 ) → ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) = ∅ )
73 72 rexeqdv ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ 𝐽 ) → ( ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ↔ ∃ 𝑛 ∈ ∅ ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
74 39 73 mtbiri ⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ 𝐽 ) → ¬ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 )
75 74 ex ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) → ( ¬ 𝑡 ∈ 𝐽 → ¬ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
76 75 con4d ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) → ( ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 → 𝑡 ∈ 𝐽 ) )
77 76 impr ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) ) → 𝑡 ∈ 𝐽 )
78 66 77 elind ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) ) → 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) )
79 simprr ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) ) → ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 )
80 78 79 jca ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) ) → ( 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
81 80 ex ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( 𝑡 ∈ ℕ ∧ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) → ( 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) ) )
82 81 reximdv2 ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 → ∃ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
83 ssrab2 ⊢ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ⊆ ℕ
84 4 83 eqsstri ⊢ 𝐽 ⊆ ℕ
85 16 84 sstri ⊢ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ⊆ ℕ
86 ssrexv ⊢ ( ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ⊆ ℕ → ( ∃ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 → ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
87 85 86 mp1i ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ∃ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 → ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
88 82 87 impbid ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ↔ ∃ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
89 38 88 bitr3d ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( 𝑝 ∈ ℕ ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) ↔ ∃ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
90 eqeq2 ⊢ ( 𝑚 = 𝑝 → ( ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 ↔ ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
91 90 2rexbidv ⊢ ( 𝑚 = 𝑝 → ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 ↔ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
92 91 elrab ⊢ ( 𝑝 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ↔ ( 𝑝 ∈ ℕ ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
93 92 a1i ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑝 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ↔ ( 𝑝 ∈ ℕ ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) ) )
94 11 imaeq2i ⊢ ( 𝐹 “ 𝑈 ) = ( 𝐹 “ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) )
95 imaiun ⊢ ( 𝐹 “ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) = ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( 𝐹 “ ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) )
96 94 95 eqtri ⊢ ( 𝐹 “ 𝑈 ) = ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( 𝐹 “ ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) )
97 96 eleq2i ⊢ ( 𝑝 ∈ ( 𝐹 “ 𝑈 ) ↔ 𝑝 ∈ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( 𝐹 “ ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) )
98 eliun ⊢ ( 𝑝 ∈ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( 𝐹 “ ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ↔ ∃ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) 𝑝 ∈ ( 𝐹 “ ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) )
99 f1ofn ⊢ ( 𝐹 : ( 𝐽 × ℕ0 ) –1-1-onto→ ℕ → 𝐹 Fn ( 𝐽 × ℕ0 ) )
100 12 99 ax-mp ⊢ 𝐹 Fn ( 𝐽 × ℕ0 )
101 snssi ⊢ ( 𝑡 ∈ 𝐽 → { 𝑡 } ⊆ 𝐽 )
102 101 19 20 sylancl ⊢ ( 𝑡 ∈ 𝐽 → ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) )
103 ovelimab ⊢ ( ( 𝐹 Fn ( 𝐽 × ℕ0 ) ∧ ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) ) → ( 𝑝 ∈ ( 𝐹 “ ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ↔ ∃ 𝑥 ∈ { 𝑡 } ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑝 = ( 𝑥 𝐹 𝑛 ) ) )
104 100 102 103 sylancr ⊢ ( 𝑡 ∈ 𝐽 → ( 𝑝 ∈ ( 𝐹 “ ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ↔ ∃ 𝑥 ∈ { 𝑡 } ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑝 = ( 𝑥 𝐹 𝑛 ) ) )
105 vex ⊢ 𝑡 ∈ V
106 oveq1 ⊢ ( 𝑥 = 𝑡 → ( 𝑥 𝐹 𝑛 ) = ( 𝑡 𝐹 𝑛 ) )
107 106 eqeq2d ⊢ ( 𝑥 = 𝑡 → ( 𝑝 = ( 𝑥 𝐹 𝑛 ) ↔ 𝑝 = ( 𝑡 𝐹 𝑛 ) ) )
108 107 rexbidv ⊢ ( 𝑥 = 𝑡 → ( ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑝 = ( 𝑥 𝐹 𝑛 ) ↔ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑝 = ( 𝑡 𝐹 𝑛 ) ) )
109 105 108 rexsn ⊢ ( ∃ 𝑥 ∈ { 𝑡 } ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑝 = ( 𝑥 𝐹 𝑛 ) ↔ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑝 = ( 𝑡 𝐹 𝑛 ) )
110 104 109 bitrdi ⊢ ( 𝑡 ∈ 𝐽 → ( 𝑝 ∈ ( 𝐹 “ ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ↔ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑝 = ( 𝑡 𝐹 𝑛 ) ) )
111 df-ov ⊢ ( 𝑡 𝐹 𝑛 ) = ( 𝐹 ‘ ⟨ 𝑡 , 𝑛 ⟩ )
112 111 eqeq1i ⊢ ( ( 𝑡 𝐹 𝑛 ) = 𝑝 ↔ ( 𝐹 ‘ ⟨ 𝑡 , 𝑛 ⟩ ) = 𝑝 )
113 eqcom ⊢ ( ( 𝑡 𝐹 𝑛 ) = 𝑝 ↔ 𝑝 = ( 𝑡 𝐹 𝑛 ) )
114 112 113 bitr3i ⊢ ( ( 𝐹 ‘ ⟨ 𝑡 , 𝑛 ⟩ ) = 𝑝 ↔ 𝑝 = ( 𝑡 𝐹 𝑛 ) )
115 opelxpi ⊢ ( ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0 ) → ⟨ 𝑡 , 𝑛 ⟩ ∈ ( 𝐽 × ℕ0 ) )
116 4 5 oddpwdcv ⊢ ( ⟨ 𝑡 , 𝑛 ⟩ ∈ ( 𝐽 × ℕ0 ) → ( 𝐹 ‘ ⟨ 𝑡 , 𝑛 ⟩ ) = ( ( 2 ↑ ( 2nd ‘ ⟨ 𝑡 , 𝑛 ⟩ ) ) · ( 1st ‘ ⟨ 𝑡 , 𝑛 ⟩ ) ) )
117 vex ⊢ 𝑛 ∈ V
118 105 117 op2nd ⊢ ( 2nd ‘ ⟨ 𝑡 , 𝑛 ⟩ ) = 𝑛
119 118 oveq2i ⊢ ( 2 ↑ ( 2nd ‘ ⟨ 𝑡 , 𝑛 ⟩ ) ) = ( 2 ↑ 𝑛 )
120 105 117 op1st ⊢ ( 1st ‘ ⟨ 𝑡 , 𝑛 ⟩ ) = 𝑡
121 119 120 oveq12i ⊢ ( ( 2 ↑ ( 2nd ‘ ⟨ 𝑡 , 𝑛 ⟩ ) ) · ( 1st ‘ ⟨ 𝑡 , 𝑛 ⟩ ) ) = ( ( 2 ↑ 𝑛 ) · 𝑡 )
122 116 121 eqtrdi ⊢ ( ⟨ 𝑡 , 𝑛 ⟩ ∈ ( 𝐽 × ℕ0 ) → ( 𝐹 ‘ ⟨ 𝑡 , 𝑛 ⟩ ) = ( ( 2 ↑ 𝑛 ) · 𝑡 ) )
123 115 122 syl ⊢ ( ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ‘ ⟨ 𝑡 , 𝑛 ⟩ ) = ( ( 2 ↑ 𝑛 ) · 𝑡 ) )
124 123 eqeq1d ⊢ ( ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐹 ‘ ⟨ 𝑡 , 𝑛 ⟩ ) = 𝑝 ↔ ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
125 114 124 bitr3id ⊢ ( ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑝 = ( 𝑡 𝐹 𝑛 ) ↔ ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
126 29 125 sylan2 ⊢ ( ( 𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) → ( 𝑝 = ( 𝑡 𝐹 𝑛 ) ↔ ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
127 126 rexbidva ⊢ ( 𝑡 ∈ 𝐽 → ( ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) 𝑝 = ( 𝑡 𝐹 𝑛 ) ↔ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
128 110 127 bitrd ⊢ ( 𝑡 ∈ 𝐽 → ( 𝑝 ∈ ( 𝐹 “ ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ↔ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
129 17 128 syl ⊢ ( 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) → ( 𝑝 ∈ ( 𝐹 “ ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ↔ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
130 129 rexbiia ⊢ ( ∃ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) 𝑝 ∈ ( 𝐹 “ ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ↔ ∃ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 )
131 97 98 130 3bitri ⊢ ( 𝑝 ∈ ( 𝐹 “ 𝑈 ) ↔ ∃ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 )
132 131 a1i ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑝 ∈ ( 𝐹 “ 𝑈 ) ↔ ∃ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑝 ) )
133 89 93 132 3bitr4rd ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑝 ∈ ( 𝐹 “ 𝑈 ) ↔ 𝑝 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) )
134 133 eqrdv ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐹 “ 𝑈 ) = { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } )
135 f1oeq3 ⊢ ( ( 𝐹 “ 𝑈 ) = { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → ( ( 𝐹 ↾ 𝑈 ) : 𝑈 –1-1-onto→ ( 𝐹 “ 𝑈 ) ↔ ( 𝐹 ↾ 𝑈 ) : 𝑈 –1-1-onto→ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) )
136 134 135 syl ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( 𝐹 ↾ 𝑈 ) : 𝑈 –1-1-onto→ ( 𝐹 “ 𝑈 ) ↔ ( 𝐹 ↾ 𝑈 ) : 𝑈 –1-1-onto→ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) )
137 25 136 mpbii ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐹 ↾ 𝑈 ) : 𝑈 –1-1-onto→ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } )