Description: The canonical injection from the generating set I to the base set of the free monoid. (Contributed by Mario Carneiro, 27-Feb-2016)
Ref | Expression | ||
---|---|---|---|
Hypothesis | vrmdfval.u | |- U = ( varFMnd ` I ) |
|
Assertion | vrmdfval | |- ( I e. V -> U = ( j e. I |-> <" j "> ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vrmdfval.u | |- U = ( varFMnd ` I ) |
|
2 | df-vrmd | |- varFMnd = ( i e. _V |-> ( j e. i |-> <" j "> ) ) |
|
3 | mpteq1 | |- ( i = I -> ( j e. i |-> <" j "> ) = ( j e. I |-> <" j "> ) ) |
|
4 | elex | |- ( I e. V -> I e. _V ) |
|
5 | mptexg | |- ( I e. V -> ( j e. I |-> <" j "> ) e. _V ) |
|
6 | 2 3 4 5 | fvmptd3 | |- ( I e. V -> ( varFMnd ` I ) = ( j e. I |-> <" j "> ) ) |
7 | 1 6 | syl5eq | |- ( I e. V -> U = ( j e. I |-> <" j "> ) ) |