Step |
Hyp |
Ref |
Expression |
1 |
|
cats1cld.1 |
|- T = ( S ++ <" X "> ) |
2 |
|
cats1cld.2 |
|- ( ph -> S e. Word A ) |
3 |
|
cats1cld.3 |
|- ( ph -> X e. A ) |
4 |
|
cats1co.4 |
|- ( ph -> F : A --> B ) |
5 |
|
cats1co.5 |
|- ( ph -> ( F o. S ) = U ) |
6 |
|
cats1co.6 |
|- V = ( U ++ <" ( F ` X ) "> ) |
7 |
3
|
s1cld |
|- ( ph -> <" X "> e. Word A ) |
8 |
|
ccatco |
|- ( ( S e. Word A /\ <" X "> e. Word A /\ F : A --> B ) -> ( F o. ( S ++ <" X "> ) ) = ( ( F o. S ) ++ ( F o. <" X "> ) ) ) |
9 |
2 7 4 8
|
syl3anc |
|- ( ph -> ( F o. ( S ++ <" X "> ) ) = ( ( F o. S ) ++ ( F o. <" X "> ) ) ) |
10 |
|
s1co |
|- ( ( X e. A /\ F : A --> B ) -> ( F o. <" X "> ) = <" ( F ` X ) "> ) |
11 |
3 4 10
|
syl2anc |
|- ( ph -> ( F o. <" X "> ) = <" ( F ` X ) "> ) |
12 |
5 11
|
oveq12d |
|- ( ph -> ( ( F o. S ) ++ ( F o. <" X "> ) ) = ( U ++ <" ( F ` X ) "> ) ) |
13 |
9 12
|
eqtrd |
|- ( ph -> ( F o. ( S ++ <" X "> ) ) = ( U ++ <" ( F ` X ) "> ) ) |
14 |
1
|
coeq2i |
|- ( F o. T ) = ( F o. ( S ++ <" X "> ) ) |
15 |
13 14 6
|
3eqtr4g |
|- ( ph -> ( F o. T ) = V ) |