Metamath Proof Explorer

Theorem eulerpartlemmf

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 30-Aug-2018) (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 eulerpartlemmf ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ 𝐻 )

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 bitsf1o ⊢ ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin )
12 f1of ⊢ ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) → ( bits ↾ ℕ0 ) : ℕ0 ⟶ ( 𝒫 ℕ0 ∩ Fin ) )
13 11 12 ax-mp ⊢ ( bits ↾ ℕ0 ) : ℕ0 ⟶ ( 𝒫 ℕ0 ∩ Fin )
14 1 2 3 4 5 6 7 8 9 eulerpartlemt0 ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ↔ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 ) )
15 14 biimpi ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 ) )
16 15 simp1d ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝐴 ∈ ( ℕ0 ↑m ℕ ) )
17 nn0ex ⊢ ℕ0 ∈ V
18 nnex ⊢ ℕ ∈ V
19 17 18 elmap ⊢ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) ↔ 𝐴 : ℕ ⟶ ℕ0 )
20 16 19 sylib ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝐴 : ℕ ⟶ ℕ0 )
21 ssrab2 ⊢ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ⊆ ℕ
22 4 21 eqsstri ⊢ 𝐽 ⊆ ℕ
23 fssres ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝐽 ⊆ ℕ ) → ( 𝐴 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 )
24 20 22 23 sylancl ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐴 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 )
25 fco2 ⊢ ( ( ( bits ↾ ℕ0 ) : ℕ0 ⟶ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( 𝐴 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 ) → ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) : 𝐽 ⟶ ( 𝒫 ℕ0 ∩ Fin ) )
26 13 24 25 sylancr ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) : 𝐽 ⟶ ( 𝒫 ℕ0 ∩ Fin ) )
27 17 pwex ⊢ 𝒫 ℕ0 ∈ V
28 27 inex1 ⊢ ( 𝒫 ℕ0 ∩ Fin ) ∈ V
29 18 22 ssexi ⊢ 𝐽 ∈ V
30 28 29 elmap ⊢ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ↔ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) : 𝐽 ⟶ ( 𝒫 ℕ0 ∩ Fin ) )
31 26 30 sylibr ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) )
32 15 simp2d ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ 𝐴 “ ℕ ) ∈ Fin )
33 0nn0 ⊢ 0 ∈ ℕ0
34 suppimacnv ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 0 ∈ ℕ0 ) → ( 𝐴 supp 0 ) = ( ◡ 𝐴 “ ( V ∖ { 0 } ) ) )
35 33 34 mpan2 ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐴 supp 0 ) = ( ◡ 𝐴 “ ( V ∖ { 0 } ) ) )
36 frnsuppeq ⊢ ( ( ℕ ∈ V ∧ 0 ∈ ℕ0 ) → ( 𝐴 : ℕ ⟶ ℕ0 → ( 𝐴 supp 0 ) = ( ◡ 𝐴 “ ( ℕ0 ∖ { 0 } ) ) ) )
37 18 33 36 mp2an ⊢ ( 𝐴 : ℕ ⟶ ℕ0 → ( 𝐴 supp 0 ) = ( ◡ 𝐴 “ ( ℕ0 ∖ { 0 } ) ) )
38 20 37 syl ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐴 supp 0 ) = ( ◡ 𝐴 “ ( ℕ0 ∖ { 0 } ) ) )
39 35 38 eqtr3d ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ 𝐴 “ ( V ∖ { 0 } ) ) = ( ◡ 𝐴 “ ( ℕ0 ∖ { 0 } ) ) )
40 39 eleq1d ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( ◡ 𝐴 “ ( V ∖ { 0 } ) ) ∈ Fin ↔ ( ◡ 𝐴 “ ( ℕ0 ∖ { 0 } ) ) ∈ Fin ) )
41 dfn2 ⊢ ℕ = ( ℕ0 ∖ { 0 } )
42 41 imaeq2i ⊢ ( ◡ 𝐴 “ ℕ ) = ( ◡ 𝐴 “ ( ℕ0 ∖ { 0 } ) )
43 42 eleq1i ⊢ ( ( ◡ 𝐴 “ ℕ ) ∈ Fin ↔ ( ◡ 𝐴 “ ( ℕ0 ∖ { 0 } ) ) ∈ Fin )
44 40 43 bitr4di ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( ◡ 𝐴 “ ( V ∖ { 0 } ) ) ∈ Fin ↔ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) )
45 32 44 mpbird ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ 𝐴 “ ( V ∖ { 0 } ) ) ∈ Fin )
46 resss ⊢ ( 𝐴 ↾ 𝐽 ) ⊆ 𝐴
47 cnvss ⊢ ( ( 𝐴 ↾ 𝐽 ) ⊆ 𝐴 → ◡ ( 𝐴 ↾ 𝐽 ) ⊆ ◡ 𝐴 )
48 imass1 ⊢ ( ◡ ( 𝐴 ↾ 𝐽 ) ⊆ ◡ 𝐴 → ( ◡ ( 𝐴 ↾ 𝐽 ) “ ( V ∖ { 0 } ) ) ⊆ ( ◡ 𝐴 “ ( V ∖ { 0 } ) ) )
49 46 47 48 mp2b ⊢ ( ◡ ( 𝐴 ↾ 𝐽 ) “ ( V ∖ { 0 } ) ) ⊆ ( ◡ 𝐴 “ ( V ∖ { 0 } ) )
50 ssfi ⊢ ( ( ( ◡ 𝐴 “ ( V ∖ { 0 } ) ) ∈ Fin ∧ ( ◡ ( 𝐴 ↾ 𝐽 ) “ ( V ∖ { 0 } ) ) ⊆ ( ◡ 𝐴 “ ( V ∖ { 0 } ) ) ) → ( ◡ ( 𝐴 ↾ 𝐽 ) “ ( V ∖ { 0 } ) ) ∈ Fin )
51 45 49 50 sylancl ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ ( 𝐴 ↾ 𝐽 ) “ ( V ∖ { 0 } ) ) ∈ Fin )
52 cnvco ⊢ ◡ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) = ( ◡ ( 𝐴 ↾ 𝐽 ) ∘ ◡ bits )
53 52 imaeq1i ⊢ ( ◡ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) “ ( V ∖ { ∅ } ) ) = ( ( ◡ ( 𝐴 ↾ 𝐽 ) ∘ ◡ bits ) “ ( V ∖ { ∅ } ) )
54 imaco ⊢ ( ( ◡ ( 𝐴 ↾ 𝐽 ) ∘ ◡ bits ) “ ( V ∖ { ∅ } ) ) = ( ◡ ( 𝐴 ↾ 𝐽 ) “ ( ◡ bits “ ( V ∖ { ∅ } ) ) )
55 53 54 eqtri ⊢ ( ◡ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) “ ( V ∖ { ∅ } ) ) = ( ◡ ( 𝐴 ↾ 𝐽 ) “ ( ◡ bits “ ( V ∖ { ∅ } ) ) )
56 ffun ⊢ ( 𝐴 : ℕ ⟶ ℕ0 → Fun 𝐴 )
57 funres ⊢ ( Fun 𝐴 → Fun ( 𝐴 ↾ 𝐽 ) )
58 20 56 57 3syl ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → Fun ( 𝐴 ↾ 𝐽 ) )
59 ssv ⊢ ( ◡ bits “ V ) ⊆ V
60 ssdif ⊢ ( ( ◡ bits “ V ) ⊆ V → ( ( ◡ bits “ V ) ∖ ( ◡ bits “ { ∅ } ) ) ⊆ ( V ∖ ( ◡ bits “ { ∅ } ) ) )
61 59 60 ax-mp ⊢ ( ( ◡ bits “ V ) ∖ ( ◡ bits “ { ∅ } ) ) ⊆ ( V ∖ ( ◡ bits “ { ∅ } ) )
62 bitsf ⊢ bits : ℤ ⟶ 𝒫 ℕ0
63 ffun ⊢ ( bits : ℤ ⟶ 𝒫 ℕ0 → Fun bits )
64 difpreima ⊢ ( Fun bits → ( ◡ bits “ ( V ∖ { ∅ } ) ) = ( ( ◡ bits “ V ) ∖ ( ◡ bits “ { ∅ } ) ) )
65 62 63 64 mp2b ⊢ ( ◡ bits “ ( V ∖ { ∅ } ) ) = ( ( ◡ bits “ V ) ∖ ( ◡ bits “ { ∅ } ) )
66 bitsf1 ⊢ bits : ℤ –1-1→ 𝒫 ℕ0
67 0z ⊢ 0 ∈ ℤ
68 snssi ⊢ ( 0 ∈ ℤ → { 0 } ⊆ ℤ )
69 67 68 ax-mp ⊢ { 0 } ⊆ ℤ
70 f1imacnv ⊢ ( ( bits : ℤ –1-1→ 𝒫 ℕ0 ∧ { 0 } ⊆ ℤ ) → ( ◡ bits “ ( bits “ { 0 } ) ) = { 0 } )
71 66 69 70 mp2an ⊢ ( ◡ bits “ ( bits “ { 0 } ) ) = { 0 }
72 ffn ⊢ ( bits : ℤ ⟶ 𝒫 ℕ0 → bits Fn ℤ )
73 62 72 ax-mp ⊢ bits Fn ℤ
74 fnsnfv ⊢ ( ( bits Fn ℤ ∧ 0 ∈ ℤ ) → { ( bits ‘ 0 ) } = ( bits “ { 0 } ) )
75 73 67 74 mp2an ⊢ { ( bits ‘ 0 ) } = ( bits “ { 0 } )
76 0bits ⊢ ( bits ‘ 0 ) = ∅
77 76 sneqi ⊢ { ( bits ‘ 0 ) } = { ∅ }
78 75 77 eqtr3i ⊢ ( bits “ { 0 } ) = { ∅ }
79 78 imaeq2i ⊢ ( ◡ bits “ ( bits “ { 0 } ) ) = ( ◡ bits “ { ∅ } )
80 71 79 eqtr3i ⊢ { 0 } = ( ◡ bits “ { ∅ } )
81 80 difeq2i ⊢ ( V ∖ { 0 } ) = ( V ∖ ( ◡ bits “ { ∅ } ) )
82 61 65 81 3sstr4i ⊢ ( ◡ bits “ ( V ∖ { ∅ } ) ) ⊆ ( V ∖ { 0 } )
83 sspreima ⊢ ( ( Fun ( 𝐴 ↾ 𝐽 ) ∧ ( ◡ bits “ ( V ∖ { ∅ } ) ) ⊆ ( V ∖ { 0 } ) ) → ( ◡ ( 𝐴 ↾ 𝐽 ) “ ( ◡ bits “ ( V ∖ { ∅ } ) ) ) ⊆ ( ◡ ( 𝐴 ↾ 𝐽 ) “ ( V ∖ { 0 } ) ) )
84 58 82 83 sylancl ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ ( 𝐴 ↾ 𝐽 ) “ ( ◡ bits “ ( V ∖ { ∅ } ) ) ) ⊆ ( ◡ ( 𝐴 ↾ 𝐽 ) “ ( V ∖ { 0 } ) ) )
85 55 84 eqsstrid ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) “ ( V ∖ { ∅ } ) ) ⊆ ( ◡ ( 𝐴 ↾ 𝐽 ) “ ( V ∖ { 0 } ) ) )
86 ssfi ⊢ ( ( ( ◡ ( 𝐴 ↾ 𝐽 ) “ ( V ∖ { 0 } ) ) ∈ Fin ∧ ( ◡ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) “ ( V ∖ { ∅ } ) ) ⊆ ( ◡ ( 𝐴 ↾ 𝐽 ) “ ( V ∖ { 0 } ) ) ) → ( ◡ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) “ ( V ∖ { ∅ } ) ) ∈ Fin )
87 51 85 86 syl2anc ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) “ ( V ∖ { ∅ } ) ) ∈ Fin )
88 oveq1 ⊢ ( 𝑟 = ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) → ( 𝑟 supp ∅ ) = ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) supp ∅ ) )
89 88 eleq1d ⊢ ( 𝑟 = ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) → ( ( 𝑟 supp ∅ ) ∈ Fin ↔ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) supp ∅ ) ∈ Fin ) )
90 89 6 elrab2 ⊢ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ 𝐻 ↔ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∧ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) supp ∅ ) ∈ Fin ) )
91 zex ⊢ ℤ ∈ V
92 fex ⊢ ( ( bits : ℤ ⟶ 𝒫 ℕ0 ∧ ℤ ∈ V ) → bits ∈ V )
93 62 91 92 mp2an ⊢ bits ∈ V
94 resexg ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐴 ↾ 𝐽 ) ∈ V )
95 coexg ⊢ ( ( bits ∈ V ∧ ( 𝐴 ↾ 𝐽 ) ∈ V ) → ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ V )
96 93 94 95 sylancr ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ V )
97 0ex ⊢ ∅ ∈ V
98 suppimacnv ⊢ ( ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ V ∧ ∅ ∈ V ) → ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) supp ∅ ) = ( ◡ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) “ ( V ∖ { ∅ } ) ) )
99 97 98 mpan2 ⊢ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ V → ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) supp ∅ ) = ( ◡ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) “ ( V ∖ { ∅ } ) ) )
100 99 eleq1d ⊢ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ V → ( ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) supp ∅ ) ∈ Fin ↔ ( ◡ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) “ ( V ∖ { ∅ } ) ) ∈ Fin ) )
101 100 anbi2d ⊢ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ V → ( ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∧ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) supp ∅ ) ∈ Fin ) ↔ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∧ ( ◡ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) “ ( V ∖ { ∅ } ) ) ∈ Fin ) ) )
102 96 101 syl ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∧ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) supp ∅ ) ∈ Fin ) ↔ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∧ ( ◡ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) “ ( V ∖ { ∅ } ) ) ∈ Fin ) ) )
103 90 102 syl5bb ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ 𝐻 ↔ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∧ ( ◡ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) “ ( V ∖ { ∅ } ) ) ∈ Fin ) ) )
104 31 87 103 mpbir2and ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ 𝐻 )