Theorem s2co

Description: Mapping a doubleton word 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 )
Assertion	s2co	|- ( ph -> ( F o. <" A B "> ) = <" ( F ` A ) ( F ` B ) "> )

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		df-s2	|- <" A B "> = ( <" A "> ++ <" B "> )
5	2	s1cld	|- ( ph -> <" A "> e. Word X )
6		s1co	|- ( ( A e. X /\ F : X --> Y ) -> ( F o. <" A "> ) = <" ( F ` A ) "> )
7	2 1 6	syl2anc	|- ( ph -> ( F o. <" A "> ) = <" ( F ` A ) "> )
8		df-s2	|- <" ( F ` A ) ( F ` B ) "> = ( <" ( F ` A ) "> ++ <" ( F ` B ) "> )
9	4 5 3 1 7 8	cats1co	|- ( ph -> ( F o. <" A B "> ) = <" ( F ` A ) ( F ` B ) "> )