Metamath Proof Explorer

Theorem 7rexfrabdioph

Description: Diophantine set builder for existential quantifier, explicit substitution, seven 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 )
rexfrabdioph.3 
|- K = ( L + 1 )
rexfrabdioph.4 
|- J = ( K + 1 )
rexfrabdioph.5 
|- I = ( J + 1 )
rexfrabdioph.6 
|- H = ( I + 1 )
rexfrabdioph.7 
|- G = ( H + 1 )
Assertion 7rexfrabdioph 
|- ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... G ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph } e. ( Dioph ` G ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q 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 rexfrabdioph.4 
 |-  J = ( K + 1 )
5 rexfrabdioph.5 
 |-  I = ( J + 1 )
6 rexfrabdioph.6 
 |-  H = ( I + 1 )
7 rexfrabdioph.7 
 |-  G = ( H + 1 )
8 sbc2rex 
 |-  ( [. ( a ` M ) / v ]. E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 ph <-> E. w e. NN0 E. x e. NN0 [. ( a ` M ) / v ]. E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 ph )
9 sbc4rex 
 |-  ( [. ( a ` M ) / v ]. E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 ph <-> E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 [. ( a ` M ) / v ]. ph )
10 9 2rexbii 
 |-  ( E. w e. NN0 E. x e. NN0 [. ( a ` M ) / v ]. E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 ph <-> E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 [. ( a ` M ) / v ]. ph )
11 8 10 bitri 
 |-  ( [. ( a ` M ) / v ]. E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 ph <-> E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 [. ( a ` M ) / v ]. ph )
12 11 sbcbii 
 |-  ( [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 ph <-> [. ( a |` ( 1 ... N ) ) / u ]. E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 [. ( a ` M ) / v ]. ph )
13 sbc2rex 
 |-  ( [. ( a |` ( 1 ... N ) ) / u ]. E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 [. ( a ` M ) / v ]. ph <-> E. w e. NN0 E. x e. NN0 [. ( a |` ( 1 ... N ) ) / u ]. E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 [. ( a ` M ) / v ]. ph )
14 sbc4rex 
 |-  ( [. ( a |` ( 1 ... N ) ) / u ]. E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 [. ( a ` M ) / v ]. ph <-> E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph )
15 14 2rexbii 
 |-  ( E. w e. NN0 E. x e. NN0 [. ( a |` ( 1 ... N ) ) / u ]. E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 [. ( a ` M ) / v ]. ph <-> E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph )
16 12 13 15 3bitri 
 |-  ( [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 ph <-> E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph )
17 16 rabbii 
 |-  { a e. ( NN0 ^m ( 1 ... M ) ) | [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 ph } = { a e. ( NN0 ^m ( 1 ... M ) ) | E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph }
18 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
19 1 18 eqeltrid 
 |-  ( N e. NN0 -> M e. NN )
20 19 nnnn0d 
 |-  ( N e. NN0 -> M e. NN0 )
21 20 adantr 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... G ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph } e. ( Dioph ` G ) ) -> M e. NN0 )
22 sbcrot3 
 |-  ( [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( a ` M ) / v ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph )
23 22 sbcbii 
 |-  ( [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( a |` ( 1 ... N ) ) / u ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( a ` M ) / v ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph )
24 sbcrot3 
 |-  ( [. ( a |` ( 1 ... N ) ) / u ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( a ` M ) / v ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph )
25 sbcrot5 
 |-  ( [. ( a ` M ) / v ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. [. ( a ` M ) / v ]. ph )
26 25 sbcbii 
 |-  ( [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( a |` ( 1 ... N ) ) / u ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. [. ( a ` M ) / v ]. ph )
27 sbcrot5 
 |-  ( [. ( a |` ( 1 ... N ) ) / u ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. [. ( a ` M ) / v ]. ph <-> [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph )
28 26 27 bitri 
 |-  ( [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph )
29 28 sbcbii 
 |-  ( [. ( t ` K ) / x ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph )
30 29 sbcbii 
 |-  ( [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph )
31 23 24 30 3bitri 
 |-  ( [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph )
32 31 sbcbii 
 |-  ( [. ( t |` ( 1 ... M ) ) / a ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( t |` ( 1 ... M ) ) / a ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph )
33 reseq1 
 |-  ( a = ( t |` ( 1 ... M ) ) -> ( a |` ( 1 ... N ) ) = ( ( t |` ( 1 ... M ) ) |` ( 1 ... N ) ) )
34 33 sbccomieg 
 |-  ( [. ( t |` ( 1 ... M ) ) / a ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( ( t |` ( 1 ... M ) ) |` ( 1 ... N ) ) / u ]. [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph )
35 fzssp1 
 |-  ( 1 ... N ) C_ ( 1 ... ( N + 1 ) )
36 1 oveq2i 
 |-  ( 1 ... M ) = ( 1 ... ( N + 1 ) )
37 35 36 sseqtrri 
 |-  ( 1 ... N ) C_ ( 1 ... M )
38 resabs1 
 |-  ( ( 1 ... N ) C_ ( 1 ... M ) -> ( ( t |` ( 1 ... M ) ) |` ( 1 ... N ) ) = ( t |` ( 1 ... N ) ) )
39 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 ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( t |` ( 1 ... N ) ) / u ]. [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph ) )
40 37 38 39 mp2b 
 |-  ( [. ( ( t |` ( 1 ... M ) ) |` ( 1 ... N ) ) / u ]. [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( t |` ( 1 ... N ) ) / u ]. [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph )
41 vex 
 |-  t e. _V
42 41 resex 
 |-  ( t |` ( 1 ... M ) ) e. _V
43 fveq1 
 |-  ( a = ( t |` ( 1 ... M ) ) -> ( a ` M ) = ( ( t |` ( 1 ... M ) ) ` M ) )
44 43 sbcco3gw 
 |-  ( ( t |` ( 1 ... M ) ) e. _V -> ( [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( ( t |` ( 1 ... M ) ) ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph ) )
45 42 44 ax-mp 
 |-  ( [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( ( t |` ( 1 ... M ) ) ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph )
46 elfz1end 
 |-  ( M e. NN <-> M e. ( 1 ... M ) )
47 19 46 sylib 
 |-  ( N e. NN0 -> M e. ( 1 ... M ) )
48 fvres 
 |-  ( M e. ( 1 ... M ) -> ( ( t |` ( 1 ... M ) ) ` M ) = ( t ` M ) )
49 dfsbcq 
 |-  ( ( ( t |` ( 1 ... M ) ) ` M ) = ( t ` M ) -> ( [. ( ( t |` ( 1 ... M ) ) ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph ) )
50 47 48 49 3syl 
 |-  ( N e. NN0 -> ( [. ( ( t |` ( 1 ... M ) ) ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph ) )
51 45 50 syl5bb 
 |-  ( N e. NN0 -> ( [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph ) )
52 51 sbcbidv 
 |-  ( N e. NN0 -> ( [. ( t |` ( 1 ... N ) ) / u ]. [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph ) )
53 40 52 syl5bb 
 |-  ( N e. NN0 -> ( [. ( ( t |` ( 1 ... M ) ) |` ( 1 ... N ) ) / u ]. [. ( t |` ( 1 ... M ) ) / a ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph ) )
54 34 53 syl5bb 
 |-  ( N e. NN0 -> ( [. ( t |` ( 1 ... M ) ) / a ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph <-> [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph ) )
55 32 54 bitr3id 
 |-  ( N e. NN0 -> ( [. ( t |` ( 1 ... M ) ) / a ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph <-> [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph ) )
56 55 rabbidv 
 |-  ( N e. NN0 -> { t e. ( NN0 ^m ( 1 ... G ) ) | [. ( t |` ( 1 ... M ) ) / a ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph } = { t e. ( NN0 ^m ( 1 ... G ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph } )
57 56 eleq1d 
 |-  ( N e. NN0 -> ( { t e. ( NN0 ^m ( 1 ... G ) ) | [. ( t |` ( 1 ... M ) ) / a ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph } e. ( Dioph ` G ) <-> { t e. ( NN0 ^m ( 1 ... G ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph } e. ( Dioph ` G ) ) )
58 57 biimpar 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... G ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph } e. ( Dioph ` G ) ) -> { t e. ( NN0 ^m ( 1 ... G ) ) | [. ( t |` ( 1 ... M ) ) / a ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph } e. ( Dioph ` G ) )
59 2 3 4 5 6 7 6rexfrabdioph 
 |-  ( ( M e. NN0 /\ { t e. ( NN0 ^m ( 1 ... G ) ) | [. ( t |` ( 1 ... M ) ) / a ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph } e. ( Dioph ` G ) ) -> { a e. ( NN0 ^m ( 1 ... M ) ) | E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph } e. ( Dioph ` M ) )
60 21 58 59 syl2anc 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... G ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph } e. ( Dioph ` G ) ) -> { a e. ( NN0 ^m ( 1 ... M ) ) | E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. ph } e. ( Dioph ` M ) )
61 17 60 eqeltrid 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... G ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph } e. ( Dioph ` G ) ) -> { a e. ( NN0 ^m ( 1 ... M ) ) | [. ( a |` ( 1 ... N ) ) / u ]. [. ( a ` M ) / v ]. E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 ph } e. ( Dioph ` M ) )
62 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 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 ph } e. ( Dioph ` M ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 ph } e. ( Dioph ` N ) )
63 61 62 syldan 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... G ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph } e. ( Dioph ` G ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 ph } e. ( Dioph ` N ) )