| 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 |
|
wlkd.e |
|- ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) |
| 5 |
1 2 3 4
|
wlkdlem2 |
|- ( ph -> ( ( ( # ` F ) e. NN -> ( P ` ( # ` F ) ) e. ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) e. ( I ` ( F ` k ) ) ) ) |
| 6 |
|
elfvdm |
|- ( ( P ` k ) e. ( I ` ( F ` k ) ) -> ( F ` k ) e. dom I ) |
| 7 |
6
|
ralimi |
|- ( A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) e. ( I ` ( F ` k ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( F ` k ) e. dom I ) |
| 8 |
5 7
|
simpl2im |
|- ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) ( F ` k ) e. dom I ) |
| 9 |
|
iswrdsymb |
|- ( ( F e. Word _V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( F ` k ) e. dom I ) -> F e. Word dom I ) |
| 10 |
2 8 9
|
syl2anc |
|- ( ph -> F e. Word dom I ) |