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	⊢ ( 𝐴 ∈ ℕ0 → ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∈ ( Dioph ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ 0 = 0
2	1	rgenw	⊢ ∀ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) 0 = 0
3		rabid2	⊢ ( ( ℕ0 ↑m ( 1 ... 𝐴 ) ) = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 0 = 0 } ↔ ∀ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) 0 = 0 )
4	2 3	mpbir	⊢ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 0 = 0 }
5		ovex	⊢ ( 1 ... 𝐴 ) ∈ V
6		0z	⊢ 0 ∈ ℤ
7		mzpconstmpt	⊢ ( ( ( 1 ... 𝐴 ) ∈ V ∧ 0 ∈ ℤ ) → ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 𝐴 ) ) ↦ 0 ) ∈ ( mzPoly ‘ ( 1 ... 𝐴 ) ) )
8	5 6 7	mp2an	⊢ ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 𝐴 ) ) ↦ 0 ) ∈ ( mzPoly ‘ ( 1 ... 𝐴 ) )
9		eq0rabdioph	⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 𝐴 ) ) ↦ 0 ) ∈ ( mzPoly ‘ ( 1 ... 𝐴 ) ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 0 = 0 } ∈ ( Dioph ‘ 𝐴 ) )
10	8 9	mpan2	⊢ ( 𝐴 ∈ ℕ0 → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∣ 0 = 0 } ∈ ( Dioph ‘ 𝐴 ) )
11	4 10	eqeltrid	⊢ ( 𝐴 ∈ ℕ0 → ( ℕ0 ↑m ( 1 ... 𝐴 ) ) ∈ ( Dioph ‘ 𝐴 ) )