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