Theorem eldioph4i

Description: Forward-only version of eldioph4b . (Contributed by Stefan O'Rear, 16-Oct-2014)

	Ref	Expression
Hypotheses	eldioph4b.a	$$⊢W\in \mathrm{V}$$
	eldioph4b.b	$$⊢\neg W\in \mathrm{Fin}$$
	eldioph4b.c	$$⊢W\cap \mathbb{N}=\varnothing$$
Assertion	eldioph4i	$$⊢\left(N\in {\mathbb{N}}_0\wedge P\in \mathrm{mzPoly}\left(W\cup \left(1\dots N\right)\right)\right)\to \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists w\in \left({{\mathbb{N}}_0}^W\right)P\left(t\cup w\right)=0\right\}\in \mathrm{Dioph}\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		eldioph4b.a	$$⊢W\in \mathrm{V}$$
2		eldioph4b.b	$$⊢\neg W\in \mathrm{Fin}$$
3		eldioph4b.c	$$⊢W\cap \mathbb{N}=\varnothing$$
4		uneq1	$$⊢t=a\to t\cup w=a\cup w$$
5	4	fveqeq2d	$$⊢t=a\to \left(P\left(t\cup w\right)=0\leftrightarrow P\left(a\cup w\right)=0\right)$$
6	5	rexbidv	$$⊢t=a\to \left(\exists w\in \left({{\mathbb{N}}_0}^W\right)P\left(t\cup w\right)=0\leftrightarrow \exists w\in \left({{\mathbb{N}}_0}^W\right)P\left(a\cup w\right)=0\right)$$
7		uneq2	$$⊢w=b\to a\cup w=a\cup b$$
8	7	fveqeq2d	$$⊢w=b\to \left(P\left(a\cup w\right)=0\leftrightarrow P\left(a\cup b\right)=0\right)$$
9	8	cbvrexvw	$$⊢\exists w\in \left({{\mathbb{N}}_0}^W\right)P\left(a\cup w\right)=0\leftrightarrow \exists b\in \left({{\mathbb{N}}_0}^W\right)P\left(a\cup b\right)=0$$
10	6 9	bitrdi	$$⊢t=a\to \left(\exists w\in \left({{\mathbb{N}}_0}^W\right)P\left(t\cup w\right)=0\leftrightarrow \exists b\in \left({{\mathbb{N}}_0}^W\right)P\left(a\cup b\right)=0\right)$$
11	10	cbvrabv	$$⊢\left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists w\in \left({{\mathbb{N}}_0}^W\right)P\left(t\cup w\right)=0\right\}=\left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists b\in \left({{\mathbb{N}}_0}^W\right)P\left(a\cup b\right)=0\right\}$$
12		fveq1	$$⊢p=P\to p\left(a\cup b\right)=P\left(a\cup b\right)$$
13	12	eqeq1d	$$⊢p=P\to \left(p\left(a\cup b\right)=0\leftrightarrow P\left(a\cup b\right)=0\right)$$
14	13	rexbidv	$$⊢p=P\to \left(\exists b\in \left({{\mathbb{N}}_0}^W\right)p\left(a\cup b\right)=0\leftrightarrow \exists b\in \left({{\mathbb{N}}_0}^W\right)P\left(a\cup b\right)=0\right)$$
15	14	rabbidv	$$⊢p=P\to \left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists b\in \left({{\mathbb{N}}_0}^W\right)p\left(a\cup b\right)=0\right\}=\left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists b\in \left({{\mathbb{N}}_0}^W\right)P\left(a\cup b\right)=0\right\}$$
16	15	rspceeqv	$$⊢\left(P\in \mathrm{mzPoly}\left(W\cup \left(1\dots N\right)\right)\wedge \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists w\in \left({{\mathbb{N}}_0}^W\right)P\left(t\cup w\right)=0\right\}=\left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists b\in \left({{\mathbb{N}}_0}^W\right)P\left(a\cup b\right)=0\right\}\right)\to \exists p\in \mathrm{mzPoly}\left(W\cup \left(1\dots N\right)\right)\left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists w\in \left({{\mathbb{N}}_0}^W\right)P\left(t\cup w\right)=0\right\}=\left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists b\in \left({{\mathbb{N}}_0}^W\right)p\left(a\cup b\right)=0\right\}$$
17	11 16	mpan2	$$⊢P\in \mathrm{mzPoly}\left(W\cup \left(1\dots N\right)\right)\to \exists p\in \mathrm{mzPoly}\left(W\cup \left(1\dots N\right)\right)\left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists w\in \left({{\mathbb{N}}_0}^W\right)P\left(t\cup w\right)=0\right\}=\left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists b\in \left({{\mathbb{N}}_0}^W\right)p\left(a\cup b\right)=0\right\}$$
18	17	anim2i	$$⊢\left(N\in {\mathbb{N}}_0\wedge P\in \mathrm{mzPoly}\left(W\cup \left(1\dots N\right)\right)\right)\to \left(N\in {\mathbb{N}}_0\wedge \exists p\in \mathrm{mzPoly}\left(W\cup \left(1\dots N\right)\right)\left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists w\in \left({{\mathbb{N}}_0}^W\right)P\left(t\cup w\right)=0\right\}=\left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists b\in \left({{\mathbb{N}}_0}^W\right)p\left(a\cup b\right)=0\right\}\right)$$
19	1 2 3	eldioph4b	$$⊢\left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists w\in \left({{\mathbb{N}}_0}^W\right)P\left(t\cup w\right)=0\right\}\in \mathrm{Dioph}\left(N\right)\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge \exists p\in \mathrm{mzPoly}\left(W\cup \left(1\dots N\right)\right)\left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists w\in \left({{\mathbb{N}}_0}^W\right)P\left(t\cup w\right)=0\right\}=\left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists b\in \left({{\mathbb{N}}_0}^W\right)p\left(a\cup b\right)=0\right\}\right)$$
20	18 19	sylibr	$$⊢\left(N\in {\mathbb{N}}_0\wedge P\in \mathrm{mzPoly}\left(W\cup \left(1\dots N\right)\right)\right)\to \left\{t\in \left({{\mathbb{N}}_0}^{\left(1\dots N\right)}\right)|\exists w\in \left({{\mathbb{N}}_0}^W\right)P\left(t\cup w\right)=0\right\}\in \mathrm{Dioph}\left(N\right)$$