# Metamath Proof Explorer

## 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 {ℕ}_{0}\to {{ℕ}_{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({{ℕ}_{0}}^{\left(1\dots {A}\right)}\right)\phantom{\rule{.4em}{0ex}}0=0$
3 rabid2 ${⊢}{{ℕ}_{0}}^{\left(1\dots {A}\right)}=\left\{{a}\in \left({{ℕ}_{0}}^{\left(1\dots {A}\right)}\right)|0=0\right\}↔\forall {a}\in \left({{ℕ}_{0}}^{\left(1\dots {A}\right)}\right)\phantom{\rule{.4em}{0ex}}0=0$
4 2 3 mpbir ${⊢}{{ℕ}_{0}}^{\left(1\dots {A}\right)}=\left\{{a}\in \left({{ℕ}_{0}}^{\left(1\dots {A}\right)}\right)|0=0\right\}$
5 ovex ${⊢}\left(1\dots {A}\right)\in \mathrm{V}$
6 0z ${⊢}0\in ℤ$
7 mzpconstmpt ${⊢}\left(\left(1\dots {A}\right)\in \mathrm{V}\wedge 0\in ℤ\right)\to \left({a}\in \left({ℤ}^{\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({ℤ}^{\left(1\dots {A}\right)}\right)⟼0\right)\in \mathrm{mzPoly}\left(\left(1\dots {A}\right)\right)$
9 eq0rabdioph ${⊢}\left({A}\in {ℕ}_{0}\wedge \left({a}\in \left({ℤ}^{\left(1\dots {A}\right)}\right)⟼0\right)\in \mathrm{mzPoly}\left(\left(1\dots {A}\right)\right)\right)\to \left\{{a}\in \left({{ℕ}_{0}}^{\left(1\dots {A}\right)}\right)|0=0\right\}\in \mathrm{Dioph}\left({A}\right)$
10 8 9 mpan2 ${⊢}{A}\in {ℕ}_{0}\to \left\{{a}\in \left({{ℕ}_{0}}^{\left(1\dots {A}\right)}\right)|0=0\right\}\in \mathrm{Dioph}\left({A}\right)$
11 4 10 eqeltrid ${⊢}{A}\in {ℕ}_{0}\to {{ℕ}_{0}}^{\left(1\dots {A}\right)}\in \mathrm{Dioph}\left({A}\right)$