Metamath Proof Explorer


Theorem vrmdfval

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

Proof

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