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 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } )