Metamath Proof Explorer

Theorem eldiophb

Description: Initial expression of Diophantine property of a set. (Contributed by Stefan O'Rear, 5-Oct-2014) (Revised by Mario Carneiro, 22-Sep-2015)

Ref Expression
Assertion eldiophb 
|- ( D e. ( Dioph ` N ) <-> ( N e. NN0 /\ E. k e. ( ZZ>= ` N ) E. p e. ( mzPoly ` ( 1 ... k ) ) D = { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )

Proof

Step Hyp Ref Expression
1 df-dioph 
 |-  Dioph = ( n e. NN0 |-> ran ( k e. ( ZZ>= ` n ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 ) } ) )
2 1 dmmptss 
 |-  dom Dioph C_ NN0
3 elfvdm 
 |-  ( D e. ( Dioph ` N ) -> N e. dom Dioph )
4 2 3 sseldi 
 |-  ( D e. ( Dioph ` N ) -> N e. NN0 )
5 fveq2 
 |-  ( n = N -> ( ZZ>= ` n ) = ( ZZ>= ` N ) )
6 eqidd 
 |-  ( n = N -> ( mzPoly ` ( 1 ... k ) ) = ( mzPoly ` ( 1 ... k ) ) )
7 oveq2 
 |-  ( n = N -> ( 1 ... n ) = ( 1 ... N ) )
8 7 reseq2d 
 |-  ( n = N -> ( u |` ( 1 ... n ) ) = ( u |` ( 1 ... N ) ) )
9 8 eqeq2d 
 |-  ( n = N -> ( t = ( u |` ( 1 ... n ) ) <-> t = ( u |` ( 1 ... N ) ) ) )
10 9 anbi1d 
 |-  ( n = N -> ( ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 ) <-> ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) ) )
11 10 rexbidv 
 |-  ( n = N -> ( E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 ) <-> E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) ) )
12 11 abbidv 
 |-  ( n = N -> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 ) } = { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } )
13 5 6 12 mpoeq123dv 
 |-  ( n = N -> ( k e. ( ZZ>= ` n ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 ) } ) = ( k e. ( ZZ>= ` N ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
14 13 rneqd 
 |-  ( n = N -> ran ( k e. ( ZZ>= ` n ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 ) } ) = ran ( k e. ( ZZ>= ` N ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
15 ovex 
 |-  ( NN0 ^m ( 1 ... N ) ) e. _V
16 15 pwex 
 |-  ~P ( NN0 ^m ( 1 ... N ) ) e. _V
17 eqid 
 |-  ( k e. ( ZZ>= ` N ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) = ( k e. ( ZZ>= ` N ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } )
18 17 rnmpo 
 |-  ran ( k e. ( ZZ>= ` N ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) = { d | E. k e. ( ZZ>= ` N ) E. p e. ( mzPoly ` ( 1 ... k ) ) d = { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } }
19 elmapi 
 |-  ( u e. ( NN0 ^m ( 1 ... k ) ) -> u : ( 1 ... k ) --> NN0 )
20 fzss2 
 |-  ( k e. ( ZZ>= ` N ) -> ( 1 ... N ) C_ ( 1 ... k ) )
21 fssres 
 |-  ( ( u : ( 1 ... k ) --> NN0 /\ ( 1 ... N ) C_ ( 1 ... k ) ) -> ( u |` ( 1 ... N ) ) : ( 1 ... N ) --> NN0 )
22 19 20 21 syl2anr 
 |-  ( ( k e. ( ZZ>= ` N ) /\ u e. ( NN0 ^m ( 1 ... k ) ) ) -> ( u |` ( 1 ... N ) ) : ( 1 ... N ) --> NN0 )
23 nn0ex 
 |-  NN0 e. _V
24 ovex 
 |-  ( 1 ... N ) e. _V
25 23 24 elmap 
 |-  ( ( u |` ( 1 ... N ) ) e. ( NN0 ^m ( 1 ... N ) ) <-> ( u |` ( 1 ... N ) ) : ( 1 ... N ) --> NN0 )
26 22 25 sylibr 
 |-  ( ( k e. ( ZZ>= ` N ) /\ u e. ( NN0 ^m ( 1 ... k ) ) ) -> ( u |` ( 1 ... N ) ) e. ( NN0 ^m ( 1 ... N ) ) )
27 eleq1 
 |-  ( t = ( u |` ( 1 ... N ) ) -> ( t e. ( NN0 ^m ( 1 ... N ) ) <-> ( u |` ( 1 ... N ) ) e. ( NN0 ^m ( 1 ... N ) ) ) )
28 27 adantr 
 |-  ( ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) -> ( t e. ( NN0 ^m ( 1 ... N ) ) <-> ( u |` ( 1 ... N ) ) e. ( NN0 ^m ( 1 ... N ) ) ) )
29 26 28 syl5ibrcom 
 |-  ( ( k e. ( ZZ>= ` N ) /\ u e. ( NN0 ^m ( 1 ... k ) ) ) -> ( ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) -> t e. ( NN0 ^m ( 1 ... N ) ) ) )
30 29 rexlimdva 
 |-  ( k e. ( ZZ>= ` N ) -> ( E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) -> t e. ( NN0 ^m ( 1 ... N ) ) ) )
31 30 abssdv 
 |-  ( k e. ( ZZ>= ` N ) -> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } C_ ( NN0 ^m ( 1 ... N ) ) )
32 15 elpw2 
 |-  ( { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } e. ~P ( NN0 ^m ( 1 ... N ) ) <-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } C_ ( NN0 ^m ( 1 ... N ) ) )
33 31 32 sylibr 
 |-  ( k e. ( ZZ>= ` N ) -> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } e. ~P ( NN0 ^m ( 1 ... N ) ) )
34 eleq1 
 |-  ( d = { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } -> ( d e. ~P ( NN0 ^m ( 1 ... N ) ) <-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } e. ~P ( NN0 ^m ( 1 ... N ) ) ) )
35 33 34 syl5ibrcom 
 |-  ( k e. ( ZZ>= ` N ) -> ( d = { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } -> d e. ~P ( NN0 ^m ( 1 ... N ) ) ) )
36 35 rexlimdvw 
 |-  ( k e. ( ZZ>= ` N ) -> ( E. p e. ( mzPoly ` ( 1 ... k ) ) d = { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } -> d e. ~P ( NN0 ^m ( 1 ... N ) ) ) )
37 36 rexlimiv 
 |-  ( E. k e. ( ZZ>= ` N ) E. p e. ( mzPoly ` ( 1 ... k ) ) d = { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } -> d e. ~P ( NN0 ^m ( 1 ... N ) ) )
38 37 abssi 
 |-  { d | E. k e. ( ZZ>= ` N ) E. p e. ( mzPoly ` ( 1 ... k ) ) d = { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } } C_ ~P ( NN0 ^m ( 1 ... N ) )
39 18 38 eqsstri 
 |-  ran ( k e. ( ZZ>= ` N ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) C_ ~P ( NN0 ^m ( 1 ... N ) )
40 16 39 ssexi 
 |-  ran ( k e. ( ZZ>= ` N ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) e. _V
41 14 1 40 fvmpt 
 |-  ( N e. NN0 -> ( Dioph ` N ) = ran ( k e. ( ZZ>= ` N ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
42 41 eleq2d 
 |-  ( N e. NN0 -> ( D e. ( Dioph ` N ) <-> D e. ran ( k e. ( ZZ>= ` N ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) ) )
43 ovex 
 |-  ( NN0 ^m ( 1 ... k ) ) e. _V
44 43 abrexex 
 |-  { t | E. u e. ( NN0 ^m ( 1 ... k ) ) t = ( u |` ( 1 ... N ) ) } e. _V
45 simpl 
 |-  ( ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) -> t = ( u |` ( 1 ... N ) ) )
46 45 reximi 
 |-  ( E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) -> E. u e. ( NN0 ^m ( 1 ... k ) ) t = ( u |` ( 1 ... N ) ) )
47 46 ss2abi 
 |-  { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } C_ { t | E. u e. ( NN0 ^m ( 1 ... k ) ) t = ( u |` ( 1 ... N ) ) }
48 44 47 ssexi 
 |-  { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } e. _V
49 17 48 elrnmpo 
 |-  ( D e. ran ( k e. ( ZZ>= ` N ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) <-> E. k e. ( ZZ>= ` N ) E. p e. ( mzPoly ` ( 1 ... k ) ) D = { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } )
50 42 49 bitrdi 
 |-  ( N e. NN0 -> ( D e. ( Dioph ` N ) <-> E. k e. ( ZZ>= ` N ) E. p e. ( mzPoly ` ( 1 ... k ) ) D = { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
51 4 50 biadanii 
 |-  ( D e. ( Dioph ` N ) <-> ( N e. NN0 /\ E. k e. ( ZZ>= ` N ) E. p e. ( mzPoly ` ( 1 ... k ) ) D = { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )