This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) "> )