Theorem s3co

Description: Mapping a length 3 string by a function. (Contributed by Mario Carneiro, 27-Feb-2016)

	Ref	Expression
Hypotheses	s2co.1	|- ( ph -> F : X --> Y )
	s2co.2	|- ( ph -> A e. X )
	s2co.3	|- ( ph -> B e. X )
	s3co.4	|- ( ph -> C e. X )
Assertion	s3co	|- ( ph -> ( F o. <" A B C "> ) = <" ( F ` A ) ( F ` B ) ( F ` C ) "> )

Proof

Step	Hyp	Ref	Expression
1		s2co.1	|- ( ph -> F : X --> Y )
2		s2co.2	|- ( ph -> A e. X )
3		s2co.3	|- ( ph -> B e. X )
4		s3co.4	|- ( ph -> C e. X )
5		df-s3	|- <" A B C "> = ( <" A B "> ++ <" C "> )
6	2 3	s2cld	|- ( ph -> <" A B "> e. Word X )
7	1 2 3	s2co	|- ( ph -> ( F o. <" A B "> ) = <" ( F ` A ) ( F ` B ) "> )
8		df-s3	|- <" ( F ` A ) ( F ` B ) ( F ` C ) "> = ( <" ( F ` A ) ( F ` B ) "> ++ <" ( F ` C ) "> )
9	5 6 4 1 7 8	cats1co	|- ( ph -> ( F o. <" A B C "> ) = <" ( F ` A ) ( F ` B ) ( F ` C ) "> )