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