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 sselid
 |-  ( 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 ) } ) )