Metamath Proof Explorer

Theorem sseqf

Description: A strong recursive sequence is a function over the nonnegative integers. (Contributed by Thierry Arnoux, 23-Apr-2019) (Proof shortened by AV, 7-Mar-2022)

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 )
Assertion sseqf 
|- ( ph -> ( M seqstr F ) : NN0 --> S )

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 wrdf 
 |-  ( M e. Word S -> M : ( 0 ..^ ( # ` M ) ) --> S )
6 2 5 syl 
 |-  ( ph -> M : ( 0 ..^ ( # ` M ) ) --> S )
7 vex 
 |-  w e. _V
8 7 a1i 
 |-  ( ( ph /\ w e. ( W \ { (/) } ) ) -> w e. _V )
9 fvex 
 |-  ( x ` ( ( # ` x ) - 1 ) ) e. _V
10 df-lsw 
 |-  lastS = ( x e. _V |-> ( x ` ( ( # ` x ) - 1 ) ) )
11 9 10 dmmpti 
 |-  dom lastS = _V
12 8 11 eleqtrrdi 
 |-  ( ( ph /\ w e. ( W \ { (/) } ) ) -> w e. dom lastS )
13 eldifsn 
 |-  ( w e. ( W \ { (/) } ) <-> ( w e. W /\ w =/= (/) ) )
14 inss1 
 |-  ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) ) C_ Word S
15 3 14 eqsstri 
 |-  W C_ Word S
16 15 sseli 
 |-  ( w e. W -> w e. Word S )
17 lswcl 
 |-  ( ( w e. Word S /\ w =/= (/) ) -> ( lastS ` w ) e. S )
18 16 17 sylan 
 |-  ( ( w e. W /\ w =/= (/) ) -> ( lastS ` w ) e. S )
19 13 18 sylbi 
 |-  ( w e. ( W \ { (/) } ) -> ( lastS ` w ) e. S )
20 19 adantl 
 |-  ( ( ph /\ w e. ( W \ { (/) } ) ) -> ( lastS ` w ) e. S )
21 12 20 jca 
 |-  ( ( ph /\ w e. ( W \ { (/) } ) ) -> ( w e. dom lastS /\ ( lastS ` w ) e. S ) )
22 21 ralrimiva 
 |-  ( ph -> A. w e. ( W \ { (/) } ) ( w e. dom lastS /\ ( lastS ` w ) e. S ) )
23 9 10 fnmpti 
 |-  lastS Fn _V
24 fnfun 
 |-  ( lastS Fn _V -> Fun lastS )
25 ffvresb 
 |-  ( Fun lastS -> ( ( lastS |` ( W \ { (/) } ) ) : ( W \ { (/) } ) --> S <-> A. w e. ( W \ { (/) } ) ( w e. dom lastS /\ ( lastS ` w ) e. S ) ) )
26 23 24 25 mp2b 
 |-  ( ( lastS |` ( W \ { (/) } ) ) : ( W \ { (/) } ) --> S <-> A. w e. ( W \ { (/) } ) ( w e. dom lastS /\ ( lastS ` w ) e. S ) )
27 22 26 sylibr 
 |-  ( ph -> ( lastS |` ( W \ { (/) } ) ) : ( W \ { (/) } ) --> S )
28 eqid 
 |-  ( ZZ>= ` ( # ` M ) ) = ( ZZ>= ` ( # ` M ) )
29 lencl 
 |-  ( M e. Word S -> ( # ` M ) e. NN0 )
30 29 nn0zd 
 |-  ( M e. Word S -> ( # ` M ) e. ZZ )
31 2 30 syl 
 |-  ( ph -> ( # ` M ) e. ZZ )
32 ovex 
 |-  ( M ++ <" ( F ` M ) "> ) e. _V
33 simpr 
 |-  ( ( ph /\ a e. ( ZZ>= ` ( # ` M ) ) ) -> a e. ( ZZ>= ` ( # ` M ) ) )
34 2 29 syl 
 |-  ( ph -> ( # ` M ) e. NN0 )
35 34 adantr 
 |-  ( ( ph /\ a e. ( ZZ>= ` ( # ` M ) ) ) -> ( # ` M ) e. NN0 )
36 elnn0uz 
 |-  ( ( # ` M ) e. NN0 <-> ( # ` M ) e. ( ZZ>= ` 0 ) )
37 35 36 sylib 
 |-  ( ( ph /\ a e. ( ZZ>= ` ( # ` M ) ) ) -> ( # ` M ) e. ( ZZ>= ` 0 ) )
38 uztrn 
 |-  ( ( a e. ( ZZ>= ` ( # ` M ) ) /\ ( # ` M ) e. ( ZZ>= ` 0 ) ) -> a e. ( ZZ>= ` 0 ) )
39 33 37 38 syl2anc 
 |-  ( ( ph /\ a e. ( ZZ>= ` ( # ` M ) ) ) -> a e. ( ZZ>= ` 0 ) )
40 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
41 39 40 eleqtrrdi 
 |-  ( ( ph /\ a e. ( ZZ>= ` ( # ` M ) ) ) -> a e. NN0 )
42 fvconst2g 
 |-  ( ( ( M ++ <" ( F ` M ) "> ) e. _V /\ a e. NN0 ) -> ( ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ` a ) = ( M ++ <" ( F ` M ) "> ) )
43 32 41 42 sylancr 
 |-  ( ( ph /\ a e. ( ZZ>= ` ( # ` M ) ) ) -> ( ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ` a ) = ( M ++ <" ( F ` M ) "> ) )
44 1 2 3 4 sseqmw 
 |-  ( ph -> M e. W )
45 4 44 ffvelrnd 
 |-  ( ph -> ( F ` M ) e. S )
46 45 s1cld 
 |-  ( ph -> <" ( F ` M ) "> e. Word S )
47 ccatcl 
 |-  ( ( M e. Word S /\ <" ( F ` M ) "> e. Word S ) -> ( M ++ <" ( F ` M ) "> ) e. Word S )
48 2 46 47 syl2anc 
 |-  ( ph -> ( M ++ <" ( F ` M ) "> ) e. Word S )
49 32 a1i 
 |-  ( ph -> ( M ++ <" ( F ` M ) "> ) e. _V )
50 ccatws1len 
 |-  ( M e. Word S -> ( # ` ( M ++ <" ( F ` M ) "> ) ) = ( ( # ` M ) + 1 ) )
51 2 50 syl 
 |-  ( ph -> ( # ` ( M ++ <" ( F ` M ) "> ) ) = ( ( # ` M ) + 1 ) )
52 uzid 
 |-  ( ( # ` M ) e. ZZ -> ( # ` M ) e. ( ZZ>= ` ( # ` M ) ) )
53 peano2uz 
 |-  ( ( # ` M ) e. ( ZZ>= ` ( # ` M ) ) -> ( ( # ` M ) + 1 ) e. ( ZZ>= ` ( # ` M ) ) )
54 31 52 53 3syl 
 |-  ( ph -> ( ( # ` M ) + 1 ) e. ( ZZ>= ` ( # ` M ) ) )
55 51 54 eqeltrd 
 |-  ( ph -> ( # ` ( M ++ <" ( F ` M ) "> ) ) e. ( ZZ>= ` ( # ` M ) ) )
56 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
57 ffn 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> # Fn _V )
58 elpreima 
 |-  ( # Fn _V -> ( ( M ++ <" ( F ` M ) "> ) e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) <-> ( ( M ++ <" ( F ` M ) "> ) e. _V /\ ( # ` ( M ++ <" ( F ` M ) "> ) ) e. ( ZZ>= ` ( # ` M ) ) ) ) )
59 56 57 58 mp2b 
 |-  ( ( M ++ <" ( F ` M ) "> ) e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) <-> ( ( M ++ <" ( F ` M ) "> ) e. _V /\ ( # ` ( M ++ <" ( F ` M ) "> ) ) e. ( ZZ>= ` ( # ` M ) ) ) )
60 49 55 59 sylanbrc 
 |-  ( ph -> ( M ++ <" ( F ` M ) "> ) e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) )
61 48 60 elind 
 |-  ( ph -> ( M ++ <" ( F ` M ) "> ) e. ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) ) )
62 61 3 eleqtrrdi 
 |-  ( ph -> ( M ++ <" ( F ` M ) "> ) e. W )
63 62 adantr 
 |-  ( ( ph /\ a e. ( ZZ>= ` ( # ` M ) ) ) -> ( M ++ <" ( F ` M ) "> ) e. W )
64 ccatws1n0 
 |-  ( M e. Word S -> ( M ++ <" ( F ` M ) "> ) =/= (/) )
65 2 64 syl 
 |-  ( ph -> ( M ++ <" ( F ` M ) "> ) =/= (/) )
66 65 adantr 
 |-  ( ( ph /\ a e. ( ZZ>= ` ( # ` M ) ) ) -> ( M ++ <" ( F ` M ) "> ) =/= (/) )
67 eldifsn 
 |-  ( ( M ++ <" ( F ` M ) "> ) e. ( W \ { (/) } ) <-> ( ( M ++ <" ( F ` M ) "> ) e. W /\ ( M ++ <" ( F ` M ) "> ) =/= (/) ) )
68 63 66 67 sylanbrc 
 |-  ( ( ph /\ a e. ( ZZ>= ` ( # ` M ) ) ) -> ( M ++ <" ( F ` M ) "> ) e. ( W \ { (/) } ) )
69 43 68 eqeltrd 
 |-  ( ( ph /\ a e. ( ZZ>= ` ( # ` M ) ) ) -> ( ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ` a ) e. ( W \ { (/) } ) )
70 eqidd 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) = ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) )
71 simprl 
 |-  ( ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) /\ ( x = a /\ y = b ) ) -> x = a )
72 71 fveq2d 
 |-  ( ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) /\ ( x = a /\ y = b ) ) -> ( F ` x ) = ( F ` a ) )
73 72 s1eqd 
 |-  ( ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) /\ ( x = a /\ y = b ) ) -> <" ( F ` x ) "> = <" ( F ` a ) "> )
74 71 73 oveq12d 
 |-  ( ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) /\ ( x = a /\ y = b ) ) -> ( x ++ <" ( F ` x ) "> ) = ( a ++ <" ( F ` a ) "> ) )
75 vex 
 |-  a e. _V
76 75 a1i 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> a e. _V )
77 vex 
 |-  b e. _V
78 77 a1i 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> b e. _V )
79 ovex 
 |-  ( a ++ <" ( F ` a ) "> ) e. _V
80 79 a1i 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> ( a ++ <" ( F ` a ) "> ) e. _V )
81 70 74 76 78 80 ovmpod 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> ( a ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) b ) = ( a ++ <" ( F ` a ) "> ) )
82 eldifi 
 |-  ( a e. ( W \ { (/) } ) -> a e. W )
83 82 ad2antrl 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> a e. W )
84 15 83 sselid 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> a e. Word S )
85 4 adantr 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> F : W --> S )
86 85 83 ffvelrnd 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> ( F ` a ) e. S )
87 86 s1cld 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> <" ( F ` a ) "> e. Word S )
88 ccatcl 
 |-  ( ( a e. Word S /\ <" ( F ` a ) "> e. Word S ) -> ( a ++ <" ( F ` a ) "> ) e. Word S )
89 84 87 88 syl2anc 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> ( a ++ <" ( F ` a ) "> ) e. Word S )
90 15 82 sselid 
 |-  ( a e. ( W \ { (/) } ) -> a e. Word S )
91 90 ad2antrl 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> a e. Word S )
92 ccatws1len 
 |-  ( a e. Word S -> ( # ` ( a ++ <" ( F ` a ) "> ) ) = ( ( # ` a ) + 1 ) )
93 91 92 syl 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> ( # ` ( a ++ <" ( F ` a ) "> ) ) = ( ( # ` a ) + 1 ) )
94 83 3 eleqtrdi 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> a e. ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) ) )
95 94 elin2d 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> a e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) )
96 elpreima 
 |-  ( # Fn _V -> ( a e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) <-> ( a e. _V /\ ( # ` a ) e. ( ZZ>= ` ( # ` M ) ) ) ) )
97 56 57 96 mp2b 
 |-  ( a e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) <-> ( a e. _V /\ ( # ` a ) e. ( ZZ>= ` ( # ` M ) ) ) )
98 95 97 sylib 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> ( a e. _V /\ ( # ` a ) e. ( ZZ>= ` ( # ` M ) ) ) )
99 peano2uz 
 |-  ( ( # ` a ) e. ( ZZ>= ` ( # ` M ) ) -> ( ( # ` a ) + 1 ) e. ( ZZ>= ` ( # ` M ) ) )
100 98 99 simpl2im 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> ( ( # ` a ) + 1 ) e. ( ZZ>= ` ( # ` M ) ) )
101 93 100 eqeltrd 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> ( # ` ( a ++ <" ( F ` a ) "> ) ) e. ( ZZ>= ` ( # ` M ) ) )
102 elpreima 
 |-  ( # Fn _V -> ( ( a ++ <" ( F ` a ) "> ) e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) <-> ( ( a ++ <" ( F ` a ) "> ) e. _V /\ ( # ` ( a ++ <" ( F ` a ) "> ) ) e. ( ZZ>= ` ( # ` M ) ) ) ) )
103 56 57 102 mp2b 
 |-  ( ( a ++ <" ( F ` a ) "> ) e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) <-> ( ( a ++ <" ( F ` a ) "> ) e. _V /\ ( # ` ( a ++ <" ( F ` a ) "> ) ) e. ( ZZ>= ` ( # ` M ) ) ) )
104 80 101 103 sylanbrc 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> ( a ++ <" ( F ` a ) "> ) e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) )
105 89 104 elind 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> ( a ++ <" ( F ` a ) "> ) e. ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) ) )
106 105 3 eleqtrrdi 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> ( a ++ <" ( F ` a ) "> ) e. W )
107 ccatws1n0 
 |-  ( a e. Word S -> ( a ++ <" ( F ` a ) "> ) =/= (/) )
108 91 107 syl 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> ( a ++ <" ( F ` a ) "> ) =/= (/) )
109 eldifsn 
 |-  ( ( a ++ <" ( F ` a ) "> ) e. ( W \ { (/) } ) <-> ( ( a ++ <" ( F ` a ) "> ) e. W /\ ( a ++ <" ( F ` a ) "> ) =/= (/) ) )
110 106 108 109 sylanbrc 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> ( a ++ <" ( F ` a ) "> ) e. ( W \ { (/) } ) )
111 81 110 eqeltrd 
 |-  ( ( ph /\ ( a e. ( W \ { (/) } ) /\ b e. ( W \ { (/) } ) ) ) -> ( a ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) b ) e. ( W \ { (/) } ) )
112 28 31 69 111 seqf 
 |-  ( ph -> seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) : ( ZZ>= ` ( # ` M ) ) --> ( W \ { (/) } ) )
113 fco2 
 |-  ( ( ( lastS |` ( W \ { (/) } ) ) : ( W \ { (/) } ) --> S /\ seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) : ( ZZ>= ` ( # ` M ) ) --> ( W \ { (/) } ) ) -> ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) : ( ZZ>= ` ( # ` M ) ) --> S )
114 27 112 113 syl2anc 
 |-  ( ph -> ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) : ( ZZ>= ` ( # ` M ) ) --> S )
115 fzouzdisj 
 |-  ( ( 0 ..^ ( # ` M ) ) i^i ( ZZ>= ` ( # ` M ) ) ) = (/)
116 115 a1i 
 |-  ( ph -> ( ( 0 ..^ ( # ` M ) ) i^i ( ZZ>= ` ( # ` M ) ) ) = (/) )
117 fun 
 |-  ( ( ( M : ( 0 ..^ ( # ` M ) ) --> S /\ ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) : ( ZZ>= ` ( # ` M ) ) --> S ) /\ ( ( 0 ..^ ( # ` M ) ) i^i ( ZZ>= ` ( # ` M ) ) ) = (/) ) -> ( M u. ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ) : ( ( 0 ..^ ( # ` M ) ) u. ( ZZ>= ` ( # ` M ) ) ) --> ( S u. S ) )
118 6 114 116 117 syl21anc 
 |-  ( ph -> ( M u. ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ) : ( ( 0 ..^ ( # ` M ) ) u. ( ZZ>= ` ( # ` M ) ) ) --> ( S u. S ) )
119 1 2 3 4 sseqval 
 |-  ( ph -> ( M seqstr F ) = ( M u. ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ) )
120 fzouzsplit 
 |-  ( ( # ` M ) e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 0 ) = ( ( 0 ..^ ( # ` M ) ) u. ( ZZ>= ` ( # ` M ) ) ) )
121 36 120 sylbi 
 |-  ( ( # ` M ) e. NN0 -> ( ZZ>= ` 0 ) = ( ( 0 ..^ ( # ` M ) ) u. ( ZZ>= ` ( # ` M ) ) ) )
122 2 29 121 3syl 
 |-  ( ph -> ( ZZ>= ` 0 ) = ( ( 0 ..^ ( # ` M ) ) u. ( ZZ>= ` ( # ` M ) ) ) )
123 40 122 syl5eq 
 |-  ( ph -> NN0 = ( ( 0 ..^ ( # ` M ) ) u. ( ZZ>= ` ( # ` M ) ) ) )
124 unidm 
 |-  ( S u. S ) = S
125 124 a1i 
 |-  ( ph -> ( S u. S ) = S )
126 125 eqcomd 
 |-  ( ph -> S = ( S u. S ) )
127 119 123 126 feq123d 
 |-  ( ph -> ( ( M seqstr F ) : NN0 --> S <-> ( M u. ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ) : ( ( 0 ..^ ( # ` M ) ) u. ( ZZ>= ` ( # ` M ) ) ) --> ( S u. S ) ) )
128 118 127 mpbird 
 |-  ( ph -> ( M seqstr F ) : NN0 --> S )