Theorem vrmdf

Description: The mapping from the index set to the generators is a function into the free monoid. (Contributed by Mario Carneiro, 27-Feb-2016)

	Ref	Expression
Hypothesis	vrmdfval.u	$$⊢U={var}_{\mathit{FMnd}}\left(I\right)$$
Assertion	vrmdf	$$⊢I\in V\to U:I⟶\mathrm{Word}I$$

Proof

Step	Hyp	Ref	Expression
1		vrmdfval.u	$$⊢U={var}_{\mathit{FMnd}}\left(I\right)$$
2	1	vrmdfval	$$⊢I\in V\to U=\left(j\in I⟼⟨“j”⟩\right)$$
3		s1cl	$$⊢j\in I\to ⟨“j”⟩\in \mathrm{Word}I$$
4	3	adantl	$$⊢\left(I\in V\wedge j\in I\right)\to ⟨“j”⟩\in \mathrm{Word}I$$
5	2 4	fmpt3d	$$⊢I\in V\to U:I⟶\mathrm{Word}I$$