Theorem vdioph

Description: The "universal" set (as large as possible given eldiophss ) is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014)

	Ref	Expression
Assertion	vdioph	$$⊢A\in {\mathbb{N}}_0\to {{\mathbb{N}}_0}^{\left(1\dots A\right)}\in \mathrm{Dioph}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢0=0$$
2	1	rgenw	$$⊢\forall a\in \left({{\mathbb{N}}_0}^{\left(1\dots A\right)}\right)0=0$$
3		rabid2	$$⊢{{\mathbb{N}}_0}^{\left(1\dots A\right)}=\left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots A\right)}\right)|0=0\right\}\leftrightarrow \forall a\in \left({{\mathbb{N}}_0}^{\left(1\dots A\right)}\right)0=0$$
4	2 3	mpbir	$$⊢{{\mathbb{N}}_0}^{\left(1\dots A\right)}=\left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots A\right)}\right)|0=0\right\}$$
5		ovex	$$⊢\left(1\dots A\right)\in \mathrm{V}$$
6		0z	$$⊢0\in \mathbb{Z}$$
7		mzpconstmpt	$$⊢\left(\left(1\dots A\right)\in \mathrm{V}\wedge 0\in \mathbb{Z}\right)\to \left(a\in \left({\mathbb{Z}}^{\left(1\dots A\right)}\right)⟼0\right)\in \mathrm{mzPoly}\left(\left(1\dots A\right)\right)$$
8	5 6 7	mp2an	$$⊢\left(a\in \left({\mathbb{Z}}^{\left(1\dots A\right)}\right)⟼0\right)\in \mathrm{mzPoly}\left(\left(1\dots A\right)\right)$$
9		eq0rabdioph	$$⊢\left(A\in {\mathbb{N}}_0\wedge \left(a\in \left({\mathbb{Z}}^{\left(1\dots A\right)}\right)⟼0\right)\in \mathrm{mzPoly}\left(\left(1\dots A\right)\right)\right)\to \left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots A\right)}\right)|0=0\right\}\in \mathrm{Dioph}\left(A\right)$$
10	8 9	mpan2	$$⊢A\in {\mathbb{N}}_0\to \left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots A\right)}\right)|0=0\right\}\in \mathrm{Dioph}\left(A\right)$$
11	4 10	eqeltrid	$$⊢A\in {\mathbb{N}}_0\to {{\mathbb{N}}_0}^{\left(1\dots A\right)}\in \mathrm{Dioph}\left(A\right)$$