Metamath Proof Explorer

Theorem efgs1

Description: A singleton of an irreducible word is an extension sequence. (Contributed by Mario Carneiro, 27-Sep-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 efgs1 
|- ( A e. D -> <" A "> e. dom S )

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 eldifi 
 |-  ( A e. ( W \ U_ x e. W ran ( T ` x ) ) -> A e. W )
8 7 5 eleq2s 
 |-  ( A e. D -> A e. W )
9 8 s1cld 
 |-  ( A e. D -> <" A "> e. Word W )
10 s1nz 
 |-  <" A "> =/= (/)
11 eldifsn 
 |-  ( <" A "> e. ( Word W \ { (/) } ) <-> ( <" A "> e. Word W /\ <" A "> =/= (/) ) )
12 9 10 11 sylanblrc 
 |-  ( A e. D -> <" A "> e. ( Word W \ { (/) } ) )
13 s1fv 
 |-  ( A e. D -> ( <" A "> ` 0 ) = A )
14 id 
 |-  ( A e. D -> A e. D )
15 13 14 eqeltrd 
 |-  ( A e. D -> ( <" A "> ` 0 ) e. D )
16 s1len 
 |-  ( # ` <" A "> ) = 1
17 16 a1i 
 |-  ( A e. D -> ( # ` <" A "> ) = 1 )
18 17 oveq2d 
 |-  ( A e. D -> ( 1 ..^ ( # ` <" A "> ) ) = ( 1 ..^ 1 ) )
19 fzo0 
 |-  ( 1 ..^ 1 ) = (/)
20 18 19 eqtrdi 
 |-  ( A e. D -> ( 1 ..^ ( # ` <" A "> ) ) = (/) )
21 rzal 
 |-  ( ( 1 ..^ ( # ` <" A "> ) ) = (/) -> A. i e. ( 1 ..^ ( # ` <" A "> ) ) ( <" A "> ` i ) e. ran ( T ` ( <" A "> ` ( i - 1 ) ) ) )
22 20 21 syl 
 |-  ( A e. D -> A. i e. ( 1 ..^ ( # ` <" A "> ) ) ( <" A "> ` i ) e. ran ( T ` ( <" A "> ` ( i - 1 ) ) ) )
23 1 2 3 4 5 6 efgsdm 
 |-  ( <" A "> e. dom S <-> ( <" A "> e. ( Word W \ { (/) } ) /\ ( <" A "> ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` <" A "> ) ) ( <" A "> ` i ) e. ran ( T ` ( <" A "> ` ( i - 1 ) ) ) ) )
24 12 15 22 23 syl3anbrc 
 |-  ( A e. D -> <" A "> e. dom S )