Theorem 6rexfrabdioph

Description: Diophantine set builder for existential quantifier, explicit substitution, six 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$$
	rexfrabdioph.5	$$⊢I=J+1$$
	rexfrabdioph.6	$$⊢H=I+1$$
Assertion	6rexfrabdioph	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots H\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(H\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\exists z\in {\mathbb{N}}_0\exists p\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		rexfrabdioph.5	$$⊢I=J+1$$
6		rexfrabdioph.6	$$⊢H=I+1$$
7		sbc4rex	$$⊢\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\exists z\in {\mathbb{N}}_0\exists p\in {\mathbb{N}}_0\phi \leftrightarrow \exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\exists z\in {\mathbb{N}}_0\exists p\in {\mathbb{N}}_0\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi$$
8	7	sbcbii	$$⊢\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\exists z\in {\mathbb{N}}_0\exists p\in {\mathbb{N}}_0\phi \leftrightarrow \underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\exists z\in {\mathbb{N}}_0\exists p\in {\mathbb{N}}_0\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi$$
9		sbc4rex	$$⊢\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\exists z\in {\mathbb{N}}_0\exists p\in {\mathbb{N}}_0\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi \leftrightarrow \exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\exists z\in {\mathbb{N}}_0\exists p\in {\mathbb{N}}_0\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi$$
10	8 9	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\exists z\in {\mathbb{N}}_0\exists p\in {\mathbb{N}}_0\phi \leftrightarrow \exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\exists z\in {\mathbb{N}}_0\exists p\in {\mathbb{N}}_0\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi$$
11	10	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\exists z\in {\mathbb{N}}_0\exists p\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\exists z\in {\mathbb{N}}_0\exists p\in {\mathbb{N}}_0\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi$$
12		sbc4rex	$$⊢\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\exists z\in {\mathbb{N}}_0\exists p\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\exists z\in {\mathbb{N}}_0\exists p\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$$
13	11 12	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\exists z\in {\mathbb{N}}_0\exists p\in {\mathbb{N}}_0\phi \leftrightarrow \exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_0\exists z\in {\mathbb{N}}_0\exists p\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$$
14	13	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\exists z\in {\mathbb{N}}_0\exists p\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\exists z\in {\mathbb{N}}_0\exists p\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\}$$
15		nn0p1nn	$$⊢N\in {\mathbb{N}}_0\to N+1\in \mathbb{N}$$
16	1 15	eqeltrid	$$⊢N\in {\mathbb{N}}_0\to M\in \mathbb{N}$$
17	16	peano2nnd	$$⊢N\in {\mathbb{N}}_0\to M+1\in \mathbb{N}$$
18	2 17	eqeltrid	$$⊢N\in {\mathbb{N}}_0\to L\in \mathbb{N}$$
19	18	nnnn0d	$$⊢N\in {\mathbb{N}}_0\to L\in {\mathbb{N}}_0$$
20	19	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots H\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(H\right)\right)\to L\in {\mathbb{N}}_0$$
21		sbcrot5	$$⊢\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi$$
22	21	sbcbii	$$⊢\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi$$
23		sbcrot5	$$⊢\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi$$
24	22 23	bitri	$$⊢\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi$$
25	24	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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \leftrightarrow \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{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(M\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}a\left(L\right)/w\underset{\dot{}}{]}\phi$$
26		sbcrot5	$$⊢\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{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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$$
27	25 26	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{}}{]}\underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(K\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(J\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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$$
28	27	sbcbii	$$⊢\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \leftrightarrow \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{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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$$
29		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)}$$
30	29	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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi$$
31		fzssp1	$$⊢\left(1\dots N\right)\subseteq \left(1\dots N+1\right)$$
32	1	oveq2i	$$⊢\left(1\dots M\right)=\left(1\dots N+1\right)$$
33	31 32	sseqtrri	$$⊢\left(1\dots N\right)\subseteq \left(1\dots M\right)$$
34		fzssp1	$$⊢\left(1\dots M\right)\subseteq \left(1\dots M+1\right)$$
35	2	oveq2i	$$⊢\left(1\dots L\right)=\left(1\dots M+1\right)$$
36	34 35	sseqtrri	$$⊢\left(1\dots M\right)\subseteq \left(1\dots L\right)$$
37	33 36	sstri	$$⊢\left(1\dots N\right)\subseteq \left(1\dots L\right)$$
38		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)}$$
39		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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right)$$
40	37 38 39	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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi$$
41		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)$$
42	41	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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi$$
43		elfz1end	$$⊢M\in \mathbb{N}\leftrightarrow M\in \left(1\dots M\right)$$
44	16 43	sylib	$$⊢N\in {\mathbb{N}}_0\to M\in \left(1\dots M\right)$$
45	36 44	sselid	$$⊢N\in {\mathbb{N}}_0\to M\in \left(1\dots L\right)$$
46		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)$$
47		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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right)$$
48	45 46 47	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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right)$$
49		vex	$$⊢t\in \mathrm{V}$$
50	49	resex	$$⊢{t\upharpoonright }_{\left(1\dots L\right)}\in \mathrm{V}$$
51		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)$$
52	51	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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right)$$
53	50 52	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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi$$
54		elfz1end	$$⊢L\in \mathbb{N}\leftrightarrow L\in \left(1\dots L\right)$$
55	18 54	sylib	$$⊢N\in {\mathbb{N}}_0\to L\in \left(1\dots L\right)$$
56		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)$$
57		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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right)$$
58	55 56 57	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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right)$$
59	53 58	bitrid	$$⊢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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right)$$
60	59	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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right)$$
61	48 60	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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right)$$
62	42 61	bitrid	$$⊢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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right)$$
63	62	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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right)$$
64	40 63	bitrid	$$⊢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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right)$$
65	30 64	bitrid	$$⊢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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right)$$
66	28 65	bitr3id	$$⊢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{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right)$$
67	66	rabbidv	$$⊢N\in {\mathbb{N}}_0\to \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots H\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{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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 H\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right\}$$
68	67	eleq1d	$$⊢N\in {\mathbb{N}}_0\to \left(\left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots H\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{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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(H\right)\leftrightarrow \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots H\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(H\right)\right)$$
69	68	biimpar	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots H\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(H\right)\right)\to \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots H\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{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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(H\right)$$
70	3 4 5 6	4rexfrabdioph	$$⊢\left(L\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots H\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{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\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(H\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\exists z\in {\mathbb{N}}_0\exists p\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)$$
71	20 69 70	syl2anc	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots H\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(H\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\exists z\in {\mathbb{N}}_0\exists p\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)$$
72	14 71	eqeltrid	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots H\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(H\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\exists z\in {\mathbb{N}}_0\exists p\in {\mathbb{N}}_0\phi \right\}\in \mathrm{Dioph}\left(L\right)$$
73	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\exists z\in {\mathbb{N}}_0\exists p\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\exists z\in {\mathbb{N}}_0\exists p\in {\mathbb{N}}_0\phi \right\}\in \mathrm{Dioph}\left(N\right)$$
74	72 73	syldan	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots H\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{}}{]}\underset{\dot{}}{[}t\left(I\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(H\right)/p\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(H\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\exists z\in {\mathbb{N}}_0\exists p\in {\mathbb{N}}_0\phi \right\}\in \mathrm{Dioph}\left(N\right)$$