This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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