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

Metamath Proof Explorer

Theorem s1co

Description: Mapping of a singleton word. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s1co 
|- ( ( S e. A /\ F : A --> B ) -> ( F o. <" S "> ) = <" ( F ` S ) "> )

Proof

Step Hyp Ref Expression
1 s1val 
 |-  ( S e. A -> <" S "> = { <. 0 , S >. } )
2 0cn 
 |-  0 e. CC
3 xpsng 
 |-  ( ( 0 e. CC /\ S e. A ) -> ( { 0 } X. { S } ) = { <. 0 , S >. } )
4 2 3 mpan 
 |-  ( S e. A -> ( { 0 } X. { S } ) = { <. 0 , S >. } )
5 1 4 eqtr4d 
 |-  ( S e. A -> <" S "> = ( { 0 } X. { S } ) )
6 5 adantr 
 |-  ( ( S e. A /\ F : A --> B ) -> <" S "> = ( { 0 } X. { S } ) )
7 6 coeq2d 
 |-  ( ( S e. A /\ F : A --> B ) -> ( F o. <" S "> ) = ( F o. ( { 0 } X. { S } ) ) )
8 fvex 
 |-  ( F ` S ) e. _V
9 s1val 
 |-  ( ( F ` S ) e. _V -> <" ( F ` S ) "> = { <. 0 , ( F ` S ) >. } )
10 8 9 ax-mp 
 |-  <" ( F ` S ) "> = { <. 0 , ( F ` S ) >. }
11 c0ex 
 |-  0 e. _V
12 11 8 xpsn 
 |-  ( { 0 } X. { ( F ` S ) } ) = { <. 0 , ( F ` S ) >. }
13 10 12 eqtr4i 
 |-  <" ( F ` S ) "> = ( { 0 } X. { ( F ` S ) } )
14 ffn 
 |-  ( F : A --> B -> F Fn A )
15 id 
 |-  ( S e. A -> S e. A )
16 fcoconst 
 |-  ( ( F Fn A /\ S e. A ) -> ( F o. ( { 0 } X. { S } ) ) = ( { 0 } X. { ( F ` S ) } ) )
17 14 15 16 syl2anr 
 |-  ( ( S e. A /\ F : A --> B ) -> ( F o. ( { 0 } X. { S } ) ) = ( { 0 } X. { ( F ` S ) } ) )
18 13 17 eqtr4id 
 |-  ( ( S e. A /\ F : A --> B ) -> <" ( F ` S ) "> = ( F o. ( { 0 } X. { S } ) ) )
19 7 18 eqtr4d 
 |-  ( ( S e. A /\ F : A --> B ) -> ( F o. <" S "> ) = <" ( F ` S ) "> )