Metamath Proof Explorer

Theorem efgsdm

Description: Elementhood in the domain of S , the set of sequences of extensions starting at an irreducible word. (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 efgsdm 
|- ( F e. dom S <-> ( F e. ( Word W \ { (/) } ) /\ ( F ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )

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 fveq1 
 |-  ( f = F -> ( f ` 0 ) = ( F ` 0 ) )
8 7 eleq1d 
 |-  ( f = F -> ( ( f ` 0 ) e. D <-> ( F ` 0 ) e. D ) )
9 fveq2 
 |-  ( f = F -> ( # ` f ) = ( # ` F ) )
10 9 oveq2d 
 |-  ( f = F -> ( 1 ..^ ( # ` f ) ) = ( 1 ..^ ( # ` F ) ) )
11 fveq1 
 |-  ( f = F -> ( f ` i ) = ( F ` i ) )
12 fveq1 
 |-  ( f = F -> ( f ` ( i - 1 ) ) = ( F ` ( i - 1 ) ) )
13 12 fveq2d 
 |-  ( f = F -> ( T ` ( f ` ( i - 1 ) ) ) = ( T ` ( F ` ( i - 1 ) ) ) )
14 13 rneqd 
 |-  ( f = F -> ran ( T ` ( f ` ( i - 1 ) ) ) = ran ( T ` ( F ` ( i - 1 ) ) ) )
15 11 14 eleq12d 
 |-  ( f = F -> ( ( f ` i ) e. ran ( T ` ( f ` ( i - 1 ) ) ) <-> ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )
16 10 15 raleqbidv 
 |-  ( f = F -> ( A. i e. ( 1 ..^ ( # ` f ) ) ( f ` i ) e. ran ( T ` ( f ` ( i - 1 ) ) ) <-> A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )
17 8 16 anbi12d 
 |-  ( f = F -> ( ( ( f ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` f ) ) ( f ` i ) e. ran ( T ` ( f ` ( i - 1 ) ) ) ) <-> ( ( F ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) ) )
18 1 2 3 4 5 6 efgsf 
 |-  S : { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } --> W
19 18 fdmi 
 |-  dom S = { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) }
20 fveq1 
 |-  ( t = f -> ( t ` 0 ) = ( f ` 0 ) )
21 20 eleq1d 
 |-  ( t = f -> ( ( t ` 0 ) e. D <-> ( f ` 0 ) e. D ) )
22 fveq2 
 |-  ( k = i -> ( t ` k ) = ( t ` i ) )
23 fvoveq1 
 |-  ( k = i -> ( t ` ( k - 1 ) ) = ( t ` ( i - 1 ) ) )
24 23 fveq2d 
 |-  ( k = i -> ( T ` ( t ` ( k - 1 ) ) ) = ( T ` ( t ` ( i - 1 ) ) ) )
25 24 rneqd 
 |-  ( k = i -> ran ( T ` ( t ` ( k - 1 ) ) ) = ran ( T ` ( t ` ( i - 1 ) ) ) )
26 22 25 eleq12d 
 |-  ( k = i -> ( ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) <-> ( t ` i ) e. ran ( T ` ( t ` ( i - 1 ) ) ) ) )
27 26 cbvralvw 
 |-  ( A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) <-> A. i e. ( 1 ..^ ( # ` t ) ) ( t ` i ) e. ran ( T ` ( t ` ( i - 1 ) ) ) )
28 fveq2 
 |-  ( t = f -> ( # ` t ) = ( # ` f ) )
29 28 oveq2d 
 |-  ( t = f -> ( 1 ..^ ( # ` t ) ) = ( 1 ..^ ( # ` f ) ) )
30 fveq1 
 |-  ( t = f -> ( t ` i ) = ( f ` i ) )
31 fveq1 
 |-  ( t = f -> ( t ` ( i - 1 ) ) = ( f ` ( i - 1 ) ) )
32 31 fveq2d 
 |-  ( t = f -> ( T ` ( t ` ( i - 1 ) ) ) = ( T ` ( f ` ( i - 1 ) ) ) )
33 32 rneqd 
 |-  ( t = f -> ran ( T ` ( t ` ( i - 1 ) ) ) = ran ( T ` ( f ` ( i - 1 ) ) ) )
34 30 33 eleq12d 
 |-  ( t = f -> ( ( t ` i ) e. ran ( T ` ( t ` ( i - 1 ) ) ) <-> ( f ` i ) e. ran ( T ` ( f ` ( i - 1 ) ) ) ) )
35 29 34 raleqbidv 
 |-  ( t = f -> ( A. i e. ( 1 ..^ ( # ` t ) ) ( t ` i ) e. ran ( T ` ( t ` ( i - 1 ) ) ) <-> A. i e. ( 1 ..^ ( # ` f ) ) ( f ` i ) e. ran ( T ` ( f ` ( i - 1 ) ) ) ) )
36 27 35 bitrid 
 |-  ( t = f -> ( A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) <-> A. i e. ( 1 ..^ ( # ` f ) ) ( f ` i ) e. ran ( T ` ( f ` ( i - 1 ) ) ) ) )
37 21 36 anbi12d 
 |-  ( t = f -> ( ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) <-> ( ( f ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` f ) ) ( f ` i ) e. ran ( T ` ( f ` ( i - 1 ) ) ) ) ) )
38 37 cbvrabv 
 |-  { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } = { f e. ( Word W \ { (/) } ) | ( ( f ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` f ) ) ( f ` i ) e. ran ( T ` ( f ` ( i - 1 ) ) ) ) }
39 19 38 eqtri 
 |-  dom S = { f e. ( Word W \ { (/) } ) | ( ( f ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` f ) ) ( f ` i ) e. ran ( T ` ( f ` ( i - 1 ) ) ) ) }
40 17 39 elrab2 
 |-  ( F e. dom S <-> ( F e. ( Word W \ { (/) } ) /\ ( ( F ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) ) )
41 3anass 
 |-  ( ( F e. ( Word W \ { (/) } ) /\ ( F ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) <-> ( F e. ( Word W \ { (/) } ) /\ ( ( F ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) ) )
42 40 41 bitr4i 
 |-  ( F e. dom S <-> ( F e. ( Word W \ { (/) } ) /\ ( F ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )