Theorem 3rexfrabdioph

Description: Diophantine set builder for existential quantifier, explicit substitution, two variables. (Contributed by Stefan O'Rear, 17-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$$
Assertion	3rexfrabdioph	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots K\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(K\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\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		sbc2rex	$$⊢\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\exists w\in {\mathbb{N}}_0\exists x\in {\mathbb{N}}_0\phi \leftrightarrow \exists w\in {\mathbb{N}}_0\exists x\in {\mathbb{N}}_0\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\phi$$
5	4	sbcbii	$$⊢\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\exists x\in {\mathbb{N}}_0\phi \leftrightarrow \underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\exists w\in {\mathbb{N}}_0\exists x\in {\mathbb{N}}_0\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\phi$$
6		sbc2rex	$$⊢\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\exists w\in {\mathbb{N}}_0\exists x\in {\mathbb{N}}_0\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\phi \leftrightarrow \exists w\in {\mathbb{N}}_0\exists x\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$$
7	5 6	bitri	$$⊢\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\exists x\in {\mathbb{N}}_0\phi \leftrightarrow \exists w\in {\mathbb{N}}_0\exists x\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$$
8	7	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\exists x\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\exists x\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\}$$
9		nn0p1nn	$$⊢N\in {\mathbb{N}}_0\to N+1\in \mathbb{N}$$
10	1 9	eqeltrid	$$⊢N\in {\mathbb{N}}_0\to M\in \mathbb{N}$$
11	10	nnnn0d	$$⊢N\in {\mathbb{N}}_0\to M\in {\mathbb{N}}_0$$
12	11	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots K\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(K\right)\right)\to M\in {\mathbb{N}}_0$$
13		sbcrot3	$$⊢\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\phi$$
14	13	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{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\phi$$
15		sbcrot3	$$⊢\underset{\dot{}}{[}\left({a\upharpoonright }_{\left(1\dots N\right)}\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\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$$
16	14 15	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{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(L\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\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$$
17	16	sbcbii	$$⊢\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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\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{}}{[}t\left(K\right)/x\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$$
18		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)}$$
19	18	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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\phi$$
20		fzssp1	$$⊢\left(1\dots N\right)\subseteq \left(1\dots N+1\right)$$
21	1	oveq2i	$$⊢\left(1\dots M\right)=\left(1\dots N+1\right)$$
22	20 21	sseqtrri	$$⊢\left(1\dots N\right)\subseteq \left(1\dots M\right)$$
23		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)}$$
24		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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\phi \right)$$
25	22 23 24	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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\phi$$
26		vex	$$⊢t\in \mathrm{V}$$
27	26	resex	$$⊢{t\upharpoonright }_{\left(1\dots M\right)}\in \mathrm{V}$$
28		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)$$
29	28	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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\phi \right)$$
30	27 29	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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\phi$$
31		elfz1end	$$⊢M\in \mathbb{N}\leftrightarrow M\in \left(1\dots M\right)$$
32	10 31	sylib	$$⊢N\in {\mathbb{N}}_0\to M\in \left(1\dots M\right)$$
33		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)$$
34		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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\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{}}{]}\phi \right)$$
35	32 33 34	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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\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{}}{]}\phi \right)$$
36	30 35	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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\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{}}{]}\phi \right)$$
37	36	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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\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{}}{]}\phi \right)$$
38	25 37	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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\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{}}{]}\phi \right)$$
39	19 38	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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\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{}}{]}\phi \right)$$
40	17 39	bitr3id	$$⊢N\in {\mathbb{N}}_0\to \left(\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{}}{[}t\left(K\right)/x\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 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{}}{]}\phi \right)$$
41	40	rabbidv	$$⊢N\in {\mathbb{N}}_0\to \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots K\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{}}{[}t\left(K\right)/x\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\}=\left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots K\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{}}{]}\phi \right\}$$
42	41	eleq1d	$$⊢N\in {\mathbb{N}}_0\to \left(\left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots K\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{}}{[}t\left(K\right)/x\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(K\right)\leftrightarrow \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots K\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(K\right)\right)$$
43	42	biimpar	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots K\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(K\right)\right)\to \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots K\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{}}{[}t\left(K\right)/x\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(K\right)$$
44	2 3	2rexfrabdioph	$$⊢\left(M\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots K\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{}}{[}t\left(K\right)/x\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(K\right)\right)\to \left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots M\right)}\right)|\exists w\in {\mathbb{N}}_0\exists x\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)$$
45	12 43 44	syl2anc	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots K\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(K\right)\right)\to \left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots M\right)}\right)|\exists w\in {\mathbb{N}}_0\exists x\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)$$
46	8 45	eqeltrid	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots K\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(K\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\exists x\in {\mathbb{N}}_0\phi \right\}\in \mathrm{Dioph}\left(M\right)$$
47	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\exists x\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\exists x\in {\mathbb{N}}_0\phi \right\}\in \mathrm{Dioph}\left(N\right)$$
48	46 47	syldan	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots K\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(K\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\phi \right\}\in \mathrm{Dioph}\left(N\right)$$