Metamath Proof Explorer

Theorem sseqp1

Description: Value of the strong sequence builder function at a successor. (Contributed by Thierry Arnoux, 24-Apr-2019)

Ref Expression
Hypotheses sseqval.1 
|- ( ph -> S e. _V )
sseqval.2 
|- ( ph -> M e. Word S )
sseqval.3 
|- W = ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )
sseqval.4 
|- ( ph -> F : W --> S )
sseqfv2.4 
|- ( ph -> N e. ( ZZ>= ` ( # ` M ) ) )
Assertion sseqp1 
|- ( ph -> ( ( M seqstr F ) ` N ) = ( F ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) )

Proof

Step Hyp Ref Expression
1 sseqval.1 
 |-  ( ph -> S e. _V )
2 sseqval.2 
 |-  ( ph -> M e. Word S )
3 sseqval.3 
 |-  W = ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )
4 sseqval.4 
 |-  ( ph -> F : W --> S )
5 sseqfv2.4 
 |-  ( ph -> N e. ( ZZ>= ` ( # ` M ) ) )
6 1 2 3 4 5 sseqfv2 
 |-  ( ph -> ( ( M seqstr F ) ` N ) = ( lastS ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` N ) ) )
7 fveq2 
 |-  ( i = ( # ` M ) -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` i ) = ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( # ` M ) ) )
8 oveq2 
 |-  ( i = ( # ` M ) -> ( 0 ..^ i ) = ( 0 ..^ ( # ` M ) ) )
9 8 reseq2d 
 |-  ( i = ( # ` M ) -> ( ( M seqstr F ) |` ( 0 ..^ i ) ) = ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) )
10 9 fveq2d 
 |-  ( i = ( # ` M ) -> ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) = ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) ) )
11 10 s1eqd 
 |-  ( i = ( # ` M ) -> <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) "> = <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) ) "> )
12 9 11 oveq12d 
 |-  ( i = ( # ` M ) -> ( ( ( M seqstr F ) |` ( 0 ..^ i ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) "> ) = ( ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) ) "> ) )
13 7 12 eqeq12d 
 |-  ( i = ( # ` M ) -> ( ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` i ) = ( ( ( M seqstr F ) |` ( 0 ..^ i ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) "> ) <-> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( # ` M ) ) = ( ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) ) "> ) ) )
14 13 imbi2d 
 |-  ( i = ( # ` M ) -> ( ( ph -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` i ) = ( ( ( M seqstr F ) |` ( 0 ..^ i ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) "> ) ) <-> ( ph -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( # ` M ) ) = ( ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) ) "> ) ) ) )
15 fveq2 
 |-  ( i = n -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` i ) = ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) )
16 oveq2 
 |-  ( i = n -> ( 0 ..^ i ) = ( 0 ..^ n ) )
17 16 reseq2d 
 |-  ( i = n -> ( ( M seqstr F ) |` ( 0 ..^ i ) ) = ( ( M seqstr F ) |` ( 0 ..^ n ) ) )
18 17 fveq2d 
 |-  ( i = n -> ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) = ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) )
19 18 s1eqd 
 |-  ( i = n -> <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) "> = <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> )
20 17 19 oveq12d 
 |-  ( i = n -> ( ( ( M seqstr F ) |` ( 0 ..^ i ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) "> ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) )
21 15 20 eqeq12d 
 |-  ( i = n -> ( ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` i ) = ( ( ( M seqstr F ) |` ( 0 ..^ i ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) "> ) <-> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) )
22 21 imbi2d 
 |-  ( i = n -> ( ( ph -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` i ) = ( ( ( M seqstr F ) |` ( 0 ..^ i ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) "> ) ) <-> ( ph -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) ) )
23 fveq2 
 |-  ( i = ( n + 1 ) -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` i ) = ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( n + 1 ) ) )
24 oveq2 
 |-  ( i = ( n + 1 ) -> ( 0 ..^ i ) = ( 0 ..^ ( n + 1 ) ) )
25 24 reseq2d 
 |-  ( i = ( n + 1 ) -> ( ( M seqstr F ) |` ( 0 ..^ i ) ) = ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) )
26 25 fveq2d 
 |-  ( i = ( n + 1 ) -> ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) = ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ) )
27 26 s1eqd 
 |-  ( i = ( n + 1 ) -> <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) "> = <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ) "> )
28 25 27 oveq12d 
 |-  ( i = ( n + 1 ) -> ( ( ( M seqstr F ) |` ( 0 ..^ i ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) "> ) = ( ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ) "> ) )
29 23 28 eqeq12d 
 |-  ( i = ( n + 1 ) -> ( ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` i ) = ( ( ( M seqstr F ) |` ( 0 ..^ i ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) "> ) <-> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( n + 1 ) ) = ( ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ) "> ) ) )
30 29 imbi2d 
 |-  ( i = ( n + 1 ) -> ( ( ph -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` i ) = ( ( ( M seqstr F ) |` ( 0 ..^ i ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) "> ) ) <-> ( ph -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( n + 1 ) ) = ( ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ) "> ) ) ) )
31 fveq2 
 |-  ( i = N -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` i ) = ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` N ) )
32 oveq2 
 |-  ( i = N -> ( 0 ..^ i ) = ( 0 ..^ N ) )
33 32 reseq2d 
 |-  ( i = N -> ( ( M seqstr F ) |` ( 0 ..^ i ) ) = ( ( M seqstr F ) |` ( 0 ..^ N ) ) )
34 33 fveq2d 
 |-  ( i = N -> ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) = ( F ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) )
35 34 s1eqd 
 |-  ( i = N -> <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) "> = <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) "> )
36 33 35 oveq12d 
 |-  ( i = N -> ( ( ( M seqstr F ) |` ( 0 ..^ i ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) "> ) = ( ( ( M seqstr F ) |` ( 0 ..^ N ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) "> ) )
37 31 36 eqeq12d 
 |-  ( i = N -> ( ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` i ) = ( ( ( M seqstr F ) |` ( 0 ..^ i ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) "> ) <-> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` N ) = ( ( ( M seqstr F ) |` ( 0 ..^ N ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) "> ) ) )
38 37 imbi2d 
 |-  ( i = N -> ( ( ph -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` i ) = ( ( ( M seqstr F ) |` ( 0 ..^ i ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ i ) ) ) "> ) ) <-> ( ph -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` N ) = ( ( ( M seqstr F ) |` ( 0 ..^ N ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) "> ) ) ) )
39 ovex 
 |-  ( M ++ <" ( F ` M ) "> ) e. _V
40 lencl 
 |-  ( M e. Word S -> ( # ` M ) e. NN0 )
41 2 40 syl 
 |-  ( ph -> ( # ` M ) e. NN0 )
42 fvconst2g 
 |-  ( ( ( M ++ <" ( F ` M ) "> ) e. _V /\ ( # ` M ) e. NN0 ) -> ( ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ` ( # ` M ) ) = ( M ++ <" ( F ` M ) "> ) )
43 39 41 42 sylancr 
 |-  ( ph -> ( ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ` ( # ` M ) ) = ( M ++ <" ( F ` M ) "> ) )
44 40 nn0zd 
 |-  ( M e. Word S -> ( # ` M ) e. ZZ )
45 seq1 
 |-  ( ( # ` M ) e. ZZ -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( # ` M ) ) = ( ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ` ( # ` M ) ) )
46 2 44 45 3syl 
 |-  ( ph -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( # ` M ) ) = ( ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ` ( # ` M ) ) )
47 1 2 3 4 sseqfres 
 |-  ( ph -> ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) = M )
48 47 fveq2d 
 |-  ( ph -> ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) ) = ( F ` M ) )
49 48 s1eqd 
 |-  ( ph -> <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) ) "> = <" ( F ` M ) "> )
50 47 49 oveq12d 
 |-  ( ph -> ( ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) ) "> ) = ( M ++ <" ( F ` M ) "> ) )
51 43 46 50 3eqtr4d 
 |-  ( ph -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( # ` M ) ) = ( ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) ) "> ) )
52 51 a1i 
 |-  ( ( # ` M ) e. ZZ -> ( ph -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( # ` M ) ) = ( ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) ) "> ) ) )
53 seqp1 
 |-  ( n e. ( ZZ>= ` ( # ` M ) ) -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( n + 1 ) ) = ( ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) ( ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ` ( n + 1 ) ) ) )
54 53 adantl 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( n + 1 ) ) = ( ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) ( ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ` ( n + 1 ) ) ) )
55 id 
 |-  ( x = a -> x = a )
56 fveq2 
 |-  ( x = a -> ( F ` x ) = ( F ` a ) )
57 56 s1eqd 
 |-  ( x = a -> <" ( F ` x ) "> = <" ( F ` a ) "> )
58 55 57 oveq12d 
 |-  ( x = a -> ( x ++ <" ( F ` x ) "> ) = ( a ++ <" ( F ` a ) "> ) )
59 eqidd 
 |-  ( y = b -> ( a ++ <" ( F ` a ) "> ) = ( a ++ <" ( F ` a ) "> ) )
60 58 59 cbvmpov 
 |-  ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) = ( a e. _V , b e. _V |-> ( a ++ <" ( F ` a ) "> ) )
61 60 a1i 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) = ( a e. _V , b e. _V |-> ( a ++ <" ( F ` a ) "> ) ) )
62 simprl 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( a = ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) /\ b = ( ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ` ( n + 1 ) ) ) ) -> a = ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) )
63 62 fveq2d 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( a = ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) /\ b = ( ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ` ( n + 1 ) ) ) ) -> ( F ` a ) = ( F ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ) )
64 63 s1eqd 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( a = ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) /\ b = ( ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ` ( n + 1 ) ) ) ) -> <" ( F ` a ) "> = <" ( F ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ) "> )
65 62 64 oveq12d 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( a = ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) /\ b = ( ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ` ( n + 1 ) ) ) ) -> ( a ++ <" ( F ` a ) "> ) = ( ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ++ <" ( F ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ) "> ) )
66 fvexd 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) e. _V )
67 fvexd 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ` ( n + 1 ) ) e. _V )
68 ovex 
 |-  ( ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ++ <" ( F ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ) "> ) e. _V
69 68 a1i 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ++ <" ( F ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ) "> ) e. _V )
70 61 65 66 67 69 ovmpod 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) ( ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ` ( n + 1 ) ) ) = ( ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ++ <" ( F ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ) "> ) )
71 54 70 eqtrd 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( n + 1 ) ) = ( ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ++ <" ( F ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ) "> ) )
72 71 adantr 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( n + 1 ) ) = ( ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ++ <" ( F ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ) "> ) )
73 1 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> S e. _V )
74 2 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> M e. Word S )
75 4 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> F : W --> S )
76 simpr 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> n e. ( ZZ>= ` ( # ` M ) ) )
77 73 74 3 75 76 sseqfv2 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( ( M seqstr F ) ` n ) = ( lastS ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ) )
78 77 adantr 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) -> ( ( M seqstr F ) ` n ) = ( lastS ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ) )
79 simpr 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) )
80 79 fveq2d 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) -> ( lastS ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ) = ( lastS ` ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) )
81 1 2 3 4 sseqf 
 |-  ( ph -> ( M seqstr F ) : NN0 --> S )
82 fzo0ssnn0 
 |-  ( 0 ..^ n ) C_ NN0
83 fssres 
 |-  ( ( ( M seqstr F ) : NN0 --> S /\ ( 0 ..^ n ) C_ NN0 ) -> ( ( M seqstr F ) |` ( 0 ..^ n ) ) : ( 0 ..^ n ) --> S )
84 81 82 83 sylancl 
 |-  ( ph -> ( ( M seqstr F ) |` ( 0 ..^ n ) ) : ( 0 ..^ n ) --> S )
85 iswrdi 
 |-  ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) : ( 0 ..^ n ) --> S -> ( ( M seqstr F ) |` ( 0 ..^ n ) ) e. Word S )
86 84 85 syl 
 |-  ( ph -> ( ( M seqstr F ) |` ( 0 ..^ n ) ) e. Word S )
87 86 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( ( M seqstr F ) |` ( 0 ..^ n ) ) e. Word S )
88 elex 
 |-  ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) e. Word S -> ( ( M seqstr F ) |` ( 0 ..^ n ) ) e. _V )
89 87 88 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( ( M seqstr F ) |` ( 0 ..^ n ) ) e. _V )
90 81 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( M seqstr F ) : NN0 --> S )
91 eluznn0 
 |-  ( ( ( # ` M ) e. NN0 /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> n e. NN0 )
92 41 91 sylan 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> n e. NN0 )
93 73 90 92 subiwrdlen 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( # ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) = n )
94 93 76 eqeltrd 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( # ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) e. ( ZZ>= ` ( # ` M ) ) )
95 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
96 ffn 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> # Fn _V )
97 elpreima 
 |-  ( # Fn _V -> ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) <-> ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) e. _V /\ ( # ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) e. ( ZZ>= ` ( # ` M ) ) ) ) )
98 95 96 97 mp2b 
 |-  ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) <-> ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) e. _V /\ ( # ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) e. ( ZZ>= ` ( # ` M ) ) ) )
99 89 94 98 sylanbrc 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( ( M seqstr F ) |` ( 0 ..^ n ) ) e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) )
100 87 99 elind 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( ( M seqstr F ) |` ( 0 ..^ n ) ) e. ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) ) )
101 100 3 eleqtrrdi 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( ( M seqstr F ) |` ( 0 ..^ n ) ) e. W )
102 75 101 ffvelcdmd 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) e. S )
103 lswccats1 
 |-  ( ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) e. Word S /\ ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) e. S ) -> ( lastS ` ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) = ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) )
104 87 102 103 syl2anc 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( lastS ` ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) = ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) )
105 104 adantr 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) -> ( lastS ` ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) = ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) )
106 78 80 105 3eqtrrd 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) -> ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) = ( ( M seqstr F ) ` n ) )
107 106 s1eqd 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) -> <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> = <" ( ( M seqstr F ) ` n ) "> )
108 107 oveq2d 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) -> ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( ( M seqstr F ) ` n ) "> ) )
109 73 90 92 iwrdsplit 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( ( M seqstr F ) ` n ) "> ) )
110 109 adantr 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) -> ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( ( M seqstr F ) ` n ) "> ) )
111 108 79 110 3eqtr4d 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) )
112 111 fveq2d 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) -> ( F ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ) = ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ) )
113 112 s1eqd 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) -> <" ( F ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ) "> = <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ) "> )
114 111 113 oveq12d 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) -> ( ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ++ <" ( F ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) ) "> ) = ( ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ) "> ) )
115 72 114 eqtrd 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) /\ ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( n + 1 ) ) = ( ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ) "> ) )
116 115 ex 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( # ` M ) ) ) -> ( ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( n + 1 ) ) = ( ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ) "> ) ) )
117 116 expcom 
 |-  ( n e. ( ZZ>= ` ( # ` M ) ) -> ( ph -> ( ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( n + 1 ) ) = ( ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ) "> ) ) ) )
118 117 a2d 
 |-  ( n e. ( ZZ>= ` ( # ` M ) ) -> ( ( ph -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` n ) = ( ( ( M seqstr F ) |` ( 0 ..^ n ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ n ) ) ) "> ) ) -> ( ph -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` ( n + 1 ) ) = ( ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ ( n + 1 ) ) ) ) "> ) ) ) )
119 14 22 30 38 52 118 uzind4 
 |-  ( N e. ( ZZ>= ` ( # ` M ) ) -> ( ph -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` N ) = ( ( ( M seqstr F ) |` ( 0 ..^ N ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) "> ) ) )
120 5 119 mpcom 
 |-  ( ph -> ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` N ) = ( ( ( M seqstr F ) |` ( 0 ..^ N ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) "> ) )
121 120 fveq2d 
 |-  ( ph -> ( lastS ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` N ) ) = ( lastS ` ( ( ( M seqstr F ) |` ( 0 ..^ N ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) "> ) ) )
122 fzo0ssnn0 
 |-  ( 0 ..^ N ) C_ NN0
123 fssres 
 |-  ( ( ( M seqstr F ) : NN0 --> S /\ ( 0 ..^ N ) C_ NN0 ) -> ( ( M seqstr F ) |` ( 0 ..^ N ) ) : ( 0 ..^ N ) --> S )
124 81 122 123 sylancl 
 |-  ( ph -> ( ( M seqstr F ) |` ( 0 ..^ N ) ) : ( 0 ..^ N ) --> S )
125 iswrdi 
 |-  ( ( ( M seqstr F ) |` ( 0 ..^ N ) ) : ( 0 ..^ N ) --> S -> ( ( M seqstr F ) |` ( 0 ..^ N ) ) e. Word S )
126 124 125 syl 
 |-  ( ph -> ( ( M seqstr F ) |` ( 0 ..^ N ) ) e. Word S )
127 elex 
 |-  ( ( ( M seqstr F ) |` ( 0 ..^ N ) ) e. Word S -> ( ( M seqstr F ) |` ( 0 ..^ N ) ) e. _V )
128 126 127 syl 
 |-  ( ph -> ( ( M seqstr F ) |` ( 0 ..^ N ) ) e. _V )
129 eluznn0 
 |-  ( ( ( # ` M ) e. NN0 /\ N e. ( ZZ>= ` ( # ` M ) ) ) -> N e. NN0 )
130 41 5 129 syl2anc 
 |-  ( ph -> N e. NN0 )
131 1 81 130 subiwrdlen 
 |-  ( ph -> ( # ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) = N )
132 131 5 eqeltrd 
 |-  ( ph -> ( # ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) e. ( ZZ>= ` ( # ` M ) ) )
133 elpreima 
 |-  ( # Fn _V -> ( ( ( M seqstr F ) |` ( 0 ..^ N ) ) e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) <-> ( ( ( M seqstr F ) |` ( 0 ..^ N ) ) e. _V /\ ( # ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) e. ( ZZ>= ` ( # ` M ) ) ) ) )
134 95 96 133 mp2b 
 |-  ( ( ( M seqstr F ) |` ( 0 ..^ N ) ) e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) <-> ( ( ( M seqstr F ) |` ( 0 ..^ N ) ) e. _V /\ ( # ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) e. ( ZZ>= ` ( # ` M ) ) ) )
135 128 132 134 sylanbrc 
 |-  ( ph -> ( ( M seqstr F ) |` ( 0 ..^ N ) ) e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) )
136 126 135 elind 
 |-  ( ph -> ( ( M seqstr F ) |` ( 0 ..^ N ) ) e. ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) ) )
137 136 3 eleqtrrdi 
 |-  ( ph -> ( ( M seqstr F ) |` ( 0 ..^ N ) ) e. W )
138 4 137 ffvelcdmd 
 |-  ( ph -> ( F ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) e. S )
139 lswccats1 
 |-  ( ( ( ( M seqstr F ) |` ( 0 ..^ N ) ) e. Word S /\ ( F ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) e. S ) -> ( lastS ` ( ( ( M seqstr F ) |` ( 0 ..^ N ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) "> ) ) = ( F ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) )
140 126 138 139 syl2anc 
 |-  ( ph -> ( lastS ` ( ( ( M seqstr F ) |` ( 0 ..^ N ) ) ++ <" ( F ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) "> ) ) = ( F ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) )
141 6 121 140 3eqtrd 
 |-  ( ph -> ( ( M seqstr F ) ` N ) = ( F ` ( ( M seqstr F ) |` ( 0 ..^ N ) ) ) )