Metamath Proof Explorer

Theorem eldiophss

Description: Diophantine sets are sets of tuples of nonnegative integers. (Contributed by Stefan O'Rear, 10-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Assertion eldiophss 
|- ( A e. ( Dioph ` B ) -> A C_ ( NN0 ^m ( 1 ... B ) ) )

Proof

Step Hyp Ref Expression
1 eldioph3b 
 |-  ( A e. ( Dioph ` B ) <-> ( B e. NN0 /\ E. a e. ( mzPoly ` NN ) A = { b | E. c e. ( NN0 ^m NN ) ( b = ( c |` ( 1 ... B ) ) /\ ( a ` c ) = 0 ) } ) )
2 simpr 
 |-  ( ( ( B e. NN0 /\ a e. ( mzPoly ` NN ) ) /\ A = { b | E. c e. ( NN0 ^m NN ) ( b = ( c |` ( 1 ... B ) ) /\ ( a ` c ) = 0 ) } ) -> A = { b | E. c e. ( NN0 ^m NN ) ( b = ( c |` ( 1 ... B ) ) /\ ( a ` c ) = 0 ) } )
3 vex 
 |-  d e. _V
4 eqeq1 
 |-  ( b = d -> ( b = ( c |` ( 1 ... B ) ) <-> d = ( c |` ( 1 ... B ) ) ) )
5 4 anbi1d 
 |-  ( b = d -> ( ( b = ( c |` ( 1 ... B ) ) /\ ( a ` c ) = 0 ) <-> ( d = ( c |` ( 1 ... B ) ) /\ ( a ` c ) = 0 ) ) )
6 5 rexbidv 
 |-  ( b = d -> ( E. c e. ( NN0 ^m NN ) ( b = ( c |` ( 1 ... B ) ) /\ ( a ` c ) = 0 ) <-> E. c e. ( NN0 ^m NN ) ( d = ( c |` ( 1 ... B ) ) /\ ( a ` c ) = 0 ) ) )
7 3 6 elab 
 |-  ( d e. { b | E. c e. ( NN0 ^m NN ) ( b = ( c |` ( 1 ... B ) ) /\ ( a ` c ) = 0 ) } <-> E. c e. ( NN0 ^m NN ) ( d = ( c |` ( 1 ... B ) ) /\ ( a ` c ) = 0 ) )
8 simpr 
 |-  ( ( ( ( B e. NN0 /\ a e. ( mzPoly ` NN ) ) /\ c e. ( NN0 ^m NN ) ) /\ d = ( c |` ( 1 ... B ) ) ) -> d = ( c |` ( 1 ... B ) ) )
9 elfznn 
 |-  ( a e. ( 1 ... B ) -> a e. NN )
10 9 ssriv 
 |-  ( 1 ... B ) C_ NN
11 elmapssres 
 |-  ( ( c e. ( NN0 ^m NN ) /\ ( 1 ... B ) C_ NN ) -> ( c |` ( 1 ... B ) ) e. ( NN0 ^m ( 1 ... B ) ) )
12 10 11 mpan2 
 |-  ( c e. ( NN0 ^m NN ) -> ( c |` ( 1 ... B ) ) e. ( NN0 ^m ( 1 ... B ) ) )
13 12 ad2antlr 
 |-  ( ( ( ( B e. NN0 /\ a e. ( mzPoly ` NN ) ) /\ c e. ( NN0 ^m NN ) ) /\ d = ( c |` ( 1 ... B ) ) ) -> ( c |` ( 1 ... B ) ) e. ( NN0 ^m ( 1 ... B ) ) )
14 8 13 eqeltrd 
 |-  ( ( ( ( B e. NN0 /\ a e. ( mzPoly ` NN ) ) /\ c e. ( NN0 ^m NN ) ) /\ d = ( c |` ( 1 ... B ) ) ) -> d e. ( NN0 ^m ( 1 ... B ) ) )
15 14 ex 
 |-  ( ( ( B e. NN0 /\ a e. ( mzPoly ` NN ) ) /\ c e. ( NN0 ^m NN ) ) -> ( d = ( c |` ( 1 ... B ) ) -> d e. ( NN0 ^m ( 1 ... B ) ) ) )
16 15 adantrd 
 |-  ( ( ( B e. NN0 /\ a e. ( mzPoly ` NN ) ) /\ c e. ( NN0 ^m NN ) ) -> ( ( d = ( c |` ( 1 ... B ) ) /\ ( a ` c ) = 0 ) -> d e. ( NN0 ^m ( 1 ... B ) ) ) )
17 16 rexlimdva 
 |-  ( ( B e. NN0 /\ a e. ( mzPoly ` NN ) ) -> ( E. c e. ( NN0 ^m NN ) ( d = ( c |` ( 1 ... B ) ) /\ ( a ` c ) = 0 ) -> d e. ( NN0 ^m ( 1 ... B ) ) ) )
18 7 17 syl5bi 
 |-  ( ( B e. NN0 /\ a e. ( mzPoly ` NN ) ) -> ( d e. { b | E. c e. ( NN0 ^m NN ) ( b = ( c |` ( 1 ... B ) ) /\ ( a ` c ) = 0 ) } -> d e. ( NN0 ^m ( 1 ... B ) ) ) )
19 18 ssrdv 
 |-  ( ( B e. NN0 /\ a e. ( mzPoly ` NN ) ) -> { b | E. c e. ( NN0 ^m NN ) ( b = ( c |` ( 1 ... B ) ) /\ ( a ` c ) = 0 ) } C_ ( NN0 ^m ( 1 ... B ) ) )
20 19 adantr 
 |-  ( ( ( B e. NN0 /\ a e. ( mzPoly ` NN ) ) /\ A = { b | E. c e. ( NN0 ^m NN ) ( b = ( c |` ( 1 ... B ) ) /\ ( a ` c ) = 0 ) } ) -> { b | E. c e. ( NN0 ^m NN ) ( b = ( c |` ( 1 ... B ) ) /\ ( a ` c ) = 0 ) } C_ ( NN0 ^m ( 1 ... B ) ) )
21 2 20 eqsstrd 
 |-  ( ( ( B e. NN0 /\ a e. ( mzPoly ` NN ) ) /\ A = { b | E. c e. ( NN0 ^m NN ) ( b = ( c |` ( 1 ... B ) ) /\ ( a ` c ) = 0 ) } ) -> A C_ ( NN0 ^m ( 1 ... B ) ) )
22 21 r19.29an 
 |-  ( ( B e. NN0 /\ E. a e. ( mzPoly ` NN ) A = { b | E. c e. ( NN0 ^m NN ) ( b = ( c |` ( 1 ... B ) ) /\ ( a ` c ) = 0 ) } ) -> A C_ ( NN0 ^m ( 1 ... B ) ) )
23 1 22 sylbi 
 |-  ( A e. ( Dioph ` B ) -> A C_ ( NN0 ^m ( 1 ... B ) ) )