Metamath Proof Explorer

Theorem 4rexfrabdioph

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