Step |
Hyp |
Ref |
Expression |
1 |
|
df-s3 |
|- <" A B C "> = ( <" A B "> ++ <" C "> ) |
2 |
|
s2cl |
|- ( ( A e. S /\ B e. S ) -> <" A B "> e. Word S ) |
3 |
|
cats1un |
|- ( ( <" A B "> e. Word S /\ C e. S ) -> ( <" A B "> ++ <" C "> ) = ( <" A B "> u. { <. ( # ` <" A B "> ) , C >. } ) ) |
4 |
2 3
|
stoic3 |
|- ( ( A e. S /\ B e. S /\ C e. S ) -> ( <" A B "> ++ <" C "> ) = ( <" A B "> u. { <. ( # ` <" A B "> ) , C >. } ) ) |
5 |
|
s2prop |
|- ( ( A e. S /\ B e. S ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } ) |
6 |
5
|
3adant3 |
|- ( ( A e. S /\ B e. S /\ C e. S ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } ) |
7 |
|
s2len |
|- ( # ` <" A B "> ) = 2 |
8 |
7
|
opeq1i |
|- <. ( # ` <" A B "> ) , C >. = <. 2 , C >. |
9 |
8
|
sneqi |
|- { <. ( # ` <" A B "> ) , C >. } = { <. 2 , C >. } |
10 |
9
|
a1i |
|- ( ( A e. S /\ B e. S /\ C e. S ) -> { <. ( # ` <" A B "> ) , C >. } = { <. 2 , C >. } ) |
11 |
6 10
|
uneq12d |
|- ( ( A e. S /\ B e. S /\ C e. S ) -> ( <" A B "> u. { <. ( # ` <" A B "> ) , C >. } ) = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. } ) ) |
12 |
|
df-tp |
|- { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. } ) |
13 |
12
|
eqcomi |
|- ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. } ) = { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } |
14 |
13
|
a1i |
|- ( ( A e. S /\ B e. S /\ C e. S ) -> ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. } ) = { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } ) |
15 |
4 11 14
|
3eqtrd |
|- ( ( A e. S /\ B e. S /\ C e. S ) -> ( <" A B "> ++ <" C "> ) = { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } ) |
16 |
1 15
|
eqtrid |
|- ( ( A e. S /\ B e. S /\ C e. S ) -> <" A B C "> = { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } ) |