Theorem wrdco

Description: Mapping a word by a function. (Contributed by Stefan O'Rear, 27-Aug-2015)

	Ref	Expression
Assertion	wrdco	|- ( ( W e. Word A /\ F : A --> B ) -> ( F o. W ) e. Word B )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( W e. Word A /\ F : A --> B ) -> F : A --> B )
2		wrdf	|- ( W e. Word A -> W : ( 0 ..^ ( # ` W ) ) --> A )
3	2	adantr	|- ( ( W e. Word A /\ F : A --> B ) -> W : ( 0 ..^ ( # ` W ) ) --> A )
4		fco	|- ( ( F : A --> B /\ W : ( 0 ..^ ( # ` W ) ) --> A ) -> ( F o. W ) : ( 0 ..^ ( # ` W ) ) --> B )
5	1 3 4	syl2anc	|- ( ( W e. Word A /\ F : A --> B ) -> ( F o. W ) : ( 0 ..^ ( # ` W ) ) --> B )
6		iswrdi	|- ( ( F o. W ) : ( 0 ..^ ( # ` W ) ) --> B -> ( F o. W ) e. Word B )
7	5 6	syl	|- ( ( W e. Word A /\ F : A --> B ) -> ( F o. W ) e. Word B )