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	bilani	$$⊢\left(o\in \left({{\mathbb{N}}_0}^J\right)\wedge o\in R\right)\to o^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
44		cnvxp	$$⊢{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}=\left\{0\right\}\times \left(\mathbb{N}\setminus J\right)$$
45	44	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)$$
46		2nn	$$⊢2\in \mathbb{N}$$
47		2z	$$⊢2\in \mathbb{Z}$$
48		iddvds	$$⊢2\in \mathbb{Z}\to 2\parallel 2$$
49	47 48	ax-mp	$$⊢2\parallel 2$$
50		breq2	$$⊢z=2\to \left(2\parallel z\leftrightarrow 2\parallel 2\right)$$
51	50	notbid	$$⊢z=2\to \left(\neg 2\parallel z\leftrightarrow \neg 2\parallel 2\right)$$
52	51 4	elrab2	$$⊢2\in J\leftrightarrow \left(2\in \mathbb{N}\wedge \neg 2\parallel 2\right)$$
53	52	simprbi	$$⊢2\in J\to \neg 2\parallel 2$$
54	49 53	mt2	$$⊢\neg 2\in J$$
55		eldif	$$⊢2\in \left(\mathbb{N}\setminus J\right)\leftrightarrow \left(2\in \mathbb{N}\wedge \neg 2\in J\right)$$
56	46 54 55	mpbir2an	$$⊢2\in \left(\mathbb{N}\setminus J\right)$$
57		ne0i	$$⊢2\in \left(\mathbb{N}\setminus J\right)\to \mathbb{N}\setminus J\ne \varnothing$$
58		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\}$$
59	56 57 58	mp2b	$$⊢\mathrm{dom}\left(\left\{0\right\}\times \left(\mathbb{N}\setminus J\right)\right)=\left\{0\right\}$$
60	45 59	eqtri	$$⊢\mathrm{dom}{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}=\left\{0\right\}$$
61	60	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}$$
62		incom	$$⊢\mathbb{N}\cap \left\{0\right\}=\left\{0\right\}\cap \mathbb{N}$$
63		0nnn	$$⊢\neg 0\in \mathbb{N}$$
64		disjsn	$$⊢\mathbb{N}\cap \left\{0\right\}=\varnothing \leftrightarrow \neg 0\in \mathbb{N}$$
65	63 64	mpbir	$$⊢\mathbb{N}\cap \left\{0\right\}=\varnothing$$
66	61 62 65	3eqtr2i	$$⊢\mathrm{dom}{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\cap \mathbb{N}=\varnothing$$
67		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$$
68	66 67	mpbir	$$⊢{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]=\varnothing$$
69		0fi	$$⊢\varnothing \in \mathrm{Fin}$$
70	68 69	eqeltri	$$⊢{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
71		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}$$
72	43 70 71	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}$$
73	37 72	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}$$
74		cnvimass	$$⊢o^{-1}\left[\mathbb{N}\right]\subseteq \mathrm{dom}o$$
75	74 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$$
76		0ss	$$⊢\varnothing \subseteq J$$
77	68 76	eqsstri	$$⊢{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)}^{-1}\left[\mathbb{N}\right]\subseteq J$$
78	77	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$$
79	75 78	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$$
80	37 79	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$$
81	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)$$
82	33 73 80 81	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)$$
83		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)$$
84		ffn	$$⊢o:J⟶{\mathbb{N}}_0\to oFnJ$$
85		fnresdm	$$⊢oFnJ\to {o\upharpoonright }_J=o$$
86		disjdifr	$$⊢\left(\mathbb{N}\setminus J\right)\cap J=\varnothing$$
87		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)$$
88		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)$$
89	23 87 88	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$$
90	86 89	mpbi	$$⊢{\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\upharpoonright }_J=\varnothing$$
91	90	a1i	$$⊢oFnJ\to {\left(\left(\mathbb{N}\setminus J\right)\times \left\{0\right\}\right)\upharpoonright }_J=\varnothing$$
92	85 91	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$$
93	11 84 92	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$$
94		un0	$$⊢o\cup \varnothing =o$$
95	93 94	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$$
96	83 95	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$$
97		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$$
98	97	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$$
99	82 96 98	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$$
100		simpr	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to o={m\upharpoonright }_J$$
101	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)$$
102	101	birani	$$⊢\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)$$
103	102	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)$$
104	30 31	elmap	$$⊢m\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\leftrightarrow m:\mathbb{N}⟶{\mathbb{N}}_0$$
105	103 104	sylib	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to m:\mathbb{N}⟶{\mathbb{N}}_0$$
106		fssres	$$⊢\left(m:\mathbb{N}⟶{\mathbb{N}}_0\wedge J\subseteq \mathbb{N}\right)\to \left({m\upharpoonright }_J\right):J⟶{\mathbb{N}}_0$$
107	105 20 106	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$$
108	4 31	rabex2	$$⊢J\in \mathrm{V}$$
109	30 108	elmap	$$⊢{m\upharpoonright }_J\in \left({{\mathbb{N}}_0}^J\right)\leftrightarrow \left({m\upharpoonright }_J\right):J⟶{\mathbb{N}}_0$$
110	107 109	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)$$
111	100 110	eqeltrd	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to o\in \left({{\mathbb{N}}_0}^J\right)$$
112		ffun	$$⊢m:\mathbb{N}⟶{\mathbb{N}}_0\to \mathrm{Fun}m$$
113		respreima	$$⊢\mathrm{Fun}m\to {\left({m\upharpoonright }_J\right)}^{-1}\left[\mathbb{N}\right]=m^{-1}\left[\mathbb{N}\right]\cap J$$
114	105 112 113	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$$
115	102	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}$$
116		infi	$$⊢m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\to m^{-1}\left[\mathbb{N}\right]\cap J\in \mathrm{Fin}$$
117	115 116	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}$$
118	114 117	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}$$
119		vex	$$⊢m\in \mathrm{V}$$
120	119	resex	$$⊢{m\upharpoonright }_J\in \mathrm{V}$$
121		cnveq	$$⊢f={m\upharpoonright }_J\to f^{-1}={\left({m\upharpoonright }_J\right)}^{-1}$$
122	121	imaeq1d	$$⊢f={m\upharpoonright }_J\to f^{-1}\left[\mathbb{N}\right]={\left({m\upharpoonright }_J\right)}^{-1}\left[\mathbb{N}\right]$$
123	122	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)$$
124	120 123 8	elab2	$$⊢{m\upharpoonright }_J\in R\leftrightarrow {\left({m\upharpoonright }_J\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
125	118 124	sylibr	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to {m\upharpoonright }_J\in R$$
126	100 125	eqeltrd	$$⊢\left(m\in \left(T\cap R\right)\wedge o={m\upharpoonright }_J\right)\to o\in R$$
127	111 126	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)$$
128	127	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)$$
129	99 128	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$$
130	129	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\}$$
131		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\}$$
132		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)$$
133	132	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\}$$
134	130 131 133	3eqtr4i	$$⊢\left({{\mathbb{N}}_0}^J\right)\cap R=\mathrm{ran}\left(m\in \left(T\cap R\right)⟼{m\upharpoonright }_J\right)$$