Theorem 7rexfrabdioph

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