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({{\mathbb{N}}_0}^{\mathbb{N}}\right)|\left(f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\wedge \sum _{k\in \mathbb{N}}f\left(k\right)k=N\right)\right\}$$
	eulerpart.o	$$⊢O=\left\{g\in P|\forall n\in g^{-1}\left[\mathbb{N}\right]\neg 2\parallel n\right\}$$
	eulerpart.d	$$⊢D=\left\{g\in P|\forall n\in \mathbb{N}g\left(n\right)\le 1\right\}$$
	eulerpart.j	$$⊢J=\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}$$
	eulerpart.f	$$⊢F=\left(x\in J,y\in {\mathbb{N}}_0⟼2^{y}x\right)$$
	eulerpart.h	$$⊢H=\left\{r\in \left({\left(𝒫{\mathbb{N}}_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[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	eulerpart.t	$$⊢T=\left\{f\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|f^{-1}\left[\mathbb{N}\right]\subseteq J\right\}$$
	eulerpart.g	$$⊢G=\left(o\in \left(T\cap R\right)⟼{𝟙}_{\mathbb{N}}\left(F\left[M\left(\mathrm{bits}\circ \left({o\upharpoonright }_J\right)\right)\right]\right)\right)$$
Assertion	eulerpartlemmf	$$⊢A\in \left(T\cap R\right)\to \mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in H$$

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	$$⊢P=\left\{f\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|\left(f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\wedge \sum _{k\in \mathbb{N}}f\left(k\right)k=N\right)\right\}$$
2		eulerpart.o	$$⊢O=\left\{g\in P|\forall n\in g^{-1}\left[\mathbb{N}\right]\neg 2\parallel n\right\}$$
3		eulerpart.d	$$⊢D=\left\{g\in P|\forall n\in \mathbb{N}g\left(n\right)\le 1\right\}$$
4		eulerpart.j	$$⊢J=\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}$$
5		eulerpart.f	$$⊢F=\left(x\in J,y\in {\mathbb{N}}_0⟼2^{y}x\right)$$
6		eulerpart.h	$$⊢H=\left\{r\in \left({\left(𝒫{\mathbb{N}}_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[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
9		eulerpart.t	$$⊢T=\left\{f\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|f^{-1}\left[\mathbb{N}\right]\subseteq J\right\}$$
10		eulerpart.g	$$⊢G=\left(o\in \left(T\cap R\right)⟼{𝟙}_{\mathbb{N}}\left(F\left[M\left(\mathrm{bits}\circ \left({o\upharpoonright }_J\right)\right)\right]\right)\right)$$
11		bitsf1o	$$⊢\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}𝒫{\mathbb{N}}_0\cap \mathrm{Fin}$$
12		f1of	$$⊢\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\to \left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0⟶𝒫{\mathbb{N}}_0\cap \mathrm{Fin}$$
13	11 12	ax-mp	$$⊢\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0⟶𝒫{\mathbb{N}}_0\cap \mathrm{Fin}$$
14	1 2 3 4 5 6 7 8 9	eulerpartlemt0	$$⊢A\in \left(T\cap R\right)\leftrightarrow \left(A\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\wedge A^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\wedge A^{-1}\left[\mathbb{N}\right]\subseteq J\right)$$
15	14	biimpi	$$⊢A\in \left(T\cap R\right)\to \left(A\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\wedge A^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\wedge A^{-1}\left[\mathbb{N}\right]\subseteq J\right)$$
16	15	simp1d	$$⊢A\in \left(T\cap R\right)\to A\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)$$
17		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
18		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
19	17 18	elmap	$$⊢A\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\leftrightarrow A:\mathbb{N}⟶{\mathbb{N}}_0$$
20	16 19	sylib	$$⊢A\in \left(T\cap R\right)\to A:\mathbb{N}⟶{\mathbb{N}}_0$$
21		ssrab2	$$⊢\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\subseteq \mathbb{N}$$
22	4 21	eqsstri	$$⊢J\subseteq \mathbb{N}$$
23		fssres	$$⊢\left(A:\mathbb{N}⟶{\mathbb{N}}_0\wedge J\subseteq \mathbb{N}\right)\to \left({A\upharpoonright }_J\right):J⟶{\mathbb{N}}_0$$
24	20 22 23	sylancl	$$⊢A\in \left(T\cap R\right)\to \left({A\upharpoonright }_J\right):J⟶{\mathbb{N}}_0$$
25		fco2	$$⊢\left(\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0⟶𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\wedge \left({A\upharpoonright }_J\right):J⟶{\mathbb{N}}_0\right)\to \left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right):J⟶𝒫{\mathbb{N}}_0\cap \mathrm{Fin}$$
26	13 24 25	sylancr	$$⊢A\in \left(T\cap R\right)\to \left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right):J⟶𝒫{\mathbb{N}}_0\cap \mathrm{Fin}$$
27	17	pwex	$$⊢𝒫{\mathbb{N}}_0\in \mathrm{V}$$
28	27	inex1	$$⊢𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\in \mathrm{V}$$
29	18 22	ssexi	$$⊢J\in \mathrm{V}$$
30	28 29	elmap	$$⊢\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^J\right)\leftrightarrow \left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right):J⟶𝒫{\mathbb{N}}_0\cap \mathrm{Fin}$$
31	26 30	sylibr	$$⊢A\in \left(T\cap R\right)\to \mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^J\right)$$
32	15	simp2d	$$⊢A\in \left(T\cap R\right)\to A^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
33		0nn0	$$⊢0\in {\mathbb{N}}_0$$
34		suppimacnv	$$⊢\left(A\in \left(T\cap R\right)\wedge 0\in {\mathbb{N}}_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		fsuppeq	$$⊢\left(\mathbb{N}\in \mathrm{V}\wedge 0\in {\mathbb{N}}_0\right)\to \left(A:\mathbb{N}⟶{\mathbb{N}}_0\to A\mathrm{supp}0=A^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]\right)$$
37	18 33 36	mp2an	$$⊢A:\mathbb{N}⟶{\mathbb{N}}_0\to A\mathrm{supp}0=A^{-1}\left[{\mathbb{N}}_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[{\mathbb{N}}_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[{\mathbb{N}}_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}\leftrightarrow A^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]\in \mathrm{Fin}\right)$$
41		dfn2	$$⊢\mathbb{N}={\mathbb{N}}_0\setminus \left\{0\right\}$$
42	41	imaeq2i	$$⊢A^{-1}\left[\mathbb{N}\right]=A^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]$$
43	42	eleq1i	$$⊢A^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\leftrightarrow A^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]\in \mathrm{Fin}$$
44	40 43	bitr4di	$$⊢A\in \left(T\cap R\right)\to \left(A^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]\in \mathrm{Fin}\leftrightarrow A^{-1}\left[\mathbb{N}\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\upharpoonright }_J\subseteq A$$
47		cnvss	$$⊢{A\upharpoonright }_J\subseteq A\to {\left({A\upharpoonright }_J\right)}^{-1}\subseteq A^{-1}$$
48		imass1	$$⊢{\left({A\upharpoonright }_J\right)}^{-1}\subseteq A^{-1}\to {\left({A\upharpoonright }_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\upharpoonright }_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\upharpoonright }_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\upharpoonright }_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\upharpoonright }_J\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]\in \mathrm{Fin}$$
52		cnvco	$$⊢{\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)}^{-1}={\left({A\upharpoonright }_J\right)}^{-1}\circ {\mathrm{bits}}^{-1}$$
53	52	imaeq1i	$$⊢{\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]=\left({\left({A\upharpoonright }_J\right)}^{-1}\circ {\mathrm{bits}}^{-1}\right)\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]$$
54		imaco	$$⊢\left({\left({A\upharpoonright }_J\right)}^{-1}\circ {\mathrm{bits}}^{-1}\right)\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]={\left({A\upharpoonright }_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\upharpoonright }_J\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]={\left({A\upharpoonright }_J\right)}^{-1}\left[{\mathrm{bits}}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\right]$$
56		ffun	$$⊢A:\mathbb{N}⟶{\mathbb{N}}_0\to \mathrm{Fun}A$$
57		funres	$$⊢\mathrm{Fun}A\to \mathrm{Fun}\left({A\upharpoonright }_J\right)$$
58	20 56 57	3syl	$$⊢A\in \left(T\cap R\right)\to \mathrm{Fun}\left({A\upharpoonright }_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}:\mathbb{Z}⟶𝒫{\mathbb{N}}_0$$
63		ffun	$$⊢\mathrm{bits}:\mathbb{Z}⟶𝒫{\mathbb{N}}_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}:\mathbb{Z}\underset{1-1}{⟶}𝒫{\mathbb{N}}_0$$
67		0z	$$⊢0\in \mathbb{Z}$$
68		snssi	$$⊢0\in \mathbb{Z}\to \left\{0\right\}\subseteq \mathbb{Z}$$
69	67 68	ax-mp	$$⊢\left\{0\right\}\subseteq \mathbb{Z}$$
70		f1imacnv	$$⊢\left(\mathrm{bits}:\mathbb{Z}\underset{1-1}{⟶}𝒫{\mathbb{N}}_0\wedge \left\{0\right\}\subseteq \mathbb{Z}\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}:\mathbb{Z}⟶𝒫{\mathbb{N}}_0\to \mathrm{bits}Fn\mathbb{Z}$$
73	62 72	ax-mp	$$⊢\mathrm{bits}Fn\mathbb{Z}$$
74		fnsnfv	$$⊢\left(\mathrm{bits}Fn\mathbb{Z}\wedge 0\in \mathbb{Z}\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\upharpoonright }_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\upharpoonright }_J\right)}^{-1}\left[{\mathrm{bits}}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\right]\subseteq {\left({A\upharpoonright }_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\upharpoonright }_J\right)}^{-1}\left[{\mathrm{bits}}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\right]\subseteq {\left({A\upharpoonright }_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\upharpoonright }_J\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\subseteq {\left({A\upharpoonright }_J\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]$$
86		ssfi	$$⊢\left({\left({A\upharpoonright }_J\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]\in \mathrm{Fin}\wedge {\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\subseteq {\left({A\upharpoonright }_J\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]\right)\to {\left(\mathrm{bits}\circ \left({A\upharpoonright }_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\upharpoonright }_J\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\in \mathrm{Fin}$$
88		oveq1	$$⊢r=\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\to r\mathrm{supp}\varnothing =\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\mathrm{supp}\varnothing$$
89	88	eleq1d	$$⊢r=\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\to \left(r\mathrm{supp}\varnothing \in \mathrm{Fin}\leftrightarrow \left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\mathrm{supp}\varnothing \in \mathrm{Fin}\right)$$
90	89 6	elrab2	$$⊢\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in H\leftrightarrow \left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^J\right)\wedge \left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\mathrm{supp}\varnothing \in \mathrm{Fin}\right)$$
91		zex	$$⊢\mathbb{Z}\in \mathrm{V}$$
92		fex	$$⊢\left(\mathrm{bits}:\mathbb{Z}⟶𝒫{\mathbb{N}}_0\wedge \mathbb{Z}\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\upharpoonright }_J\in \mathrm{V}$$
95		coexg	$$⊢\left(\mathrm{bits}\in \mathrm{V}\wedge {A\upharpoonright }_J\in \mathrm{V}\right)\to \mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in \mathrm{V}$$
96	93 94 95	sylancr	$$⊢A\in \left(T\cap R\right)\to \mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in \mathrm{V}$$
97		0ex	$$⊢\varnothing \in \mathrm{V}$$
98		suppimacnv	$$⊢\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in \mathrm{V}\wedge \varnothing \in \mathrm{V}\right)\to \left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\mathrm{supp}\varnothing ={\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]$$
99	97 98	mpan2	$$⊢\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in \mathrm{V}\to \left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\mathrm{supp}\varnothing ={\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]$$
100	99	eleq1d	$$⊢\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in \mathrm{V}\to \left(\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\mathrm{supp}\varnothing \in \mathrm{Fin}\leftrightarrow {\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\in \mathrm{Fin}\right)$$
101	100	anbi2d	$$⊢\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in \mathrm{V}\to \left(\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^J\right)\wedge \left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\mathrm{supp}\varnothing \in \mathrm{Fin}\right)\leftrightarrow \left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^J\right)\wedge {\left(\mathrm{bits}\circ \left({A\upharpoonright }_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\upharpoonright }_J\right)\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^J\right)\wedge \left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\mathrm{supp}\varnothing \in \mathrm{Fin}\right)\leftrightarrow \left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^J\right)\wedge {\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]\in \mathrm{Fin}\right)\right)$$
103	90 102	bitrid	$$⊢A\in \left(T\cap R\right)\to \left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in H\leftrightarrow \left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^J\right)\wedge {\left(\mathrm{bits}\circ \left({A\upharpoonright }_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\upharpoonright }_J\right)\in H$$