Theorem rexfrabdioph

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

	Ref	Expression
Hypothesis	rexfrabdioph.1	$$⊢M=N+1$$
Assertion	rexfrabdioph	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots M\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{}}{]}\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\phi \right\}\in \mathrm{Dioph}\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		rexfrabdioph.1	$$⊢M=N+1$$
2		nfcv	$$⊢\underset{\_}{Ⅎ}u\left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}a\left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)$$
4		nfv	$$⊢Ⅎa\exists v\in {\mathbb{N}}_0\phi$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}u{\mathbb{N}}_0$$
6		nfsbc1v	$$⊢Ⅎu\underset{\dot{}}{[}a/u\underset{\dot{}}{]}\underset{\dot{}}{[}b/v\underset{\dot{}}{]}\phi$$
7	5 6	nfrexw	$$⊢Ⅎu\exists b\in {\mathbb{N}}_0\underset{\dot{}}{[}a/u\underset{\dot{}}{]}\underset{\dot{}}{[}b/v\underset{\dot{}}{]}\phi$$
8		nfv	$$⊢Ⅎb\phi$$
9		nfsbc1v	$$⊢Ⅎv\underset{\dot{}}{[}b/v\underset{\dot{}}{]}\phi$$
10		sbceq1a	$$⊢v=b\to \left(\phi \leftrightarrow \underset{\dot{}}{[}b/v\underset{\dot{}}{]}\phi \right)$$
11	8 9 10	cbvrexw	$$⊢\exists v\in {\mathbb{N}}_0\phi \leftrightarrow \exists b\in {\mathbb{N}}_0\underset{\dot{}}{[}b/v\underset{\dot{}}{]}\phi$$
12		sbceq1a	$$⊢u=a\to \left(\underset{\dot{}}{[}b/v\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}a/u\underset{\dot{}}{]}\underset{\dot{}}{[}b/v\underset{\dot{}}{]}\phi \right)$$
13	12	rexbidv	$$⊢u=a\to \left(\exists b\in {\mathbb{N}}_0\underset{\dot{}}{[}b/v\underset{\dot{}}{]}\phi \leftrightarrow \exists b\in {\mathbb{N}}_0\underset{\dot{}}{[}a/u\underset{\dot{}}{]}\underset{\dot{}}{[}b/v\underset{\dot{}}{]}\phi \right)$$
14	11 13	bitrid	$$⊢u=a\to \left(\exists v\in {\mathbb{N}}_0\phi \leftrightarrow \exists b\in {\mathbb{N}}_0\underset{\dot{}}{[}a/u\underset{\dot{}}{]}\underset{\dot{}}{[}b/v\underset{\dot{}}{]}\phi \right)$$
15	2 3 4 7 14	cbvrabw	$$⊢\left\{u\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists v\in {\mathbb{N}}_0\phi \right\}=\left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists b\in {\mathbb{N}}_0\underset{\dot{}}{[}a/u\underset{\dot{}}{]}\underset{\dot{}}{[}b/v\underset{\dot{}}{]}\phi \right\}$$
16		dfsbcq	$$⊢b=t\left(M\right)\to \left(\underset{\dot{}}{[}b/v\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\phi \right)$$
17	16	sbcbidv	$$⊢b=t\left(M\right)\to \left(\underset{\dot{}}{[}a/u\underset{\dot{}}{]}\underset{\dot{}}{[}b/v\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}a/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\left(M\right)/v\underset{\dot{}}{]}\phi \right)$$
18		dfsbcq	$$⊢a={t\upharpoonright }_{\left(1\dots N\right)}\to \left(\underset{\dot{}}{[}a/u\underset{\dot{}}{]}\underset{\dot{}}{[}t\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{}}{]}\phi \right)$$
19	1 17 18	rexrabdioph	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots M\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{}}{]}\phi \right\}\in \mathrm{Dioph}\left(M\right)\right)\to \left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists b\in {\mathbb{N}}_0\underset{\dot{}}{[}a/u\underset{\dot{}}{]}\underset{\dot{}}{[}b/v\underset{\dot{}}{]}\phi \right\}\in \mathrm{Dioph}\left(N\right)$$
20	15 19	eqeltrid	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots M\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{}}{]}\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\phi \right\}\in \mathrm{Dioph}\left(N\right)$$