Theorem 0dioph

Description: The empty set is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014)

	Ref	Expression
Assertion	0dioph	$$⊢A\in {\mathbb{N}}_0\to \varnothing \in \mathrm{Dioph}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-1ne0	$$⊢1\ne 0$$
2	1	neii	$$⊢\neg 1=0$$
3	2	rgenw	$$⊢\forall a\in \left({{\mathbb{N}}_0}^{\left(1\dots A\right)}\right)\neg 1=0$$
4		rabeq0	$$⊢\left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots A\right)}\right)|1=0\right\}=\varnothing \leftrightarrow \forall a\in \left({{\mathbb{N}}_0}^{\left(1\dots A\right)}\right)\neg 1=0$$
5	3 4	mpbir	$$⊢\left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots A\right)}\right)|1=0\right\}=\varnothing$$
6		ovex	$$⊢\left(1\dots A\right)\in \mathrm{V}$$
7		1z	$$⊢1\in \mathbb{Z}$$
8		mzpconstmpt	$$⊢\left(\left(1\dots A\right)\in \mathrm{V}\wedge 1\in \mathbb{Z}\right)\to \left(a\in \left({\mathbb{Z}}^{\left(1\dots A\right)}\right)⟼1\right)\in \mathrm{mzPoly}\left(\left(1\dots A\right)\right)$$
9	6 7 8	mp2an	$$⊢\left(a\in \left({\mathbb{Z}}^{\left(1\dots A\right)}\right)⟼1\right)\in \mathrm{mzPoly}\left(\left(1\dots A\right)\right)$$
10		eq0rabdioph	$$⊢\left(A\in {\mathbb{N}}_0\wedge \left(a\in \left({\mathbb{Z}}^{\left(1\dots A\right)}\right)⟼1\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)|1=0\right\}\in \mathrm{Dioph}\left(A\right)$$
11	9 10	mpan2	$$⊢A\in {\mathbb{N}}_0\to \left\{a\in \left({{\mathbb{N}}_0}^{\left(1\dots A\right)}\right)|1=0\right\}\in \mathrm{Dioph}\left(A\right)$$
12	5 11	eqeltrrid	$$⊢A\in {\mathbb{N}}_0\to \varnothing \in \mathrm{Dioph}\left(A\right)$$