Step |
Hyp |
Ref |
Expression |
1 |
|
lencl |
|- ( A e. Word V -> ( # ` A ) e. NN0 ) |
2 |
|
nn0fz0 |
|- ( ( # ` A ) e. NN0 <-> ( # ` A ) e. ( 0 ... ( # ` A ) ) ) |
3 |
1 2
|
sylib |
|- ( A e. Word V -> ( # ` A ) e. ( 0 ... ( # ` A ) ) ) |
4 |
3
|
3ad2ant1 |
|- ( ( A e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> ( # ` A ) e. ( 0 ... ( # ` A ) ) ) |
5 |
|
eleq1 |
|- ( N = ( # ` A ) -> ( N e. ( 0 ... ( # ` A ) ) <-> ( # ` A ) e. ( 0 ... ( # ` A ) ) ) ) |
6 |
5
|
3ad2ant3 |
|- ( ( A e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> ( N e. ( 0 ... ( # ` A ) ) <-> ( # ` A ) e. ( 0 ... ( # ` A ) ) ) ) |
7 |
4 6
|
mpbird |
|- ( ( A e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> N e. ( 0 ... ( # ` A ) ) ) |
8 |
|
eqid |
|- ( # ` A ) = ( # ` A ) |
9 |
8
|
pfxccatpfx1 |
|- ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... ( # ` A ) ) ) -> ( ( A ++ B ) prefix N ) = ( A prefix N ) ) |
10 |
7 9
|
syld3an3 |
|- ( ( A e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> ( ( A ++ B ) prefix N ) = ( A prefix N ) ) |
11 |
|
oveq2 |
|- ( N = ( # ` A ) -> ( A prefix N ) = ( A prefix ( # ` A ) ) ) |
12 |
11
|
3ad2ant3 |
|- ( ( A e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> ( A prefix N ) = ( A prefix ( # ` A ) ) ) |
13 |
|
pfxid |
|- ( A e. Word V -> ( A prefix ( # ` A ) ) = A ) |
14 |
13
|
3ad2ant1 |
|- ( ( A e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> ( A prefix ( # ` A ) ) = A ) |
15 |
10 12 14
|
3eqtrd |
|- ( ( A e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> ( ( A ++ B ) prefix N ) = A ) |