Step |
Hyp |
Ref |
Expression |
1 |
|
s1cl |
|- ( X e. V -> <" X "> e. Word V ) |
2 |
1
|
adantr |
|- ( ( X e. V /\ Y e. V ) -> <" X "> e. Word V ) |
3 |
|
s1cl |
|- ( Y e. V -> <" Y "> e. Word V ) |
4 |
3
|
adantl |
|- ( ( X e. V /\ Y e. V ) -> <" Y "> e. Word V ) |
5 |
|
s1len |
|- ( # ` <" X "> ) = 1 |
6 |
5
|
a1i |
|- ( X e. V -> ( # ` <" X "> ) = 1 ) |
7 |
|
1nn |
|- 1 e. NN |
8 |
6 7
|
eqeltrdi |
|- ( X e. V -> ( # ` <" X "> ) e. NN ) |
9 |
|
lbfzo0 |
|- ( 0 e. ( 0 ..^ ( # ` <" X "> ) ) <-> ( # ` <" X "> ) e. NN ) |
10 |
8 9
|
sylibr |
|- ( X e. V -> 0 e. ( 0 ..^ ( # ` <" X "> ) ) ) |
11 |
10
|
adantr |
|- ( ( X e. V /\ Y e. V ) -> 0 e. ( 0 ..^ ( # ` <" X "> ) ) ) |
12 |
|
ccatval1OLD |
|- ( ( <" X "> e. Word V /\ <" Y "> e. Word V /\ 0 e. ( 0 ..^ ( # ` <" X "> ) ) ) -> ( ( <" X "> ++ <" Y "> ) ` 0 ) = ( <" X "> ` 0 ) ) |
13 |
2 4 11 12
|
syl3anc |
|- ( ( X e. V /\ Y e. V ) -> ( ( <" X "> ++ <" Y "> ) ` 0 ) = ( <" X "> ` 0 ) ) |
14 |
|
s1fv |
|- ( X e. V -> ( <" X "> ` 0 ) = X ) |
15 |
14
|
adantr |
|- ( ( X e. V /\ Y e. V ) -> ( <" X "> ` 0 ) = X ) |
16 |
13 15
|
eqtrd |
|- ( ( X e. V /\ Y e. V ) -> ( ( <" X "> ++ <" Y "> ) ` 0 ) = X ) |