| Step |
Hyp |
Ref |
Expression |
| 1 |
|
wlkiswwlks2lem.f |
|- F = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) |
| 2 |
1
|
wlkiswwlks2lem1 |
|- ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( # ` F ) = ( ( # ` P ) - 1 ) ) |
| 3 |
|
wrdf |
|- ( P e. Word V -> P : ( 0 ..^ ( # ` P ) ) --> V ) |
| 4 |
|
lencl |
|- ( P e. Word V -> ( # ` P ) e. NN0 ) |
| 5 |
|
nn0z |
|- ( ( # ` P ) e. NN0 -> ( # ` P ) e. ZZ ) |
| 6 |
|
fzoval |
|- ( ( # ` P ) e. ZZ -> ( 0 ..^ ( # ` P ) ) = ( 0 ... ( ( # ` P ) - 1 ) ) ) |
| 7 |
5 6
|
syl |
|- ( ( # ` P ) e. NN0 -> ( 0 ..^ ( # ` P ) ) = ( 0 ... ( ( # ` P ) - 1 ) ) ) |
| 8 |
|
oveq2 |
|- ( ( ( # ` P ) - 1 ) = ( # ` F ) -> ( 0 ... ( ( # ` P ) - 1 ) ) = ( 0 ... ( # ` F ) ) ) |
| 9 |
8
|
eqcoms |
|- ( ( # ` F ) = ( ( # ` P ) - 1 ) -> ( 0 ... ( ( # ` P ) - 1 ) ) = ( 0 ... ( # ` F ) ) ) |
| 10 |
7 9
|
sylan9eq |
|- ( ( ( # ` P ) e. NN0 /\ ( # ` F ) = ( ( # ` P ) - 1 ) ) -> ( 0 ..^ ( # ` P ) ) = ( 0 ... ( # ` F ) ) ) |
| 11 |
10
|
feq2d |
|- ( ( ( # ` P ) e. NN0 /\ ( # ` F ) = ( ( # ` P ) - 1 ) ) -> ( P : ( 0 ..^ ( # ` P ) ) --> V <-> P : ( 0 ... ( # ` F ) ) --> V ) ) |
| 12 |
11
|
biimpcd |
|- ( P : ( 0 ..^ ( # ` P ) ) --> V -> ( ( ( # ` P ) e. NN0 /\ ( # ` F ) = ( ( # ` P ) - 1 ) ) -> P : ( 0 ... ( # ` F ) ) --> V ) ) |
| 13 |
12
|
expd |
|- ( P : ( 0 ..^ ( # ` P ) ) --> V -> ( ( # ` P ) e. NN0 -> ( ( # ` F ) = ( ( # ` P ) - 1 ) -> P : ( 0 ... ( # ` F ) ) --> V ) ) ) |
| 14 |
3 4 13
|
sylc |
|- ( P e. Word V -> ( ( # ` F ) = ( ( # ` P ) - 1 ) -> P : ( 0 ... ( # ` F ) ) --> V ) ) |
| 15 |
14
|
adantr |
|- ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( ( # ` F ) = ( ( # ` P ) - 1 ) -> P : ( 0 ... ( # ` F ) ) --> V ) ) |
| 16 |
2 15
|
mpd |
|- ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> P : ( 0 ... ( # ` F ) ) --> V ) |