Step |
Hyp |
Ref |
Expression |
1 |
|
wlkd.p |
|- ( ph -> P e. Word _V ) |
2 |
|
wlkd.f |
|- ( ph -> F e. Word _V ) |
3 |
|
wlkd.l |
|- ( ph -> ( # ` P ) = ( ( # ` F ) + 1 ) ) |
4 |
|
wlkdlem1.v |
|- ( ph -> A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V ) |
5 |
|
wrdf |
|- ( P e. Word _V -> P : ( 0 ..^ ( # ` P ) ) --> _V ) |
6 |
1 5
|
syl |
|- ( ph -> P : ( 0 ..^ ( # ` P ) ) --> _V ) |
7 |
3
|
oveq2d |
|- ( ph -> ( 0 ..^ ( # ` P ) ) = ( 0 ..^ ( ( # ` F ) + 1 ) ) ) |
8 |
|
lencl |
|- ( F e. Word _V -> ( # ` F ) e. NN0 ) |
9 |
2 8
|
syl |
|- ( ph -> ( # ` F ) e. NN0 ) |
10 |
9
|
nn0zd |
|- ( ph -> ( # ` F ) e. ZZ ) |
11 |
|
fzval3 |
|- ( ( # ` F ) e. ZZ -> ( 0 ... ( # ` F ) ) = ( 0 ..^ ( ( # ` F ) + 1 ) ) ) |
12 |
10 11
|
syl |
|- ( ph -> ( 0 ... ( # ` F ) ) = ( 0 ..^ ( ( # ` F ) + 1 ) ) ) |
13 |
7 12
|
eqtr4d |
|- ( ph -> ( 0 ..^ ( # ` P ) ) = ( 0 ... ( # ` F ) ) ) |
14 |
13
|
feq2d |
|- ( ph -> ( P : ( 0 ..^ ( # ` P ) ) --> _V <-> P : ( 0 ... ( # ` F ) ) --> _V ) ) |
15 |
|
ssv |
|- V C_ _V |
16 |
|
frnssb |
|- ( ( V C_ _V /\ A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V ) -> ( P : ( 0 ... ( # ` F ) ) --> _V <-> P : ( 0 ... ( # ` F ) ) --> V ) ) |
17 |
15 4 16
|
sylancr |
|- ( ph -> ( P : ( 0 ... ( # ` F ) ) --> _V <-> P : ( 0 ... ( # ` F ) ) --> V ) ) |
18 |
14 17
|
bitrd |
|- ( ph -> ( P : ( 0 ..^ ( # ` P ) ) --> _V <-> P : ( 0 ... ( # ` F ) ) --> V ) ) |
19 |
6 18
|
mpbid |
|- ( ph -> P : ( 0 ... ( # ` F ) ) --> V ) |