Step |
Hyp |
Ref |
Expression |
1 |
|
1nn0 |
|- 1 e. NN0 |
2 |
1
|
a1i |
|- ( W =/= (/) -> 1 e. NN0 ) |
3 |
|
pfxval |
|- ( ( W e. Word V /\ 1 e. NN0 ) -> ( W prefix 1 ) = ( W substr <. 0 , 1 >. ) ) |
4 |
2 3
|
sylan2 |
|- ( ( W e. Word V /\ W =/= (/) ) -> ( W prefix 1 ) = ( W substr <. 0 , 1 >. ) ) |
5 |
|
1e0p1 |
|- 1 = ( 0 + 1 ) |
6 |
5
|
opeq2i |
|- <. 0 , 1 >. = <. 0 , ( 0 + 1 ) >. |
7 |
6
|
oveq2i |
|- ( W substr <. 0 , 1 >. ) = ( W substr <. 0 , ( 0 + 1 ) >. ) |
8 |
7
|
a1i |
|- ( ( W e. Word V /\ W =/= (/) ) -> ( W substr <. 0 , 1 >. ) = ( W substr <. 0 , ( 0 + 1 ) >. ) ) |
9 |
|
lennncl |
|- ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) e. NN ) |
10 |
|
lbfzo0 |
|- ( 0 e. ( 0 ..^ ( # ` W ) ) <-> ( # ` W ) e. NN ) |
11 |
9 10
|
sylibr |
|- ( ( W e. Word V /\ W =/= (/) ) -> 0 e. ( 0 ..^ ( # ` W ) ) ) |
12 |
|
swrds1 |
|- ( ( W e. Word V /\ 0 e. ( 0 ..^ ( # ` W ) ) ) -> ( W substr <. 0 , ( 0 + 1 ) >. ) = <" ( W ` 0 ) "> ) |
13 |
11 12
|
syldan |
|- ( ( W e. Word V /\ W =/= (/) ) -> ( W substr <. 0 , ( 0 + 1 ) >. ) = <" ( W ` 0 ) "> ) |
14 |
4 8 13
|
3eqtrd |
|- ( ( W e. Word V /\ W =/= (/) ) -> ( W prefix 1 ) = <" ( W ` 0 ) "> ) |