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 | ||
Assertion | vrmdfval |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vrmdfval.u | ||
2 | df-vrmd | ||
3 | mpteq1 | ||
4 | elex | ||
5 | mptexg | ||
6 | 2 3 4 5 | fvmptd3 | |
7 | 1 6 | syl5eq |