| Step |
Hyp |
Ref |
Expression |
| 1 |
|
1wlkd.p |
|- P = <" X Y "> |
| 2 |
|
1wlkd.f |
|- F = <" J "> |
| 3 |
|
1wlkd.x |
|- ( ph -> X e. V ) |
| 4 |
|
1wlkd.y |
|- ( ph -> Y e. V ) |
| 5 |
3 4
|
s2cld |
|- ( ph -> <" X Y "> e. Word V ) |
| 6 |
|
wrdf |
|- ( <" X Y "> e. Word V -> <" X Y "> : ( 0 ..^ ( # ` <" X Y "> ) ) --> V ) |
| 7 |
|
1z |
|- 1 e. ZZ |
| 8 |
|
fzval3 |
|- ( 1 e. ZZ -> ( 0 ... 1 ) = ( 0 ..^ ( 1 + 1 ) ) ) |
| 9 |
7 8
|
ax-mp |
|- ( 0 ... 1 ) = ( 0 ..^ ( 1 + 1 ) ) |
| 10 |
2
|
fveq2i |
|- ( # ` F ) = ( # ` <" J "> ) |
| 11 |
|
s1len |
|- ( # ` <" J "> ) = 1 |
| 12 |
10 11
|
eqtri |
|- ( # ` F ) = 1 |
| 13 |
12
|
oveq2i |
|- ( 0 ... ( # ` F ) ) = ( 0 ... 1 ) |
| 14 |
|
s2len |
|- ( # ` <" X Y "> ) = 2 |
| 15 |
|
df-2 |
|- 2 = ( 1 + 1 ) |
| 16 |
14 15
|
eqtri |
|- ( # ` <" X Y "> ) = ( 1 + 1 ) |
| 17 |
16
|
oveq2i |
|- ( 0 ..^ ( # ` <" X Y "> ) ) = ( 0 ..^ ( 1 + 1 ) ) |
| 18 |
9 13 17
|
3eqtr4i |
|- ( 0 ... ( # ` F ) ) = ( 0 ..^ ( # ` <" X Y "> ) ) |
| 19 |
18
|
a1i |
|- ( <" X Y "> e. Word V -> ( 0 ... ( # ` F ) ) = ( 0 ..^ ( # ` <" X Y "> ) ) ) |
| 20 |
19
|
feq2d |
|- ( <" X Y "> e. Word V -> ( <" X Y "> : ( 0 ... ( # ` F ) ) --> V <-> <" X Y "> : ( 0 ..^ ( # ` <" X Y "> ) ) --> V ) ) |
| 21 |
6 20
|
mpbird |
|- ( <" X Y "> e. Word V -> <" X Y "> : ( 0 ... ( # ` F ) ) --> V ) |
| 22 |
5 21
|
syl |
|- ( ph -> <" X Y "> : ( 0 ... ( # ` F ) ) --> V ) |
| 23 |
1
|
feq1i |
|- ( P : ( 0 ... ( # ` F ) ) --> V <-> <" X Y "> : ( 0 ... ( # ` F ) ) --> V ) |
| 24 |
22 23
|
sylibr |
|- ( ph -> P : ( 0 ... ( # ` F ) ) --> V ) |