wrdco

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

		Ref	Expression
	Assertion	wrdco	$⊢ (W \in Word A \land F : A ⟶ B) \to F \circ W \in Word B$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (W \in Word A \land F : A ⟶ B) \to F : A ⟶ B$
2		wrdf	$⊢ W \in Word A \to W : (0 ..^\|W\|) ⟶ A$
3	2	adantr	$⊢ (W \in Word A \land F : A ⟶ B) \to W : (0 ..^\|W\|) ⟶ A$
4		fco	$⊢ (F : A ⟶ B \land W : (0 ..^\|W\|) ⟶ A) \to (F \circ W) : (0 ..^\|W\|) ⟶ B$
5	1 3 4	syl2anc	$⊢ (W \in Word A \land F : A ⟶ B) \to (F \circ W) : (0 ..^\|W\|) ⟶ B$
6		iswrdi	$⊢ (F \circ W) : (0 ..^\|W\|) ⟶ B \to F \circ W \in Word B$
7	5 6	syl	$⊢ (W \in Word A \land F : A ⟶ B) \to F \circ W \in Word B$

Metamath Proof Explorer