Step |
Hyp |
Ref |
Expression |
1 |
|
cats2cat.b |
|- B e. Word _V |
2 |
|
cats2cat.d |
|- D e. Word _V |
3 |
|
cats2cat.a |
|- A = ( B ++ <" X "> ) |
4 |
|
cats2cat.c |
|- C = ( <" Y "> ++ D ) |
5 |
3 4
|
oveq12i |
|- ( A ++ C ) = ( ( B ++ <" X "> ) ++ ( <" Y "> ++ D ) ) |
6 |
|
s1cli |
|- <" X "> e. Word _V |
7 |
|
ccatcl |
|- ( ( B e. Word _V /\ <" X "> e. Word _V ) -> ( B ++ <" X "> ) e. Word _V ) |
8 |
1 6 7
|
mp2an |
|- ( B ++ <" X "> ) e. Word _V |
9 |
|
s1cli |
|- <" Y "> e. Word _V |
10 |
|
ccatass |
|- ( ( ( B ++ <" X "> ) e. Word _V /\ <" Y "> e. Word _V /\ D e. Word _V ) -> ( ( ( B ++ <" X "> ) ++ <" Y "> ) ++ D ) = ( ( B ++ <" X "> ) ++ ( <" Y "> ++ D ) ) ) |
11 |
8 9 2 10
|
mp3an |
|- ( ( ( B ++ <" X "> ) ++ <" Y "> ) ++ D ) = ( ( B ++ <" X "> ) ++ ( <" Y "> ++ D ) ) |
12 |
|
ccatass |
|- ( ( B e. Word _V /\ <" X "> e. Word _V /\ <" Y "> e. Word _V ) -> ( ( B ++ <" X "> ) ++ <" Y "> ) = ( B ++ ( <" X "> ++ <" Y "> ) ) ) |
13 |
1 6 9 12
|
mp3an |
|- ( ( B ++ <" X "> ) ++ <" Y "> ) = ( B ++ ( <" X "> ++ <" Y "> ) ) |
14 |
|
df-s2 |
|- <" X Y "> = ( <" X "> ++ <" Y "> ) |
15 |
14
|
eqcomi |
|- ( <" X "> ++ <" Y "> ) = <" X Y "> |
16 |
15
|
oveq2i |
|- ( B ++ ( <" X "> ++ <" Y "> ) ) = ( B ++ <" X Y "> ) |
17 |
13 16
|
eqtri |
|- ( ( B ++ <" X "> ) ++ <" Y "> ) = ( B ++ <" X Y "> ) |
18 |
17
|
oveq1i |
|- ( ( ( B ++ <" X "> ) ++ <" Y "> ) ++ D ) = ( ( B ++ <" X Y "> ) ++ D ) |
19 |
5 11 18
|
3eqtr2i |
|- ( A ++ C ) = ( ( B ++ <" X Y "> ) ++ D ) |