Metamath Proof Explorer

Theorem efgsf

Description: Value of the auxiliary function S defining a sequence of extensions starting at some irreducible word. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypotheses efgval.w 
|- W = ( _I ` Word ( I X. 2o ) )
efgval.r 
|- .~ = ( ~FG ` I )
efgval2.m 
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
efgval2.t 
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
efgred.d 
|- D = ( W \ U_ x e. W ran ( T ` x ) )
efgred.s 
|- S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )
Assertion efgsf 
|- S : { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } --> W

Proof

Step Hyp Ref Expression
1 efgval.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
2 efgval.r 
 |-  .~ = ( ~FG ` I )
3 efgval2.m 
 |-  M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
4 efgval2.t 
 |-  T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
5 efgred.d 
 |-  D = ( W \ U_ x e. W ran ( T ` x ) )
6 efgred.s 
 |-  S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )
7 id 
 |-  ( m = t -> m = t )
8 fveq2 
 |-  ( m = t -> ( # ` m ) = ( # ` t ) )
9 8 oveq1d 
 |-  ( m = t -> ( ( # ` m ) - 1 ) = ( ( # ` t ) - 1 ) )
10 7 9 fveq12d 
 |-  ( m = t -> ( m ` ( ( # ` m ) - 1 ) ) = ( t ` ( ( # ` t ) - 1 ) ) )
11 10 eleq1d 
 |-  ( m = t -> ( ( m ` ( ( # ` m ) - 1 ) ) e. W <-> ( t ` ( ( # ` t ) - 1 ) ) e. W ) )
12 11 ralrab2 
 |-  ( A. m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } ( m ` ( ( # ` m ) - 1 ) ) e. W <-> A. t e. ( Word W \ { (/) } ) ( ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) -> ( t ` ( ( # ` t ) - 1 ) ) e. W ) )
13 eldifi 
 |-  ( t e. ( Word W \ { (/) } ) -> t e. Word W )
14 wrdf 
 |-  ( t e. Word W -> t : ( 0 ..^ ( # ` t ) ) --> W )
15 13 14 syl 
 |-  ( t e. ( Word W \ { (/) } ) -> t : ( 0 ..^ ( # ` t ) ) --> W )
16 eldifsn 
 |-  ( t e. ( Word W \ { (/) } ) <-> ( t e. Word W /\ t =/= (/) ) )
17 lennncl 
 |-  ( ( t e. Word W /\ t =/= (/) ) -> ( # ` t ) e. NN )
18 16 17 sylbi 
 |-  ( t e. ( Word W \ { (/) } ) -> ( # ` t ) e. NN )
19 fzo0end 
 |-  ( ( # ` t ) e. NN -> ( ( # ` t ) - 1 ) e. ( 0 ..^ ( # ` t ) ) )
20 18 19 syl 
 |-  ( t e. ( Word W \ { (/) } ) -> ( ( # ` t ) - 1 ) e. ( 0 ..^ ( # ` t ) ) )
21 15 20 ffvelrnd 
 |-  ( t e. ( Word W \ { (/) } ) -> ( t ` ( ( # ` t ) - 1 ) ) e. W )
22 21 a1d 
 |-  ( t e. ( Word W \ { (/) } ) -> ( ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) -> ( t ` ( ( # ` t ) - 1 ) ) e. W ) )
23 12 22 mprgbir 
 |-  A. m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } ( m ` ( ( # ` m ) - 1 ) ) e. W
24 6 fmpt 
 |-  ( A. m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } ( m ` ( ( # ` m ) - 1 ) ) e. W <-> S : { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } --> W )
25 23 24 mpbi 
 |-  S : { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } --> W