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