Metamath Proof Explorer

Theorem 3rexfrabdioph

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

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

Proof

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