Theorem eldioph3b

Description: Define Diophantine sets in terms of polynomials with variables indexed by NN . This avoids a quantifier over the number of witness variables and will be easier to use than eldiophb in most cases. (Contributed by Stefan O'Rear, 10-Oct-2014)

	Ref	Expression
Assertion	eldioph3b	⊢ ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℕ0 ∧ ∃ 𝑝 ∈ ( mzPoly ‘ ℕ ) 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		eldiophelnn0	⊢ ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) → 𝑁 ∈ ℕ0 )
2		nnex	⊢ ℕ ∈ V
3		1z	⊢ 1 ∈ ℤ
4		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
5	4	uzinf	⊢ ( 1 ∈ ℤ → ¬ ℕ ∈ Fin )
6	3 5	ax-mp	⊢ ¬ ℕ ∈ Fin
7		elfznn	⊢ ( 𝑝 ∈ ( 1 ... 𝑁 ) → 𝑝 ∈ ℕ )
8	7	ssriv	⊢ ( 1 ... 𝑁 ) ⊆ ℕ
9		eldioph2b	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ℕ ∈ V ) ∧ ( ¬ ℕ ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ ℕ ) ) → ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑝 ∈ ( mzPoly ‘ ℕ ) 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
10	6 8 9	mpanr12	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ℕ ∈ V ) → ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑝 ∈ ( mzPoly ‘ ℕ ) 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
11	2 10	mpan2	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑝 ∈ ( mzPoly ‘ ℕ ) 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
12	1 11	biadanii	⊢ ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℕ0 ∧ ∃ 𝑝 ∈ ( mzPoly ‘ ℕ ) 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )