Metamath Proof Explorer

Theorem rexrabdioph

Description: Diophantine set builder for existential quantification. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Hypotheses rexrabdioph.1 
|- M = ( N + 1 )
rexrabdioph.2 
|- ( v = ( t ` M ) -> ( ps <-> ch ) )
rexrabdioph.3 
|- ( u = ( t |` ( 1 ... N ) ) -> ( ch <-> ph ) )
Assertion rexrabdioph 
|- ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... M ) ) | ph } e. ( Dioph ` M ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 ps } e. ( Dioph ` N ) )

Proof

Step Hyp Ref Expression
1 rexrabdioph.1 
 |-  M = ( N + 1 )
2 rexrabdioph.2 
 |-  ( v = ( t ` M ) -> ( ps <-> ch ) )
3 rexrabdioph.3 
 |-  ( u = ( t |` ( 1 ... N ) ) -> ( ch <-> ph ) )
4 df-rab 
 |-  { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 [. b / v ]. [. a / u ]. ps } = { a | ( a e. ( NN0 ^m ( 1 ... N ) ) /\ E. b e. NN0 [. b / v ]. [. a / u ]. ps ) }
5 dfsbcq 
 |-  ( b = c -> ( [. b / v ]. [. a / u ]. ps <-> [. c / v ]. [. a / u ]. ps ) )
6 5 cbvrexvw 
 |-  ( E. b e. NN0 [. b / v ]. [. a / u ]. ps <-> E. c e. NN0 [. c / v ]. [. a / u ]. ps )
7 6 anbi2i 
 |-  ( ( a e. ( NN0 ^m ( 1 ... N ) ) /\ E. b e. NN0 [. b / v ]. [. a / u ]. ps ) <-> ( a e. ( NN0 ^m ( 1 ... N ) ) /\ E. c e. NN0 [. c / v ]. [. a / u ]. ps ) )
8 r19.42v 
 |-  ( E. c e. NN0 ( a e. ( NN0 ^m ( 1 ... N ) ) /\ [. c / v ]. [. a / u ]. ps ) <-> ( a e. ( NN0 ^m ( 1 ... N ) ) /\ E. c e. NN0 [. c / v ]. [. a / u ]. ps ) )
9 7 8 bitr4i 
 |-  ( ( a e. ( NN0 ^m ( 1 ... N ) ) /\ E. b e. NN0 [. b / v ]. [. a / u ]. ps ) <-> E. c e. NN0 ( a e. ( NN0 ^m ( 1 ... N ) ) /\ [. c / v ]. [. a / u ]. ps ) )
10 simpll 
 |-  ( ( ( N e. NN0 /\ c e. NN0 ) /\ a e. ( NN0 ^m ( 1 ... N ) ) ) -> N e. NN0 )
11 simpr 
 |-  ( ( ( N e. NN0 /\ c e. NN0 ) /\ a e. ( NN0 ^m ( 1 ... N ) ) ) -> a e. ( NN0 ^m ( 1 ... N ) ) )
12 simplr 
 |-  ( ( ( N e. NN0 /\ c e. NN0 ) /\ a e. ( NN0 ^m ( 1 ... N ) ) ) -> c e. NN0 )
13 1 mapfzcons 
 |-  ( ( N e. NN0 /\ a e. ( NN0 ^m ( 1 ... N ) ) /\ c e. NN0 ) -> ( a u. { <. M , c >. } ) e. ( NN0 ^m ( 1 ... M ) ) )
14 10 11 12 13 syl3anc 
 |-  ( ( ( N e. NN0 /\ c e. NN0 ) /\ a e. ( NN0 ^m ( 1 ... N ) ) ) -> ( a u. { <. M , c >. } ) e. ( NN0 ^m ( 1 ... M ) ) )
15 14 adantrr 
 |-  ( ( ( N e. NN0 /\ c e. NN0 ) /\ ( a e. ( NN0 ^m ( 1 ... N ) ) /\ [. c / v ]. [. a / u ]. ps ) ) -> ( a u. { <. M , c >. } ) e. ( NN0 ^m ( 1 ... M ) ) )
16 1 mapfzcons2 
 |-  ( ( a e. ( NN0 ^m ( 1 ... N ) ) /\ c e. NN0 ) -> ( ( a u. { <. M , c >. } ) ` M ) = c )
17 11 12 16 syl2anc 
 |-  ( ( ( N e. NN0 /\ c e. NN0 ) /\ a e. ( NN0 ^m ( 1 ... N ) ) ) -> ( ( a u. { <. M , c >. } ) ` M ) = c )
18 17 eqcomd 
 |-  ( ( ( N e. NN0 /\ c e. NN0 ) /\ a e. ( NN0 ^m ( 1 ... N ) ) ) -> c = ( ( a u. { <. M , c >. } ) ` M ) )
19 1 mapfzcons1 
 |-  ( a e. ( NN0 ^m ( 1 ... N ) ) -> ( ( a u. { <. M , c >. } ) |` ( 1 ... N ) ) = a )
20 19 adantl 
 |-  ( ( ( N e. NN0 /\ c e. NN0 ) /\ a e. ( NN0 ^m ( 1 ... N ) ) ) -> ( ( a u. { <. M , c >. } ) |` ( 1 ... N ) ) = a )
21 20 eqcomd 
 |-  ( ( ( N e. NN0 /\ c e. NN0 ) /\ a e. ( NN0 ^m ( 1 ... N ) ) ) -> a = ( ( a u. { <. M , c >. } ) |` ( 1 ... N ) ) )
22 21 sbceq1d 
 |-  ( ( ( N e. NN0 /\ c e. NN0 ) /\ a e. ( NN0 ^m ( 1 ... N ) ) ) -> ( [. a / u ]. ps <-> [. ( ( a u. { <. M , c >. } ) |` ( 1 ... N ) ) / u ]. ps ) )
23 18 22 sbceqbid 
 |-  ( ( ( N e. NN0 /\ c e. NN0 ) /\ a e. ( NN0 ^m ( 1 ... N ) ) ) -> ( [. c / v ]. [. a / u ]. ps <-> [. ( ( a u. { <. M , c >. } ) ` M ) / v ]. [. ( ( a u. { <. M , c >. } ) |` ( 1 ... N ) ) / u ]. ps ) )
24 23 biimpd 
 |-  ( ( ( N e. NN0 /\ c e. NN0 ) /\ a e. ( NN0 ^m ( 1 ... N ) ) ) -> ( [. c / v ]. [. a / u ]. ps -> [. ( ( a u. { <. M , c >. } ) ` M ) / v ]. [. ( ( a u. { <. M , c >. } ) |` ( 1 ... N ) ) / u ]. ps ) )
25 24 impr 
 |-  ( ( ( N e. NN0 /\ c e. NN0 ) /\ ( a e. ( NN0 ^m ( 1 ... N ) ) /\ [. c / v ]. [. a / u ]. ps ) ) -> [. ( ( a u. { <. M , c >. } ) ` M ) / v ]. [. ( ( a u. { <. M , c >. } ) |` ( 1 ... N ) ) / u ]. ps )
26 21 adantrr 
 |-  ( ( ( N e. NN0 /\ c e. NN0 ) /\ ( a e. ( NN0 ^m ( 1 ... N ) ) /\ [. c / v ]. [. a / u ]. ps ) ) -> a = ( ( a u. { <. M , c >. } ) |` ( 1 ... N ) ) )
27 fveq1 
 |-  ( b = ( a u. { <. M , c >. } ) -> ( b ` M ) = ( ( a u. { <. M , c >. } ) ` M ) )
28 reseq1 
 |-  ( b = ( a u. { <. M , c >. } ) -> ( b |` ( 1 ... N ) ) = ( ( a u. { <. M , c >. } ) |` ( 1 ... N ) ) )
29 28 sbceq1d 
 |-  ( b = ( a u. { <. M , c >. } ) -> ( [. ( b |` ( 1 ... N ) ) / u ]. ps <-> [. ( ( a u. { <. M , c >. } ) |` ( 1 ... N ) ) / u ]. ps ) )
30 27 29 sbceqbid 
 |-  ( b = ( a u. { <. M , c >. } ) -> ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps <-> [. ( ( a u. { <. M , c >. } ) ` M ) / v ]. [. ( ( a u. { <. M , c >. } ) |` ( 1 ... N ) ) / u ]. ps ) )
31 28 eqeq2d 
 |-  ( b = ( a u. { <. M , c >. } ) -> ( a = ( b |` ( 1 ... N ) ) <-> a = ( ( a u. { <. M , c >. } ) |` ( 1 ... N ) ) ) )
32 30 31 anbi12d 
 |-  ( b = ( a u. { <. M , c >. } ) -> ( ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) <-> ( [. ( ( a u. { <. M , c >. } ) ` M ) / v ]. [. ( ( a u. { <. M , c >. } ) |` ( 1 ... N ) ) / u ]. ps /\ a = ( ( a u. { <. M , c >. } ) |` ( 1 ... N ) ) ) ) )
33 32 rspcev 
 |-  ( ( ( a u. { <. M , c >. } ) e. ( NN0 ^m ( 1 ... M ) ) /\ ( [. ( ( a u. { <. M , c >. } ) ` M ) / v ]. [. ( ( a u. { <. M , c >. } ) |` ( 1 ... N ) ) / u ]. ps /\ a = ( ( a u. { <. M , c >. } ) |` ( 1 ... N ) ) ) ) -> E. b e. ( NN0 ^m ( 1 ... M ) ) ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) )
34 15 25 26 33 syl12anc 
 |-  ( ( ( N e. NN0 /\ c e. NN0 ) /\ ( a e. ( NN0 ^m ( 1 ... N ) ) /\ [. c / v ]. [. a / u ]. ps ) ) -> E. b e. ( NN0 ^m ( 1 ... M ) ) ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) )
35 34 rexlimdva2 
 |-  ( N e. NN0 -> ( E. c e. NN0 ( a e. ( NN0 ^m ( 1 ... N ) ) /\ [. c / v ]. [. a / u ]. ps ) -> E. b e. ( NN0 ^m ( 1 ... M ) ) ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) ) )
36 elmapi 
 |-  ( b e. ( NN0 ^m ( 1 ... M ) ) -> b : ( 1 ... M ) --> NN0 )
37 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
38 1 37 eqeltrid 
 |-  ( N e. NN0 -> M e. NN )
39 elfz1end 
 |-  ( M e. NN <-> M e. ( 1 ... M ) )
40 38 39 sylib 
 |-  ( N e. NN0 -> M e. ( 1 ... M ) )
41 ffvelrn 
 |-  ( ( b : ( 1 ... M ) --> NN0 /\ M e. ( 1 ... M ) ) -> ( b ` M ) e. NN0 )
42 36 40 41 syl2anr 
 |-  ( ( N e. NN0 /\ b e. ( NN0 ^m ( 1 ... M ) ) ) -> ( b ` M ) e. NN0 )
43 42 adantr 
 |-  ( ( ( N e. NN0 /\ b e. ( NN0 ^m ( 1 ... M ) ) ) /\ ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) ) -> ( b ` M ) e. NN0 )
44 simprr 
 |-  ( ( ( N e. NN0 /\ b e. ( NN0 ^m ( 1 ... M ) ) ) /\ ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) ) -> a = ( b |` ( 1 ... N ) ) )
45 1 mapfzcons1cl 
 |-  ( b e. ( NN0 ^m ( 1 ... M ) ) -> ( b |` ( 1 ... N ) ) e. ( NN0 ^m ( 1 ... N ) ) )
46 45 ad2antlr 
 |-  ( ( ( N e. NN0 /\ b e. ( NN0 ^m ( 1 ... M ) ) ) /\ ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) ) -> ( b |` ( 1 ... N ) ) e. ( NN0 ^m ( 1 ... N ) ) )
47 44 46 eqeltrd 
 |-  ( ( ( N e. NN0 /\ b e. ( NN0 ^m ( 1 ... M ) ) ) /\ ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) ) -> a e. ( NN0 ^m ( 1 ... N ) ) )
48 simprl 
 |-  ( ( ( N e. NN0 /\ b e. ( NN0 ^m ( 1 ... M ) ) ) /\ ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) ) -> [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps )
49 dfsbcq 
 |-  ( a = ( b |` ( 1 ... N ) ) -> ( [. a / u ]. ps <-> [. ( b |` ( 1 ... N ) ) / u ]. ps ) )
50 49 sbcbidv 
 |-  ( a = ( b |` ( 1 ... N ) ) -> ( [. ( b ` M ) / v ]. [. a / u ]. ps <-> [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps ) )
51 50 ad2antll 
 |-  ( ( ( N e. NN0 /\ b e. ( NN0 ^m ( 1 ... M ) ) ) /\ ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) ) -> ( [. ( b ` M ) / v ]. [. a / u ]. ps <-> [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps ) )
52 48 51 mpbird 
 |-  ( ( ( N e. NN0 /\ b e. ( NN0 ^m ( 1 ... M ) ) ) /\ ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) ) -> [. ( b ` M ) / v ]. [. a / u ]. ps )
53 dfsbcq 
 |-  ( c = ( b ` M ) -> ( [. c / v ]. [. a / u ]. ps <-> [. ( b ` M ) / v ]. [. a / u ]. ps ) )
54 53 anbi2d 
 |-  ( c = ( b ` M ) -> ( ( a e. ( NN0 ^m ( 1 ... N ) ) /\ [. c / v ]. [. a / u ]. ps ) <-> ( a e. ( NN0 ^m ( 1 ... N ) ) /\ [. ( b ` M ) / v ]. [. a / u ]. ps ) ) )
55 54 rspcev 
 |-  ( ( ( b ` M ) e. NN0 /\ ( a e. ( NN0 ^m ( 1 ... N ) ) /\ [. ( b ` M ) / v ]. [. a / u ]. ps ) ) -> E. c e. NN0 ( a e. ( NN0 ^m ( 1 ... N ) ) /\ [. c / v ]. [. a / u ]. ps ) )
56 43 47 52 55 syl12anc 
 |-  ( ( ( N e. NN0 /\ b e. ( NN0 ^m ( 1 ... M ) ) ) /\ ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) ) -> E. c e. NN0 ( a e. ( NN0 ^m ( 1 ... N ) ) /\ [. c / v ]. [. a / u ]. ps ) )
57 56 rexlimdva2 
 |-  ( N e. NN0 -> ( E. b e. ( NN0 ^m ( 1 ... M ) ) ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) -> E. c e. NN0 ( a e. ( NN0 ^m ( 1 ... N ) ) /\ [. c / v ]. [. a / u ]. ps ) ) )
58 35 57 impbid 
 |-  ( N e. NN0 -> ( E. c e. NN0 ( a e. ( NN0 ^m ( 1 ... N ) ) /\ [. c / v ]. [. a / u ]. ps ) <-> E. b e. ( NN0 ^m ( 1 ... M ) ) ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) ) )
59 9 58 syl5bb 
 |-  ( N e. NN0 -> ( ( a e. ( NN0 ^m ( 1 ... N ) ) /\ E. b e. NN0 [. b / v ]. [. a / u ]. ps ) <-> E. b e. ( NN0 ^m ( 1 ... M ) ) ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) ) )
60 59 abbidv 
 |-  ( N e. NN0 -> { a | ( a e. ( NN0 ^m ( 1 ... N ) ) /\ E. b e. NN0 [. b / v ]. [. a / u ]. ps ) } = { a | E. b e. ( NN0 ^m ( 1 ... M ) ) ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) } )
61 4 60 eqtrid 
 |-  ( N e. NN0 -> { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 [. b / v ]. [. a / u ]. ps } = { a | E. b e. ( NN0 ^m ( 1 ... M ) ) ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) } )
62 nfcv 
 |-  F/_ u ( NN0 ^m ( 1 ... N ) )
63 nfcv 
 |-  F/_ a ( NN0 ^m ( 1 ... N ) )
64 nfv 
 |-  F/ a E. v e. NN0 ps
65 nfcv 
 |-  F/_ u NN0
66 nfcv 
 |-  F/_ u b
67 nfsbc1v 
 |-  F/ u [. a / u ]. ps
68 66 67 nfsbcw 
 |-  F/ u [. b / v ]. [. a / u ]. ps
69 65 68 nfrex 
 |-  F/ u E. b e. NN0 [. b / v ]. [. a / u ]. ps
70 sbceq1a 
 |-  ( u = a -> ( ps <-> [. a / u ]. ps ) )
71 70 rexbidv 
 |-  ( u = a -> ( E. v e. NN0 ps <-> E. v e. NN0 [. a / u ]. ps ) )
72 nfv 
 |-  F/ b [. a / u ]. ps
73 nfsbc1v 
 |-  F/ v [. b / v ]. [. a / u ]. ps
74 sbceq1a 
 |-  ( v = b -> ( [. a / u ]. ps <-> [. b / v ]. [. a / u ]. ps ) )
75 72 73 74 cbvrexw 
 |-  ( E. v e. NN0 [. a / u ]. ps <-> E. b e. NN0 [. b / v ]. [. a / u ]. ps )
76 71 75 bitrdi 
 |-  ( u = a -> ( E. v e. NN0 ps <-> E. b e. NN0 [. b / v ]. [. a / u ]. ps ) )
77 62 63 64 69 76 cbvrabw 
 |-  { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 ps } = { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 [. b / v ]. [. a / u ]. ps }
78 fveq1 
 |-  ( t = b -> ( t ` M ) = ( b ` M ) )
79 reseq1 
 |-  ( t = b -> ( t |` ( 1 ... N ) ) = ( b |` ( 1 ... N ) ) )
80 79 sbceq1d 
 |-  ( t = b -> ( [. ( t |` ( 1 ... N ) ) / u ]. ps <-> [. ( b |` ( 1 ... N ) ) / u ]. ps ) )
81 78 80 sbceqbid 
 |-  ( t = b -> ( [. ( t ` M ) / v ]. [. ( t |` ( 1 ... N ) ) / u ]. ps <-> [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps ) )
82 81 rexrab 
 |-  ( E. b e. { t e. ( NN0 ^m ( 1 ... M ) ) | [. ( t ` M ) / v ]. [. ( t |` ( 1 ... N ) ) / u ]. ps } a = ( b |` ( 1 ... N ) ) <-> E. b e. ( NN0 ^m ( 1 ... M ) ) ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) )
83 82 abbii 
 |-  { a | E. b e. { t e. ( NN0 ^m ( 1 ... M ) ) | [. ( t ` M ) / v ]. [. ( t |` ( 1 ... N ) ) / u ]. ps } a = ( b |` ( 1 ... N ) ) } = { a | E. b e. ( NN0 ^m ( 1 ... M ) ) ( [. ( b ` M ) / v ]. [. ( b |` ( 1 ... N ) ) / u ]. ps /\ a = ( b |` ( 1 ... N ) ) ) }
84 61 77 83 3eqtr4g 
 |-  ( N e. NN0 -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 ps } = { a | E. b e. { t e. ( NN0 ^m ( 1 ... M ) ) | [. ( t ` M ) / v ]. [. ( t |` ( 1 ... N ) ) / u ]. ps } a = ( b |` ( 1 ... N ) ) } )
85 fvex 
 |-  ( t ` M ) e. _V
86 vex 
 |-  t e. _V
87 86 resex 
 |-  ( t |` ( 1 ... N ) ) e. _V
88 2 3 sylan9bb 
 |-  ( ( v = ( t ` M ) /\ u = ( t |` ( 1 ... N ) ) ) -> ( ps <-> ph ) )
89 85 87 88 sbc2ie 
 |-  ( [. ( t ` M ) / v ]. [. ( t |` ( 1 ... N ) ) / u ]. ps <-> ph )
90 89 rabbii 
 |-  { t e. ( NN0 ^m ( 1 ... M ) ) | [. ( t ` M ) / v ]. [. ( t |` ( 1 ... N ) ) / u ]. ps } = { t e. ( NN0 ^m ( 1 ... M ) ) | ph }
91 90 rexeqi 
 |-  ( E. b e. { t e. ( NN0 ^m ( 1 ... M ) ) | [. ( t ` M ) / v ]. [. ( t |` ( 1 ... N ) ) / u ]. ps } a = ( b |` ( 1 ... N ) ) <-> E. b e. { t e. ( NN0 ^m ( 1 ... M ) ) | ph } a = ( b |` ( 1 ... N ) ) )
92 91 abbii 
 |-  { a | E. b e. { t e. ( NN0 ^m ( 1 ... M ) ) | [. ( t ` M ) / v ]. [. ( t |` ( 1 ... N ) ) / u ]. ps } a = ( b |` ( 1 ... N ) ) } = { a | E. b e. { t e. ( NN0 ^m ( 1 ... M ) ) | ph } a = ( b |` ( 1 ... N ) ) }
93 84 92 eqtrdi 
 |-  ( N e. NN0 -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 ps } = { a | E. b e. { t e. ( NN0 ^m ( 1 ... M ) ) | ph } a = ( b |` ( 1 ... N ) ) } )
94 93 adantr 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... M ) ) | ph } e. ( Dioph ` M ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 ps } = { a | E. b e. { t e. ( NN0 ^m ( 1 ... M ) ) | ph } a = ( b |` ( 1 ... N ) ) } )
95 simpl 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... M ) ) | ph } e. ( Dioph ` M ) ) -> N e. NN0 )
96 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
97 uzid 
 |-  ( N e. ZZ -> N e. ( ZZ>= ` N ) )
98 peano2uz 
 |-  ( N e. ( ZZ>= ` N ) -> ( N + 1 ) e. ( ZZ>= ` N ) )
99 96 97 98 3syl 
 |-  ( N e. NN0 -> ( N + 1 ) e. ( ZZ>= ` N ) )
100 1 99 eqeltrid 
 |-  ( N e. NN0 -> M e. ( ZZ>= ` N ) )
101 100 adantr 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... M ) ) | ph } e. ( Dioph ` M ) ) -> M e. ( ZZ>= ` N ) )
102 simpr 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... M ) ) | ph } e. ( Dioph ` M ) ) -> { t e. ( NN0 ^m ( 1 ... M ) ) | ph } e. ( Dioph ` M ) )
103 diophrex 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ { t e. ( NN0 ^m ( 1 ... M ) ) | ph } e. ( Dioph ` M ) ) -> { a | E. b e. { t e. ( NN0 ^m ( 1 ... M ) ) | ph } a = ( b |` ( 1 ... N ) ) } e. ( Dioph ` N ) )
104 95 101 102 103 syl3anc 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... M ) ) | ph } e. ( Dioph ` M ) ) -> { a | E. b e. { t e. ( NN0 ^m ( 1 ... M ) ) | ph } a = ( b |` ( 1 ... N ) ) } e. ( Dioph ` N ) )
105 94 104 eqeltrd 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... M ) ) | ph } e. ( Dioph ` M ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 ps } e. ( Dioph ` N ) )