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