# 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 ${⊢}{P}=\left\{{f}\in \left({{ℕ}_{0}}^{ℕ}\right)|\left({{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\wedge \sum _{{k}\in ℕ}{f}\left({k}\right){k}={N}\right)\right\}$
eulerpart.o ${⊢}{O}=\left\{{g}\in {P}|\forall {n}\in {{g}}^{-1}\left[ℕ\right]\phantom{\rule{.4em}{0ex}}¬2\parallel {n}\right\}$
eulerpart.d ${⊢}{D}=\left\{{g}\in {P}|\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({n}\right)\le 1\right\}$
eulerpart.j ${⊢}{J}=\left\{{z}\in ℕ|¬2\parallel {z}\right\}$
eulerpart.f ${⊢}{F}=\left({x}\in {J},{y}\in {ℕ}_{0}⟼{2}^{{y}}{x}\right)$
eulerpart.h ${⊢}{H}=\left\{{r}\in \left({\left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)}^{{J}}\right)|{r}\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}$
eulerpart.m ${⊢}{M}=\left({r}\in {H}⟼\left\{⟨{x},{y}⟩|\left({x}\in {J}\wedge {y}\in {r}\left({x}\right)\right)\right\}\right)$
eulerpart.r ${⊢}{R}=\left\{{f}|{{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
eulerpart.t ${⊢}{T}=\left\{{f}\in \left({{ℕ}_{0}}^{ℕ}\right)|{{f}}^{-1}\left[ℕ\right]\subseteq {J}\right\}$
eulerpart.g ${⊢}{G}=\left({o}\in \left({T}\cap {R}\right)⟼{𝟙}_{ℕ}\left({F}\left[{M}\left(\mathrm{bits}\circ \left({{o}↾}_{{J}}\right)\right)\right]\right)\right)$
Assertion eulerpartlemmf ${⊢}{A}\in \left({T}\cap {R}\right)\to \mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in {H}$

### Proof

Step Hyp Ref Expression
1 eulerpart.p ${⊢}{P}=\left\{{f}\in \left({{ℕ}_{0}}^{ℕ}\right)|\left({{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\wedge \sum _{{k}\in ℕ}{f}\left({k}\right){k}={N}\right)\right\}$
2 eulerpart.o ${⊢}{O}=\left\{{g}\in {P}|\forall {n}\in {{g}}^{-1}\left[ℕ\right]\phantom{\rule{.4em}{0ex}}¬2\parallel {n}\right\}$
3 eulerpart.d ${⊢}{D}=\left\{{g}\in {P}|\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({n}\right)\le 1\right\}$
4 eulerpart.j ${⊢}{J}=\left\{{z}\in ℕ|¬2\parallel {z}\right\}$
5 eulerpart.f ${⊢}{F}=\left({x}\in {J},{y}\in {ℕ}_{0}⟼{2}^{{y}}{x}\right)$
6 eulerpart.h ${⊢}{H}=\left\{{r}\in \left({\left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)}^{{J}}\right)|{r}\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}$
7 eulerpart.m ${⊢}{M}=\left({r}\in {H}⟼\left\{⟨{x},{y}⟩|\left({x}\in {J}\wedge {y}\in {r}\left({x}\right)\right)\right\}\right)$
8 eulerpart.r ${⊢}{R}=\left\{{f}|{{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
9 eulerpart.t ${⊢}{T}=\left\{{f}\in \left({{ℕ}_{0}}^{ℕ}\right)|{{f}}^{-1}\left[ℕ\right]\subseteq {J}\right\}$
10 eulerpart.g ${⊢}{G}=\left({o}\in \left({T}\cap {R}\right)⟼{𝟙}_{ℕ}\left({F}\left[{M}\left(\mathrm{bits}\circ \left({{o}↾}_{{J}}\right)\right)\right]\right)\right)$
11 bitsf1o ${⊢}\left({\mathrm{bits}↾}_{{ℕ}_{0}}\right):{ℕ}_{0}\underset{1-1 onto}{⟶}𝒫{ℕ}_{0}\cap \mathrm{Fin}$
12 f1of ${⊢}\left({\mathrm{bits}↾}_{{ℕ}_{0}}\right):{ℕ}_{0}\underset{1-1 onto}{⟶}𝒫{ℕ}_{0}\cap \mathrm{Fin}\to \left({\mathrm{bits}↾}_{{ℕ}_{0}}\right):{ℕ}_{0}⟶𝒫{ℕ}_{0}\cap \mathrm{Fin}$
13 11 12 ax-mp ${⊢}\left({\mathrm{bits}↾}_{{ℕ}_{0}}\right):{ℕ}_{0}⟶𝒫{ℕ}_{0}\cap \mathrm{Fin}$
14 1 2 3 4 5 6 7 8 9 eulerpartlemt0 ${⊢}{A}\in \left({T}\cap {R}\right)↔\left({A}\in \left({{ℕ}_{0}}^{ℕ}\right)\wedge {{A}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\wedge {{A}}^{-1}\left[ℕ\right]\subseteq {J}\right)$
15 14 biimpi ${⊢}{A}\in \left({T}\cap {R}\right)\to \left({A}\in \left({{ℕ}_{0}}^{ℕ}\right)\wedge {{A}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\wedge {{A}}^{-1}\left[ℕ\right]\subseteq {J}\right)$
16 15 simp1d ${⊢}{A}\in \left({T}\cap {R}\right)\to {A}\in \left({{ℕ}_{0}}^{ℕ}\right)$
17 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
18 nnex ${⊢}ℕ\in \mathrm{V}$
19 17 18 elmap ${⊢}{A}\in \left({{ℕ}_{0}}^{ℕ}\right)↔{A}:ℕ⟶{ℕ}_{0}$
20 16 19 sylib ${⊢}{A}\in \left({T}\cap {R}\right)\to {A}:ℕ⟶{ℕ}_{0}$
21 ssrab2 ${⊢}\left\{{z}\in ℕ|¬2\parallel {z}\right\}\subseteq ℕ$
22 4 21 eqsstri ${⊢}{J}\subseteq ℕ$
23 fssres ${⊢}\left({A}:ℕ⟶{ℕ}_{0}\wedge {J}\subseteq ℕ\right)\to \left({{A}↾}_{{J}}\right):{J}⟶{ℕ}_{0}$
24 20 22 23 sylancl ${⊢}{A}\in \left({T}\cap {R}\right)\to \left({{A}↾}_{{J}}\right):{J}⟶{ℕ}_{0}$
25 fco2 ${⊢}\left(\left({\mathrm{bits}↾}_{{ℕ}_{0}}\right):{ℕ}_{0}⟶𝒫{ℕ}_{0}\cap \mathrm{Fin}\wedge \left({{A}↾}_{{J}}\right):{J}⟶{ℕ}_{0}\right)\to \left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right):{J}⟶𝒫{ℕ}_{0}\cap \mathrm{Fin}$
26 13 24 25 sylancr ${⊢}{A}\in \left({T}\cap {R}\right)\to \left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right):{J}⟶𝒫{ℕ}_{0}\cap \mathrm{Fin}$
27 17 pwex ${⊢}𝒫{ℕ}_{0}\in \mathrm{V}$
28 27 inex1 ${⊢}𝒫{ℕ}_{0}\cap \mathrm{Fin}\in \mathrm{V}$
29 18 22 ssexi ${⊢}{J}\in \mathrm{V}$
30 28 29 elmap ${⊢}\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in \left({\left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)}^{{J}}\right)↔\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right):{J}⟶𝒫{ℕ}_{0}\cap \mathrm{Fin}$
31 26 30 sylibr ${⊢}{A}\in \left({T}\cap {R}\right)\to \mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in \left({\left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)}^{{J}}\right)$
32 15 simp2d ${⊢}{A}\in \left({T}\cap {R}\right)\to {{A}}^{-1}\left[ℕ\right]\in \mathrm{Fin}$
33 0nn0 ${⊢}0\in {ℕ}_{0}$
34 suppimacnv ${⊢}\left({A}\in \left({T}\cap {R}\right)\wedge 0\in {ℕ}_{0}\right)\to {A}\mathrm{supp}0={{A}}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]$
35 33 34 mpan2 ${⊢}{A}\in \left({T}\cap {R}\right)\to {A}\mathrm{supp}0={{A}}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]$
36 frnsuppeq ${⊢}\left(ℕ\in \mathrm{V}\wedge 0\in {ℕ}_{0}\right)\to \left({A}:ℕ⟶{ℕ}_{0}\to {A}\mathrm{supp}0={{A}}^{-1}\left[{ℕ}_{0}\setminus \left\{0\right\}\right]\right)$
37 18 33 36 mp2an ${⊢}{A}:ℕ⟶{ℕ}_{0}\to {A}\mathrm{supp}0={{A}}^{-1}\left[{ℕ}_{0}\setminus \left\{0\right\}\right]$
38 20 37 syl ${⊢}{A}\in \left({T}\cap {R}\right)\to {A}\mathrm{supp}0={{A}}^{-1}\left[{ℕ}_{0}\setminus \left\{0\right\}\right]$
39 35 38 eqtr3d ${⊢}{A}\in \left({T}\cap {R}\right)\to {{A}}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]={{A}}^{-1}\left[{ℕ}_{0}\setminus \left\{0\right\}\right]$
40 39 eleq1d ${⊢}{A}\in \left({T}\cap {R}\right)\to \left({{A}}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]\in \mathrm{Fin}↔{{A}}^{-1}\left[{ℕ}_{0}\setminus \left\{0\right\}\right]\in \mathrm{Fin}\right)$
41 dfn2 ${⊢}ℕ={ℕ}_{0}\setminus \left\{0\right\}$
42 41 imaeq2i ${⊢}{{A}}^{-1}\left[ℕ\right]={{A}}^{-1}\left[{ℕ}_{0}\setminus \left\{0\right\}\right]$
43 42 eleq1i ${⊢}{{A}}^{-1}\left[ℕ\right]\in \mathrm{Fin}↔{{A}}^{-1}\left[{ℕ}_{0}\setminus \left\{0\right\}\right]\in \mathrm{Fin}$
44 40 43 syl6bbr ${⊢}{A}\in \left({T}\cap {R}\right)\to \left({{A}}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]\in \mathrm{Fin}↔{{A}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right)$
45 32 44 mpbird ${⊢}{A}\in \left({T}\cap {R}\right)\to {{A}}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]\in \mathrm{Fin}$
46 resss ${⊢}{{A}↾}_{{J}}\subseteq {A}$
47 cnvss ${⊢}{{A}↾}_{{J}}\subseteq {A}\to {\left({{A}↾}_{{J}}\right)}^{-1}\subseteq {{A}}^{-1}$
48 imass1 ${⊢}{\left({{A}↾}_{{J}}\right)}^{-1}\subseteq {{A}}^{-1}\to {\left({{A}↾}_{{J}}\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]\subseteq {{A}}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]$
49 46 47 48 mp2b ${⊢}{\left({{A}↾}_{{J}}\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]\subseteq {{A}}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]$
50 ssfi ${⊢}\left({{A}}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]\in \mathrm{Fin}\wedge {\left({{A}↾}_{{J}}\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]\subseteq {{A}}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]\right)\to {\left({{A}↾}_{{J}}\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]\in \mathrm{Fin}$
51 45 49 50 sylancl ${⊢}{A}\in \left({T}\cap {R}\right)\to {\left({{A}↾}_{{J}}\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]\in \mathrm{Fin}$
52 cnvco ${⊢}{\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)}^{-1}={\left({{A}↾}_{{J}}\right)}^{-1}\circ {\mathrm{bits}}^{-1}$
53 52 imaeq1i ${⊢}{\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]=\left({\left({{A}↾}_{{J}}\right)}^{-1}\circ {\mathrm{bits}}^{-1}\right)\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]$
54 imaco ${⊢}\left({\left({{A}↾}_{{J}}\right)}^{-1}\circ {\mathrm{bits}}^{-1}\right)\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]={\left({{A}↾}_{{J}}\right)}^{-1}\left[{\mathrm{bits}}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\right]$
55 53 54 eqtri ${⊢}{\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]={\left({{A}↾}_{{J}}\right)}^{-1}\left[{\mathrm{bits}}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\right]$
56 ffun ${⊢}{A}:ℕ⟶{ℕ}_{0}\to \mathrm{Fun}{A}$
57 funres ${⊢}\mathrm{Fun}{A}\to \mathrm{Fun}\left({{A}↾}_{{J}}\right)$
58 20 56 57 3syl ${⊢}{A}\in \left({T}\cap {R}\right)\to \mathrm{Fun}\left({{A}↾}_{{J}}\right)$
59 ssv ${⊢}{\mathrm{bits}}^{-1}\left[\mathrm{V}\right]\subseteq \mathrm{V}$
60 ssdif ${⊢}{\mathrm{bits}}^{-1}\left[\mathrm{V}\right]\subseteq \mathrm{V}\to {\mathrm{bits}}^{-1}\left[\mathrm{V}\right]\setminus {\mathrm{bits}}^{-1}\left[\left\{\varnothing \right\}\right]\subseteq \mathrm{V}\setminus {\mathrm{bits}}^{-1}\left[\left\{\varnothing \right\}\right]$
61 59 60 ax-mp ${⊢}{\mathrm{bits}}^{-1}\left[\mathrm{V}\right]\setminus {\mathrm{bits}}^{-1}\left[\left\{\varnothing \right\}\right]\subseteq \mathrm{V}\setminus {\mathrm{bits}}^{-1}\left[\left\{\varnothing \right\}\right]$
62 bitsf ${⊢}\mathrm{bits}:ℤ⟶𝒫{ℕ}_{0}$
63 ffun ${⊢}\mathrm{bits}:ℤ⟶𝒫{ℕ}_{0}\to \mathrm{Fun}\mathrm{bits}$
64 difpreima ${⊢}\mathrm{Fun}\mathrm{bits}\to {\mathrm{bits}}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]={\mathrm{bits}}^{-1}\left[\mathrm{V}\right]\setminus {\mathrm{bits}}^{-1}\left[\left\{\varnothing \right\}\right]$
65 62 63 64 mp2b ${⊢}{\mathrm{bits}}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]={\mathrm{bits}}^{-1}\left[\mathrm{V}\right]\setminus {\mathrm{bits}}^{-1}\left[\left\{\varnothing \right\}\right]$
66 bitsf1 ${⊢}\mathrm{bits}:ℤ\underset{1-1}{⟶}𝒫{ℕ}_{0}$
67 0z ${⊢}0\in ℤ$
68 snssi ${⊢}0\in ℤ\to \left\{0\right\}\subseteq ℤ$
69 67 68 ax-mp ${⊢}\left\{0\right\}\subseteq ℤ$
70 f1imacnv ${⊢}\left(\mathrm{bits}:ℤ\underset{1-1}{⟶}𝒫{ℕ}_{0}\wedge \left\{0\right\}\subseteq ℤ\right)\to {\mathrm{bits}}^{-1}\left[\mathrm{bits}\left[\left\{0\right\}\right]\right]=\left\{0\right\}$
71 66 69 70 mp2an ${⊢}{\mathrm{bits}}^{-1}\left[\mathrm{bits}\left[\left\{0\right\}\right]\right]=\left\{0\right\}$
72 ffn ${⊢}\mathrm{bits}:ℤ⟶𝒫{ℕ}_{0}\to \mathrm{bits}Fnℤ$
73 62 72 ax-mp ${⊢}\mathrm{bits}Fnℤ$
74 fnsnfv ${⊢}\left(\mathrm{bits}Fnℤ\wedge 0\in ℤ\right)\to \left\{\mathrm{bits}\left(0\right)\right\}=\mathrm{bits}\left[\left\{0\right\}\right]$
75 73 67 74 mp2an ${⊢}\left\{\mathrm{bits}\left(0\right)\right\}=\mathrm{bits}\left[\left\{0\right\}\right]$
76 0bits ${⊢}\mathrm{bits}\left(0\right)=\varnothing$
77 76 sneqi ${⊢}\left\{\mathrm{bits}\left(0\right)\right\}=\left\{\varnothing \right\}$
78 75 77 eqtr3i ${⊢}\mathrm{bits}\left[\left\{0\right\}\right]=\left\{\varnothing \right\}$
79 78 imaeq2i ${⊢}{\mathrm{bits}}^{-1}\left[\mathrm{bits}\left[\left\{0\right\}\right]\right]={\mathrm{bits}}^{-1}\left[\left\{\varnothing \right\}\right]$
80 71 79 eqtr3i ${⊢}\left\{0\right\}={\mathrm{bits}}^{-1}\left[\left\{\varnothing \right\}\right]$
81 80 difeq2i ${⊢}\mathrm{V}\setminus \left\{0\right\}=\mathrm{V}\setminus {\mathrm{bits}}^{-1}\left[\left\{\varnothing \right\}\right]$
82 61 65 81 3sstr4i ${⊢}{\mathrm{bits}}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\subseteq \mathrm{V}\setminus \left\{0\right\}$
83 sspreima ${⊢}\left(\mathrm{Fun}\left({{A}↾}_{{J}}\right)\wedge {\mathrm{bits}}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\subseteq \mathrm{V}\setminus \left\{0\right\}\right)\to {\left({{A}↾}_{{J}}\right)}^{-1}\left[{\mathrm{bits}}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\right]\subseteq {\left({{A}↾}_{{J}}\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]$
84 58 82 83 sylancl ${⊢}{A}\in \left({T}\cap {R}\right)\to {\left({{A}↾}_{{J}}\right)}^{-1}\left[{\mathrm{bits}}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\right]\subseteq {\left({{A}↾}_{{J}}\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]$
85 55 84 eqsstrid ${⊢}{A}\in \left({T}\cap {R}\right)\to {\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\subseteq {\left({{A}↾}_{{J}}\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]$
86 ssfi ${⊢}\left({\left({{A}↾}_{{J}}\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]\in \mathrm{Fin}\wedge {\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\subseteq {\left({{A}↾}_{{J}}\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]\right)\to {\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\in \mathrm{Fin}$
87 51 85 86 syl2anc ${⊢}{A}\in \left({T}\cap {R}\right)\to {\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\in \mathrm{Fin}$
88 oveq1 ${⊢}{r}=\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\to {r}\mathrm{supp}\varnothing =\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)\mathrm{supp}\varnothing$
89 88 eleq1d ${⊢}{r}=\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\to \left({r}\mathrm{supp}\varnothing \in \mathrm{Fin}↔\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)\mathrm{supp}\varnothing \in \mathrm{Fin}\right)$
90 89 6 elrab2 ${⊢}\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in {H}↔\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in \left({\left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)}^{{J}}\right)\wedge \left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)\mathrm{supp}\varnothing \in \mathrm{Fin}\right)$
91 zex ${⊢}ℤ\in \mathrm{V}$
92 fex ${⊢}\left(\mathrm{bits}:ℤ⟶𝒫{ℕ}_{0}\wedge ℤ\in \mathrm{V}\right)\to \mathrm{bits}\in \mathrm{V}$
93 62 91 92 mp2an ${⊢}\mathrm{bits}\in \mathrm{V}$
94 resexg ${⊢}{A}\in \left({T}\cap {R}\right)\to {{A}↾}_{{J}}\in \mathrm{V}$
95 coexg ${⊢}\left(\mathrm{bits}\in \mathrm{V}\wedge {{A}↾}_{{J}}\in \mathrm{V}\right)\to \mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in \mathrm{V}$
96 93 94 95 sylancr ${⊢}{A}\in \left({T}\cap {R}\right)\to \mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in \mathrm{V}$
97 0ex ${⊢}\varnothing \in \mathrm{V}$
98 suppimacnv ${⊢}\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in \mathrm{V}\wedge \varnothing \in \mathrm{V}\right)\to \left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)\mathrm{supp}\varnothing ={\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]$
99 97 98 mpan2 ${⊢}\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in \mathrm{V}\to \left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)\mathrm{supp}\varnothing ={\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]$
100 99 eleq1d ${⊢}\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in \mathrm{V}\to \left(\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)\mathrm{supp}\varnothing \in \mathrm{Fin}↔{\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\in \mathrm{Fin}\right)$
101 100 anbi2d ${⊢}\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in \mathrm{V}\to \left(\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in \left({\left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)}^{{J}}\right)\wedge \left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)\mathrm{supp}\varnothing \in \mathrm{Fin}\right)↔\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in \left({\left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)}^{{J}}\right)\wedge {\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\in \mathrm{Fin}\right)\right)$
102 96 101 syl ${⊢}{A}\in \left({T}\cap {R}\right)\to \left(\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in \left({\left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)}^{{J}}\right)\wedge \left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)\mathrm{supp}\varnothing \in \mathrm{Fin}\right)↔\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in \left({\left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)}^{{J}}\right)\wedge {\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\in \mathrm{Fin}\right)\right)$
103 90 102 syl5bb ${⊢}{A}\in \left({T}\cap {R}\right)\to \left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in {H}↔\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in \left({\left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)}^{{J}}\right)\wedge {\left(\mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\in \mathrm{Fin}\right)\right)$
104 31 87 103 mpbir2and ${⊢}{A}\in \left({T}\cap {R}\right)\to \mathrm{bits}\circ \left({{A}↾}_{{J}}\right)\in {H}$