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	ffvelcdmi	⊢ ( ( 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	ffvelcdmda	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑥 ∈ ℕ ) → ( 𝐴 ‘ 𝑥 ) ∈ ℕ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 ) )