Metamath Proof Explorer

Theorem 2rexfrabdioph

Description: Diophantine set builder for existential quantifier, explicit substitution, two variables. (Contributed by Stefan O'Rear, 11-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypotheses rexfrabdioph.1 
|- M = ( N + 1 )
rexfrabdioph.2 
|- L = ( M + 1 )
Assertion 2rexfrabdioph 
|- ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... L ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. ph } e. ( Dioph ` L ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 E. w e. NN0 ph } e. ( Dioph ` N ) )

Proof

Step Hyp Ref Expression
1 rexfrabdioph.1 
 |-  M = ( N + 1 )
2 rexfrabdioph.2 
 |-  L = ( M + 1 )
3 2sbcrex 
 |-  ( [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. E. w e. NN0 ph <-> E. w e. NN0 [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph )
4 3 rabbii 
 |-  { a e. ( NN0 ^m ( 1 ... M ) ) | [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. E. w e. NN0 ph } = { a e. ( NN0 ^m ( 1 ... M ) ) | E. w e. NN0 [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph }
5 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
6 1 5 eqeltrid 
 |-  ( N e. NN0 -> M e. NN0 )
7 6 adantr 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... L ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. ph } e. ( Dioph ` L ) ) -> M e. NN0 )
8 sbcrot3 
 |-  ( [. ( t ` L ) / w ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph <-> [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. ph )
9 8 sbcbii 
 |-  ( [. ( t |` ( 1 ... M ) ) / a ]. [. ( t ` L ) / w ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph <-> [. ( t |` ( 1 ... M ) ) / a ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. ph )
10 reseq1 
 |-  ( a = ( t |` ( 1 ... M ) ) -> ( a |` ( 1 ... N ) ) = ( ( t |` ( 1 ... M ) ) |` ( 1 ... N ) ) )
11 10 sbccomieg 
 |-  ( [. ( t |` ( 1 ... M ) ) / a ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. ph <-> [. ( ( t |` ( 1 ... M ) ) |` ( 1 ... N ) ) / u ]. [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. ph )
12 fzssp1 
 |-  ( 1 ... N ) C_ ( 1 ... ( N + 1 ) )
13 1 oveq2i 
 |-  ( 1 ... M ) = ( 1 ... ( N + 1 ) )
14 12 13 sseqtrri 
 |-  ( 1 ... N ) C_ ( 1 ... M )
15 resabs1 
 |-  ( ( 1 ... N ) C_ ( 1 ... M ) -> ( ( t |` ( 1 ... M ) ) |` ( 1 ... N ) ) = ( t |` ( 1 ... N ) ) )
16 dfsbcq 
 |-  ( ( ( t |` ( 1 ... M ) ) |` ( 1 ... N ) ) = ( t |` ( 1 ... N ) ) -> ( [. ( ( t |` ( 1 ... M ) ) |` ( 1 ... N ) ) / u ]. [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. ph <-> [. ( t |` ( 1 ... N ) ) / u ]. [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. ph ) )
17 14 15 16 mp2b 
 |-  ( [. ( ( t |` ( 1 ... M ) ) |` ( 1 ... N ) ) / u ]. [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. ph <-> [. ( t |` ( 1 ... N ) ) / u ]. [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. ph )
18 vex 
 |-  t e. _V
19 18 resex 
 |-  ( t |` ( 1 ... M ) ) e. _V
20 fveq1 
 |-  ( a = ( t |` ( 1 ... M ) ) -> ( a ` M ) = ( ( t |` ( 1 ... M ) ) ` M ) )
21 20 sbcco3gw 
 |-  ( ( t |` ( 1 ... M ) ) e. _V -> ( [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. ph <-> [. ( ( t |` ( 1 ... M ) ) ` M ) / v ]. [. ( t ` L ) / w ]. ph ) )
22 19 21 ax-mp 
 |-  ( [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. ph <-> [. ( ( t |` ( 1 ... M ) ) ` M ) / v ]. [. ( t ` L ) / w ]. ph )
23 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
24 1 23 eqeltrid 
 |-  ( N e. NN0 -> M e. NN )
25 elfz1end 
 |-  ( M e. NN <-> M e. ( 1 ... M ) )
26 24 25 sylib 
 |-  ( N e. NN0 -> M e. ( 1 ... M ) )
27 fvres 
 |-  ( M e. ( 1 ... M ) -> ( ( t |` ( 1 ... M ) ) ` M ) = ( t ` M ) )
28 dfsbcq 
 |-  ( ( ( t |` ( 1 ... M ) ) ` M ) = ( t ` M ) -> ( [. ( ( t |` ( 1 ... M ) ) ` M ) / v ]. [. ( t ` L ) / w ]. ph <-> [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. ph ) )
29 26 27 28 3syl 
 |-  ( N e. NN0 -> ( [. ( ( t |` ( 1 ... M ) ) ` M ) / v ]. [. ( t ` L ) / w ]. ph <-> [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. ph ) )
30 22 29 syl5bb 
 |-  ( N e. NN0 -> ( [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. ph <-> [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. ph ) )
31 30 sbcbidv 
 |-  ( N e. NN0 -> ( [. ( t |` ( 1 ... N ) ) / u ]. [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. ph <-> [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. ph ) )
32 17 31 syl5bb 
 |-  ( N e. NN0 -> ( [. ( ( t |` ( 1 ... M ) ) |` ( 1 ... N ) ) / u ]. [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. ph <-> [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. ph ) )
33 11 32 syl5bb 
 |-  ( N e. NN0 -> ( [. ( t |` ( 1 ... M ) ) / a ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. ph <-> [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. ph ) )
34 9 33 bitr2id 
 |-  ( N e. NN0 -> ( [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. ph <-> [. ( t |` ( 1 ... M ) ) / a ]. [. ( t ` L ) / w ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph ) )
35 34 rabbidv 
 |-  ( N e. NN0 -> { t e. ( NN0 ^m ( 1 ... L ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. ph } = { t e. ( NN0 ^m ( 1 ... L ) ) | [. ( t |` ( 1 ... M ) ) / a ]. [. ( t ` L ) / w ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph } )
36 35 eleq1d 
 |-  ( N e. NN0 -> ( { t e. ( NN0 ^m ( 1 ... L ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. ph } e. ( Dioph ` L ) <-> { t e. ( NN0 ^m ( 1 ... L ) ) | [. ( t |` ( 1 ... M ) ) / a ]. [. ( t ` L ) / w ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph } e. ( Dioph ` L ) ) )
37 36 biimpa 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... L ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. ph } e. ( Dioph ` L ) ) -> { t e. ( NN0 ^m ( 1 ... L ) ) | [. ( t |` ( 1 ... M ) ) / a ]. [. ( t ` L ) / w ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph } e. ( Dioph ` L ) )
38 2 rexfrabdioph 
 |-  ( ( M e. NN0 /\ { t e. ( NN0 ^m ( 1 ... L ) ) | [. ( t |` ( 1 ... M ) ) / a ]. [. ( t ` L ) / w ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph } e. ( Dioph ` L ) ) -> { a e. ( NN0 ^m ( 1 ... M ) ) | E. w e. NN0 [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph } e. ( Dioph ` M ) )
39 7 37 38 syl2anc 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... L ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. ph } e. ( Dioph ` L ) ) -> { a e. ( NN0 ^m ( 1 ... M ) ) | E. w e. NN0 [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph } e. ( Dioph ` M ) )
40 4 39 eqeltrid 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... L ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. ph } e. ( Dioph ` L ) ) -> { a e. ( NN0 ^m ( 1 ... M ) ) | [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. E. w e. NN0 ph } e. ( Dioph ` M ) )
41 1 rexfrabdioph 
 |-  ( ( N e. NN0 /\ { a e. ( NN0 ^m ( 1 ... M ) ) | [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. E. w e. NN0 ph } e. ( Dioph ` M ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 E. w e. NN0 ph } e. ( Dioph ` N ) )
42 40 41 syldan 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... L ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. ph } e. ( Dioph ` L ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 E. w e. NN0 ph } e. ( Dioph ` N ) )