Step |
Hyp |
Ref |
Expression |
1 |
|
wrdfn |
|- ( W e. Word _V -> W Fn ( 0 ..^ ( # ` W ) ) ) |
2 |
1
|
anim1i |
|- ( ( W e. Word _V /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) e. V ) -> ( W Fn ( 0 ..^ ( # ` W ) ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) e. V ) ) |
3 |
|
ffnfv |
|- ( W : ( 0 ..^ ( # ` W ) ) --> V <-> ( W Fn ( 0 ..^ ( # ` W ) ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) e. V ) ) |
4 |
2 3
|
sylibr |
|- ( ( W e. Word _V /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) e. V ) -> W : ( 0 ..^ ( # ` W ) ) --> V ) |
5 |
|
iswrdi |
|- ( W : ( 0 ..^ ( # ` W ) ) --> V -> W e. Word V ) |
6 |
4 5
|
syl |
|- ( ( W e. Word _V /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) e. V ) -> W e. Word V ) |