Theorem vrmdval

Description: The value of the generating elements of a free monoid. (Contributed by Mario Carneiro, 27-Feb-2016)

	Ref	Expression
Hypothesis	vrmdfval.u	|- U = ( varFMnd ` I )
Assertion	vrmdval	|- ( ( I e. V /\ A e. I ) -> ( U ` A ) = <" A "> )

Proof

Step	Hyp	Ref	Expression
1		vrmdfval.u	|- U = ( varFMnd ` I )
2	1	vrmdfval	|- ( I e. V -> U = ( j e. I |-> <" j "> ) )
3	2	adantr	|- ( ( I e. V /\ A e. I ) -> U = ( j e. I |-> <" j "> ) )
4		s1eq	|- ( j = A -> <" j "> = <" A "> )
5	4	adantl	|- ( ( ( I e. V /\ A e. I ) /\ j = A ) -> <" j "> = <" A "> )
6		simpr	|- ( ( I e. V /\ A e. I ) -> A e. I )
7		s1cl	|- ( A e. I -> <" A "> e. Word I )
8	7	adantl	|- ( ( I e. V /\ A e. I ) -> <" A "> e. Word I )
9	3 5 6 8	fvmptd	|- ( ( I e. V /\ A e. I ) -> ( U ` A ) = <" A "> )