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 e. NN0 -> ( NN0 ^m ( 1 ... A ) ) e. ( Dioph ` A ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  0 = 0
2 1 rgenw 
 |-  A. a e. ( NN0 ^m ( 1 ... A ) ) 0 = 0
3 rabid2 
 |-  ( ( NN0 ^m ( 1 ... A ) ) = { a e. ( NN0 ^m ( 1 ... A ) ) | 0 = 0 } <-> A. a e. ( NN0 ^m ( 1 ... A ) ) 0 = 0 )
4 2 3 mpbir 
 |-  ( NN0 ^m ( 1 ... A ) ) = { a e. ( NN0 ^m ( 1 ... A ) ) | 0 = 0 }
5 ovex 
 |-  ( 1 ... A ) e. _V
6 0z 
 |-  0 e. ZZ
7 mzpconstmpt 
 |-  ( ( ( 1 ... A ) e. _V /\ 0 e. ZZ ) -> ( a e. ( ZZ ^m ( 1 ... A ) ) |-> 0 ) e. ( mzPoly ` ( 1 ... A ) ) )
8 5 6 7 mp2an 
 |-  ( a e. ( ZZ ^m ( 1 ... A ) ) |-> 0 ) e. ( mzPoly ` ( 1 ... A ) )
9 eq0rabdioph 
 |-  ( ( A e. NN0 /\ ( a e. ( ZZ ^m ( 1 ... A ) ) |-> 0 ) e. ( mzPoly ` ( 1 ... A ) ) ) -> { a e. ( NN0 ^m ( 1 ... A ) ) | 0 = 0 } e. ( Dioph ` A ) )
10 8 9 mpan2 
 |-  ( A e. NN0 -> { a e. ( NN0 ^m ( 1 ... A ) ) | 0 = 0 } e. ( Dioph ` A ) )
11 4 10 eqeltrid 
 |-  ( A e. NN0 -> ( NN0 ^m ( 1 ... A ) ) e. ( Dioph ` A ) )