Metamath Proof Explorer


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 = ( varFMnd ` I )
Assertion vrmdf
|- ( I e. V -> U : I --> Word I )

Proof

Step Hyp Ref Expression
1 vrmdfval.u
 |-  U = ( varFMnd ` I )
2 1 vrmdfval
 |-  ( I e. V -> U = ( j e. I |-> <" j "> ) )
3 s1cl
 |-  ( j e. I -> <" j "> e. Word I )
4 3 adantl
 |-  ( ( I e. V /\ j e. I ) -> <" j "> e. Word I )
5 2 4 fmpt3d
 |-  ( I e. V -> U : I --> Word I )