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
|
syl5bb |
|- ( 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 ) ) ) ) ) |