Step |
Hyp |
Ref |
Expression |
1 |
|
lencl |
|- ( A e. Word V -> ( # ` A ) e. NN0 ) |
2 |
|
lencl |
|- ( B e. Word V -> ( # ` B ) e. NN0 ) |
3 |
|
elfz0add |
|- ( ( ( # ` A ) e. NN0 /\ ( # ` B ) e. NN0 ) -> ( N e. ( 0 ... ( # ` A ) ) -> N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) ) |
4 |
1 2 3
|
syl2an |
|- ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( # ` A ) ) -> N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) ) |
5 |
|
ccatlen |
|- ( ( A e. Word V /\ B e. Word V ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) ) |
6 |
5
|
oveq2d |
|- ( ( A e. Word V /\ B e. Word V ) -> ( 0 ... ( # ` ( A ++ B ) ) ) = ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) |
7 |
6
|
eleq2d |
|- ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( # ` ( A ++ B ) ) ) <-> N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) ) |
8 |
4 7
|
sylibrd |
|- ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( # ` A ) ) -> N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) ) |