Metamath Proof Explorer

Theorem 6rexfrabdioph

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