Theorem eulerpartlemt

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 19-Sep-2017)

	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\}$$
Assertion	eulerpartlemt	$$⊢\left({{\mathbb{N}}_0}^J\right)\cap R=\mathrm{ran}\left(m\in \left(T\cap R\right)⟼{m\upharpoonright }_J\right)$$

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		elmapi	$$⊢o\in \left({{\mathbb{N}}_0}^J\right)\to o:J⟶{\mathbb{N}}_0$$
11	10	adantr	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to o:J⟶{\mathbb{N}}_0$$
12		c0ex	$$⊢0\in \mathrm{V}$$
13	12	fconst	$$⊢\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right):\mathbb{N}\setminus J⟶\left\{0\right\}$$
14	13	a1i	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right):\mathbb{N}\setminus J⟶\left\{0\right\}$$
15		disjdif	$$⊢J\cap \left(\mathbb{N}\setminus J\right)=\varnothing$$
16	15	a1i	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to J\cap \left(\mathbb{N}\setminus J\right)=\varnothing$$
17		fun	$$⊢\left(\left(o:J⟶{\mathbb{N}}_0\wedge \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right):\mathbb{N}\setminus J⟶\left\{0\right\}\right)\wedge J\cap \left(\mathbb{N}\setminus J\right)=\varnothing \right)\to \left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\right):J\cup \left(\mathbb{N}\setminus J\right)⟶{\mathbb{N}}_0\cup \left\{0\right\}$$
18	11 14 16 17	syl21anc	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to \left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\right):J\cup \left(\mathbb{N}\setminus J\right)⟶{\mathbb{N}}_0\cup \left\{0\right\}$$
19		ssrab2	$$⊢\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\subseteq \mathbb{N}$$
20	4 19	eqsstri	$$⊢J\subseteq \mathbb{N}$$
21		undif	$$⊢J\subseteq \mathbb{N}\leftrightarrow J\cup \left(\mathbb{N}\setminus J\right)=\mathbb{N}$$
22	20 21	mpbi	$$⊢J\cup \left(\mathbb{N}\setminus J\right)=\mathbb{N}$$
23		0nn0	$$⊢0\in {\mathbb{N}}_0$$
24		snssi	$$⊢0\in {\mathbb{N}}_0\to \left\{0\right\}\subseteq {\mathbb{N}}_0$$
25	23 24	ax-mp	$$⊢\left\{0\right\}\subseteq {\mathbb{N}}_0$$
26		ssequn2	$$⊢\left\{0\right\}\subseteq {\mathbb{N}}_0\leftrightarrow {\mathbb{N}}_0\cup \left\{0\right\}={\mathbb{N}}_0$$
27	25 26	mpbi	$$⊢{\mathbb{N}}_0\cup \left\{0\right\}={\mathbb{N}}_0$$
28	22 27	feq23i	$$⊢\left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\right):J\cup \left(\mathbb{N}\setminus J\right)⟶{\mathbb{N}}_0\cup \left\{0\right\}\leftrightarrow \left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\right):\mathbb{N}⟶{\mathbb{N}}_0$$
29	18 28	sylib	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to \left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\right):\mathbb{N}⟶{\mathbb{N}}_0$$
30		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
31		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
32	30 31	elmap	$$⊢o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\leftrightarrow \left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\right):\mathbb{N}⟶{\mathbb{N}}_0$$
33	29 32	sylibr	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)$$
34		cnvun	$$⊢{\left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\right)}^{-1}=o^{-1}\cup {\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}$$
35	34	imaeq1i	$$⊢{\left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\right)}^{-1}\left[\mathbb{N}\right]=\left(o^{-1}\cup {\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\right)\left[\mathbb{N}\right]$$
36		imaundir	$$⊢\left(o^{-1}\cup {\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\right)\left[\mathbb{N}\right]=o^{-1}\left[\mathbb{N}\right]\cup {\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]$$
37	35 36	eqtri	$$⊢{\left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\right)}^{-1}\left[\mathbb{N}\right]=o^{-1}\left[\mathbb{N}\right]\cup {\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]$$
38		vex	$$⊢o\in \mathrm{V}$$
39		cnveq	$$⊢f=o\to f^{-1}=o^{-1}$$
40	39	imaeq1d	$$⊢f=o\to f^{-1}\left[\mathbb{N}\right]=o^{-1}\left[\mathbb{N}\right]$$
41	40	eleq1d	$$⊢f=o\to \left(f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\leftrightarrow o^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
42	38 41 8	elab2	$$⊢o\in R\leftrightarrow o^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
43	42	biimpi	$$⊢o\in R\to o^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
44	43	adantl	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to o^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
45		cnvxp	$$⊢{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}=\left\{0\right\}\times \left(\mathbb{N}\setminus J\right)$$
46	45	dmeqi	$$⊢\mathrm{dom}{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}=\mathrm{dom}\left(\left\{0\right\}\times \left(\mathbb{N}\setminus J\right)\right)$$
47		2nn	$$⊢2\in \mathbb{N}$$
48		2z	$$⊢2\in \mathbb{Z}$$
49		iddvds	$$⊢2\in \mathbb{Z}\to 2\parallel 2$$
50	48 49	ax-mp	$$⊢2\parallel 2$$
51		breq2	$$⊢z=2\to \left(2\parallel z\leftrightarrow 2\parallel 2\right)$$
52	51	notbid	$$⊢z=2\to \left(\neg 2\parallel z\leftrightarrow \neg 2\parallel 2\right)$$
53	52 4	elrab2	$$⊢2\in J\leftrightarrow \left(2\in \mathbb{N}\wedge \neg 2\parallel 2\right)$$
54	53	simprbi	$$⊢2\in J\to \neg 2\parallel 2$$
55	50 54	mt2	$$⊢\neg 2\in J$$
56		eldif	$$⊢2\in \left(\mathbb{N}\setminus J\right)\leftrightarrow \left(2\in \mathbb{N}\wedge \neg 2\in J\right)$$
57	47 55 56	mpbir2an	$$⊢2\in \left(\mathbb{N}\setminus J\right)$$
58		ne0i	$$⊢2\in \left(\mathbb{N}\setminus J\right)\to \mathbb{N}\setminus J\ne \varnothing$$
59		dmxp	$$⊢\mathbb{N}\setminus J\ne \varnothing \to \mathrm{dom}\left(\left\{0\right\}\times \left(\mathbb{N}\setminus J\right)\right)=\left\{0\right\}$$
60	57 58 59	mp2b	$$⊢\mathrm{dom}\left(\left\{0\right\}\times \left(\mathbb{N}\setminus J\right)\right)=\left\{0\right\}$$
61	46 60	eqtri	$$⊢\mathrm{dom}{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}=\left\{0\right\}$$
62	61	ineq1i	$$⊢\mathrm{dom}{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\cap \mathbb{N}=\left\{0\right\}\cap \mathbb{N}$$
63		incom	$$⊢\mathbb{N}\cap \left\{0\right\}=\left\{0\right\}\cap \mathbb{N}$$
64		0nnn	$$⊢\neg 0\in \mathbb{N}$$
65		disjsn	$$⊢\mathbb{N}\cap \left\{0\right\}=\varnothing \leftrightarrow \neg 0\in \mathbb{N}$$
66	64 65	mpbir	$$⊢\mathbb{N}\cap \left\{0\right\}=\varnothing$$
67	62 63 66	3eqtr2i	$$⊢\mathrm{dom}{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\cap \mathbb{N}=\varnothing$$
68		imadisj	$$⊢{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]=\varnothing \leftrightarrow \mathrm{dom}{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\cap \mathbb{N}=\varnothing$$
69	67 68	mpbir	$$⊢{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]=\varnothing$$
70		0fin	$$⊢\varnothing \in \mathrm{Fin}$$
71	69 70	eqeltri	$$⊢{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
72		unfi	$$⊢\left(o^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\wedge {\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\to o^{-1}\left[\mathbb{N}\right]\cup {\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
73	44 71 72	sylancl	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to o^{-1}\left[\mathbb{N}\right]\cup {\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
74	37 73	eqeltrid	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to {\left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
75		cnvimass	$$⊢o^{-1}\left[\mathbb{N}\right]\subseteq \mathrm{dom}o$$
76	75 11	fssdm	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to o^{-1}\left[\mathbb{N}\right]\subseteq J$$
77		0ss	$$⊢\varnothing \subseteq J$$
78	69 77	eqsstri	$$⊢{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]\subseteq J$$
79	78	a1i	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to {\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]\subseteq J$$
80	76 79	unssd	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to o^{-1}\left[\mathbb{N}\right]\cup {\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]\subseteq J$$
81	37 80	eqsstrid	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to {\left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\right)}^{-1}\left[\mathbb{N}\right]\subseteq J$$
82	1 2 3 4 5 6 7 8 9	eulerpartlemt0	$$⊢o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\in \left(T\cap R\right)\leftrightarrow \left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\wedge {\left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\wedge {\left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\right)}^{-1}\left[\mathbb{N}\right]\subseteq J\right)$$
83	33 74 81 82	syl3anbrc	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\in \left(T\cap R\right)$$
84		resundir	$$⊢{\left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\right)\upharpoonright }_J=\left({o\upharpoonright }_J\right)\cup \left({\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\upharpoonright }_J\right)$$
85		ffn	$$⊢o:J⟶{\mathbb{N}}_0\to oFnJ$$
86		fnresdm	$$⊢oFnJ\to {o\upharpoonright }_J=o$$
87		disjdifr	$$⊢\left(\mathbb{N}\setminus J\right)\cap J=\varnothing$$
88		fnconstg	$$⊢0\in {\mathbb{N}}_0\to \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)Fn\left(\mathbb{N}\setminus J\right)$$
89		fnresdisj	$$⊢\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)Fn\left(\mathbb{N}\setminus J\right)\to \left(\left(\mathbb{N}\setminus J\right)\cap J=\varnothing \leftrightarrow {\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\upharpoonright }_J=\varnothing \right)$$
90	23 88 89	mp2b	$$⊢\left(\mathbb{N}\setminus J\right)\cap J=\varnothing \leftrightarrow {\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\upharpoonright }_J=\varnothing$$
91	87 90	mpbi	$$⊢{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\upharpoonright }_J=\varnothing$$
92	91	a1i	$$⊢oFnJ\to {\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\upharpoonright }_J=\varnothing$$
93	86 92	uneq12d	$$⊢oFnJ\to \left({o\upharpoonright }_J\right)\cup \left({\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\upharpoonright }_J\right)=o\cup \varnothing$$
94	11 85 93	3syl	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to \left({o\upharpoonright }_J\right)\cup \left({\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\upharpoonright }_J\right)=o\cup \varnothing$$
95		un0	$$⊢o\cup \varnothing =o$$
96	94 95	eqtrdi	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to \left({o\upharpoonright }_J\right)\cup \left({\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\upharpoonright }_J\right)=o$$
97	84 96	eqtr2id	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to o={\left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\right)\upharpoonright }_J$$
98		reseq1	$$⊢m=o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\to {m\upharpoonright }_J={\left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\right)\upharpoonright }_J$$
99	98	rspceeqv	$$⊢\left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\in \left(T\cap R\right)\wedge o={\left(o\cup \left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\right)\upharpoonright }_J\right)\to \exists m\in \left(T\cap R\right)o={m\upharpoonright }_J$$
100	83 97 99	syl2anc	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to \exists m\in \left(T\cap R\right)o={m\upharpoonright }_J$$
101		simpr	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to o={m\upharpoonright }_J$$
102		simpl	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to m\in \left(T\cap R\right)$$
103	1 2 3 4 5 6 7 8 9	eulerpartlemt0	$$⊢m\in \left(T\cap R\right)\leftrightarrow \left(m\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\wedge m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\wedge m^{-1}\left[\mathbb{N}\right]\subseteq J\right)$$
104	102 103	sylib	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to \left(m\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\wedge m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\wedge m^{-1}\left[\mathbb{N}\right]\subseteq J\right)$$
105	104	simp1d	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to m\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)$$
106	30 31	elmap	$$⊢m\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\leftrightarrow m:\mathbb{N}⟶{\mathbb{N}}_0$$
107	105 106	sylib	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to m:\mathbb{N}⟶{\mathbb{N}}_0$$
108		fssres	$$⊢\left(m:\mathbb{N}⟶{\mathbb{N}}_0\wedge J\subseteq \mathbb{N}\right)\to \left({m\upharpoonright }_J\right):J⟶{\mathbb{N}}_0$$
109	107 20 108	sylancl	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to \left({m\upharpoonright }_J\right):J⟶{\mathbb{N}}_0$$
110	4 31	rabex2	$$⊢J\in \mathrm{V}$$
111	30 110	elmap	$$⊢{m\upharpoonright }_J\in \left({{\mathbb{N}}_0}^J\right)\leftrightarrow \left({m\upharpoonright }_J\right):J⟶{\mathbb{N}}_0$$
112	109 111	sylibr	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to {m\upharpoonright }_J\in \left({{\mathbb{N}}_0}^J\right)$$
113	101 112	eqeltrd	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to o\in \left({{\mathbb{N}}_0}^J\right)$$
114		ffun	$$⊢m:\mathbb{N}⟶{\mathbb{N}}_0\to \mathrm{Fun}m$$
115		respreima	$$⊢\mathrm{Fun}m\to {\left({m\upharpoonright }_J\right)}^{-1}\left[\mathbb{N}\right]=m^{-1}\left[\mathbb{N}\right]\cap J$$
116	107 114 115	3syl	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to {\left({m\upharpoonright }_J\right)}^{-1}\left[\mathbb{N}\right]=m^{-1}\left[\mathbb{N}\right]\cap J$$
117	104	simp2d	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
118		infi	$$⊢m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\to m^{-1}\left[\mathbb{N}\right]\cap J\in \mathrm{Fin}$$
119	117 118	syl	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to m^{-1}\left[\mathbb{N}\right]\cap J\in \mathrm{Fin}$$
120	116 119	eqeltrd	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to {\left({m\upharpoonright }_J\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
121		vex	$$⊢m\in \mathrm{V}$$
122	121	resex	$$⊢{m\upharpoonright }_J\in \mathrm{V}$$
123		cnveq	$$⊢f={m\upharpoonright }_J\to f^{-1}={\left({m\upharpoonright }_J\right)}^{-1}$$
124	123	imaeq1d	$$⊢f={m\upharpoonright }_J\to f^{-1}\left[\mathbb{N}\right]={\left({m\upharpoonright }_J\right)}^{-1}\left[\mathbb{N}\right]$$
125	124	eleq1d	$$⊢f={m\upharpoonright }_J\to \left(f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\leftrightarrow {\left({m\upharpoonright }_J\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
126	122 125 8	elab2	$$⊢{m\upharpoonright }_J\in R\leftrightarrow {\left({m\upharpoonright }_J\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
127	120 126	sylibr	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to {m\upharpoonright }_J\in R$$
128	101 127	eqeltrd	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to o\in R$$
129	113 128	jca	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to \left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)$$
130	129	rexlimiva	$$⊢\exists m\in \left(T\cap R\right)o={m\upharpoonright }_J\to \left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)$$
131	100 130	impbii	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\leftrightarrow \exists m\in \left(T\cap R\right)o={m\upharpoonright }_J$$
132	131	abbii	$$⊢\left\{o|\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\right\}=\left\{o|\exists m\in \left(T\cap R\right)o={m\upharpoonright }_J\right\}$$
133		df-in	$$⊢\left({{\mathbb{N}}_0}^J\right)\cap R=\left\{o|\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\right\}$$
134		eqid	$$⊢\left(m\in \left(T\cap R\right)⟼{m\upharpoonright }_J\right)=\left(m\in \left(T\cap R\right)⟼{m\upharpoonright }_J\right)$$
135	134	rnmpt	$$⊢\mathrm{ran}\left(m\in \left(T\cap R\right)⟼{m\upharpoonright }_J\right)=\left\{o|\exists m\in \left(T\cap R\right)o={m\upharpoonright }_J\right\}$$
136	132 133 135	3eqtr4i	$$⊢\left({{\mathbb{N}}_0}^J\right)\cap R=\mathrm{ran}\left(m\in \left(T\cap R\right)⟼{m\upharpoonright }_J\right)$$