Theorem 4rexfrabdioph

Description: Diophantine set builder for existential quantifier, explicit substitution, four variables. (Contributed by Stefan O'Rear, 11-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

	Ref	Expression
Hypotheses	rexfrabdioph.1	$$⊢M=N+1$$
	rexfrabdioph.2	$$⊢L=M+1$$
	rexfrabdioph.3	$$⊢K=L+1$$
	rexfrabdioph.4	$$⊢J=K+1$$
Assertion	4rexfrabdioph	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots J\right)}\right)|\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(J\right)\right)\to \left\{u\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists v\in {\mathbb{N}}_0\exists w\in {\mathbb{N}}_0\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\phi \right\}\in \mathrm{Dioph}\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		rexfrabdioph.1	$$⊢M=N+1$$
2		rexfrabdioph.2	$$⊢L=M+1$$
3		rexfrabdioph.3	$$⊢K=L+1$$
4		rexfrabdioph.4	$$⊢J=K+1$$
5		2sbcrex	$$⊢\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\phi \leftrightarrow \exists x\in {\mathbb{N}}_0\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\exists y\in {\mathbb{N}}_0\phi$$
6		2sbcrex	$$⊢\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\exists y\in {\mathbb{N}}_0\phi \leftrightarrow \exists y\in {\mathbb{N}}_0\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi$$
7	6	rexbii	$$⊢\exists x\in {\mathbb{N}}_0\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\exists y\in {\mathbb{N}}_0\phi \leftrightarrow \exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi$$
8	5 7	bitri	$$⊢\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\phi \leftrightarrow \exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi$$
9	8	sbcbii	$$⊢\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\phi \leftrightarrow \underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi$$
10		sbc2rex	$$⊢\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi \leftrightarrow \exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi$$
11	9 10	bitri	$$⊢\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\phi \leftrightarrow \exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi$$
12	11	rabbii	$$⊢\left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots L\right)}\right)|\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\phi \right\}=\left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots L\right)}\right)|\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi \right\}$$
13		nn0p1nn	$$⊢N\in {\mathbb{N}}_0\to N+1\in \mathbb{N}$$
14	1 13	eqeltrid	$$⊢N\in {\mathbb{N}}_0\to M\in \mathbb{N}$$
15	14	peano2nnd	$$⊢N\in {\mathbb{N}}_0\to M+1\in \mathbb{N}$$
16	2 15	eqeltrid	$$⊢N\in {\mathbb{N}}_0\to L\in \mathbb{N}$$
17	16	nnnn0d	$$⊢N\in {\mathbb{N}}_0\to L\in {\mathbb{N}}_0$$
18	17	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots J\right)}\right)|\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(J\right)\right)\to L\in {\mathbb{N}}_0$$
19		sbcrot3	$$⊢\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi$$
20		sbcrot3	$$⊢\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi$$
21	20	sbcbii	$$⊢\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi$$
22		sbcrot3	$$⊢\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi$$
23	21 22	bitri	$$⊢\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi$$
24	23	sbcbii	$$⊢\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi$$
25	19 24	bitr3i	$$⊢\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi$$
26	25	sbcbii	$$⊢\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi$$
27		reseq1	$$⊢a={t\upharpoonright }_{\left(1\dots L\right)}\to {a\upharpoonright }_{\left(1\dots N\right)}={\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\upharpoonright }_{\left(1\dots N\right)}$$
28	27	sbccomieg	$$⊢\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi$$
29		fzssp1	$$⊢\left(1\dots N\right)\subseteq \left(1\dots N+1\right)$$
30	1	oveq2i	$$⊢\left(1\dots M\right)=\left(1\dots N+1\right)$$
31	29 30	sseqtrri	$$⊢\left(1\dots N\right)\subseteq \left(1\dots M\right)$$
32		fzssp1	$$⊢\left(1\dots M\right)\subseteq \left(1\dots M+1\right)$$
33	2	oveq2i	$$⊢\left(1\dots L\right)=\left(1\dots M+1\right)$$
34	32 33	sseqtrri	$$⊢\left(1\dots M\right)\subseteq \left(1\dots L\right)$$
35	31 34	sstri	$$⊢\left(1\dots N\right)\subseteq \left(1\dots L\right)$$
36		resabs1	$$⊢\left(1\dots N\right)\subseteq \left(1\dots L\right)\to {\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\upharpoonright }_{\left(1\dots N\right)}={t\upharpoonright }_{\left(1\dots N\right)}$$
37		dfsbcq	$$⊢{\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\upharpoonright }_{\left(1\dots N\right)}={t\upharpoonright }_{\left(1\dots N\right)}\to \left(\underset{\dot{}}{[}\left({\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right)$$
38	35 36 37	mp2b	$$⊢\underset{\dot{}}{[}\left({\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi$$
39		fveq1	$$⊢a={t\upharpoonright }_{\left(1\dots L\right)}\to a\left(M\right)=\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\left(M\right)$$
40	39	sbccomieg	$$⊢\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi$$
41		elfz1end	$$⊢M\in \mathbb{N}\leftrightarrow M\in \left(1\dots M\right)$$
42	14 41	sylib	$$⊢N\in {\mathbb{N}}_0\to M\in \left(1\dots M\right)$$
43	34 42	sselid	$$⊢N\in {\mathbb{N}}_0\to M\in \left(1\dots L\right)$$
44		fvres	$$⊢M\in \left(1\dots L\right)\to \left({t\upharpoonright }_{\left(1\dots L\right)}\right)\left(M\right)=t\left(M\right)$$
45		dfsbcq	$$⊢\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\left(M\right)=t\left(M\right)\to \left(\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right)$$
46	43 44 45	3syl	$$⊢N\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right)$$
47		vex	$$⊢t\in \mathrm{V}$$
48	47	resex	$$⊢{t\upharpoonright }_{\left(1\dots L\right)}\in \mathrm{V}$$
49		fveq1	$$⊢a={t\upharpoonright }_{\left(1\dots L\right)}\to a\left(L\right)=\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\left(L\right)$$
50	49	sbcco3gw	$$⊢{t\upharpoonright }_{\left(1\dots L\right)}\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right)$$
51	48 50	ax-mp	$$⊢\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi$$
52		elfz1end	$$⊢L\in \mathbb{N}\leftrightarrow L\in \left(1\dots L\right)$$
53	16 52	sylib	$$⊢N\in {\mathbb{N}}_0\to L\in \left(1\dots L\right)$$
54		fvres	$$⊢L\in \left(1\dots L\right)\to \left({t\upharpoonright }_{\left(1\dots L\right)}\right)\left(L\right)=t\left(L\right)$$
55		dfsbcq	$$⊢\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\left(L\right)=t\left(L\right)\to \left(\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right)$$
56	53 54 55	3syl	$$⊢N\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right)$$
57	51 56	syl5bb	$$⊢N\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right)$$
58	57	sbcbidv	$$⊢N\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right)$$
59	46 58	bitrd	$$⊢N\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right)$$
60	40 59	syl5bb	$$⊢N\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right)$$
61	60	sbcbidv	$$⊢N\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right)$$
62	38 61	syl5bb	$$⊢N\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}\left({\left({t\upharpoonright }_{\left(1\dots L\right)}\right)\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right)$$
63	28 62	syl5bb	$$⊢N\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right)$$
64	26 63	syl5bb	$$⊢N\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right)$$
65	64	rabbidv	$$⊢N\in {\mathbb{N}}_0\to \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots J\right)}\right)|\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi \right\}=\left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots J\right)}\right)|\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right\}$$
66	65	eleq1d	$$⊢N\in {\mathbb{N}}_0\to \left(\left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots J\right)}\right)|\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(J\right)\leftrightarrow \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots J\right)}\right)|\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(J\right)\right)$$
67	66	biimpar	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots J\right)}\right)|\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(J\right)\right)\to \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots J\right)}\right)|\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(J\right)$$
68	3 4	2rexfrabdioph	$$⊢\left(L\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots J\right)}\right)|\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots L\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(J\right)\right)\to \left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots L\right)}\right)|\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(L\right)$$
69	18 67 68	syl2anc	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots J\right)}\right)|\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(J\right)\right)\to \left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots L\right)}\right)|\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(L\right)$$
70	12 69	eqeltrid	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots J\right)}\right)|\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(J\right)\right)\to \left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots L\right)}\right)|\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\phi \right\}\in \mathrm{Dioph}\left(L\right)$$
71	1 2	2rexfrabdioph	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots L\right)}\right)|\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\phi \right\}\in \mathrm{Dioph}\left(L\right)\right)\to \left\{u\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists v\in {\mathbb{N}}_0\exists w\in {\mathbb{N}}_0\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\phi \right\}\in \mathrm{Dioph}\left(N\right)$$
72	70 71	syldan	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots J\right)}\right)|\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(J\right)\right)\to \left\{u\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists v\in {\mathbb{N}}_0\exists w\in {\mathbb{N}}_0\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\phi \right\}\in \mathrm{Dioph}\left(N\right)$$