Theorem 2rexfrabdioph

Description: Diophantine set builder for existential quantifier, explicit substitution, two 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$$
Assertion	2rexfrabdioph	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots L\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{}}{]}\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\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		2sbcrex	$$⊢\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\exists w\in {\mathbb{N}}_0\phi \leftrightarrow \exists w\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{}}{]}\phi$$
4	3	rabbii	$$⊢\left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots M\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{}}{]}\exists w\in {\mathbb{N}}_0\phi \right\}=\left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots M\right)}\right)|\exists w\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{}}{]}\phi \right\}$$
5		peano2nn0	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{N}}_0$$
6	1 5	eqeltrid	$$⊢N\in {\mathbb{N}}_0\to M\in {\mathbb{N}}_0$$
7	6	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots L\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(L\right)\right)\to M\in {\mathbb{N}}_0$$
8		sbcrot3	$$⊢\underset{\dot{}}{[}t\left(L\right)/w\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{}}{]}\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{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\phi$$
9	8	sbcbii	$$⊢\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\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{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\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{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\phi$$
10		reseq1	$$⊢a={t\upharpoonright }_{\left(1\dots M\right)}\to {a\upharpoonright }_{\left(1\dots N\right)}={\left({t\upharpoonright }_{\left(1\dots M\right)}\right)\upharpoonright }_{\left(1\dots N\right)}$$
11	10	sbccomieg	$$⊢\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\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{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({\left({t\upharpoonright }_{\left(1\dots M\right)}\right)\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\phi$$
12		fzssp1	$$⊢\left(1\dots N\right)\subseteq \left(1\dots N+1\right)$$
13	1	oveq2i	$$⊢\left(1\dots M\right)=\left(1\dots N+1\right)$$
14	12 13	sseqtrri	$$⊢\left(1\dots N\right)\subseteq \left(1\dots M\right)$$
15		resabs1	$$⊢\left(1\dots N\right)\subseteq \left(1\dots M\right)\to {\left({t\upharpoonright }_{\left(1\dots M\right)}\right)\upharpoonright }_{\left(1\dots N\right)}={t\upharpoonright }_{\left(1\dots N\right)}$$
16		dfsbcq	$$⊢{\left({t\upharpoonright }_{\left(1\dots M\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 M\right)}\right)\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\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 M\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\phi \right)$$
17	14 15 16	mp2b	$$⊢\underset{\dot{}}{[}\left({\left({t\upharpoonright }_{\left(1\dots M\right)}\right)\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\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 M\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\phi$$
18		vex	$$⊢t\in \mathrm{V}$$
19	18	resex	$$⊢{t\upharpoonright }_{\left(1\dots M\right)}\in \mathrm{V}$$
20		fveq1	$$⊢a={t\upharpoonright }_{\left(1\dots M\right)}\to a\left(M\right)=\left({t\upharpoonright }_{\left(1\dots M\right)}\right)\left(M\right)$$
21	20	sbcco3gw	$$⊢{t\upharpoonright }_{\left(1\dots M\right)}\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\right)}\right)\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\phi \right)$$
22	19 21	ax-mp	$$⊢\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\right)}\right)\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\phi$$
23		nn0p1nn	$$⊢N\in {\mathbb{N}}_0\to N+1\in \mathbb{N}$$
24	1 23	eqeltrid	$$⊢N\in {\mathbb{N}}_0\to M\in \mathbb{N}$$
25		elfz1end	$$⊢M\in \mathbb{N}\leftrightarrow M\in \left(1\dots M\right)$$
26	24 25	sylib	$$⊢N\in {\mathbb{N}}_0\to M\in \left(1\dots M\right)$$
27		fvres	$$⊢M\in \left(1\dots M\right)\to \left({t\upharpoonright }_{\left(1\dots M\right)}\right)\left(M\right)=t\left(M\right)$$
28		dfsbcq	$$⊢\left({t\upharpoonright }_{\left(1\dots M\right)}\right)\left(M\right)=t\left(M\right)\to \left(\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\right)}\right)\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\phi \right)$$
29	26 27 28	3syl	$$⊢N\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\right)}\right)\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\phi \right)$$
30	22 29	syl5bb	$$⊢N\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\phi \right)$$
31	30	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 M\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\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{}}{]}\phi \right)$$
32	17 31	syl5bb	$$⊢N\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}\left({\left({t\upharpoonright }_{\left(1\dots M\right)}\right)\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\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{}}{]}\phi \right)$$
33	11 32	syl5bb	$$⊢N\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\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{}}{[}t\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{}}{]}\phi \right)$$
34	9 33	bitr2id	$$⊢N\in {\mathbb{N}}_0\to \left(\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{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\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{}}{]}\phi \right)$$
35	34	rabbidv	$$⊢N\in {\mathbb{N}}_0\to \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots L\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{}}{]}\phi \right\}=\left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots L\right)}\right)|\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\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{}}{]}\phi \right\}$$
36	35	eleq1d	$$⊢N\in {\mathbb{N}}_0\to \left(\left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots L\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(L\right)\leftrightarrow \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots L\right)}\right)|\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(L\right)\right)$$
37	36	biimpa	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots L\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(L\right)\right)\to \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots L\right)}\right)|\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(L\right)$$
38	2	rexfrabdioph	$$⊢\left(M\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots L\right)}\right)|\underset{\dot{}}{[}\left({t\upharpoonright }_{\left(1\dots M\right)}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(L\right)\right)\to \left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots M\right)}\right)|\exists w\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(M\right)$$
39	7 37 38	syl2anc	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots L\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(L\right)\right)\to \left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots M\right)}\right)|\exists w\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(M\right)$$
40	4 39	eqeltrid	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots L\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(L\right)\right)\to \left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots M\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{}}{]}\exists w\in {\mathbb{N}}_0\phi \right\}\in \mathrm{Dioph}\left(M\right)$$
41	1	rexfrabdioph	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots M\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{}}{]}\exists w\in {\mathbb{N}}_0\phi \right\}\in \mathrm{Dioph}\left(M\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\phi \right\}\in \mathrm{Dioph}\left(N\right)$$
42	40 41	syldan	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots L\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{}}{]}\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\phi \right\}\in \mathrm{Dioph}\left(N\right)$$