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 = var FMnd I
Assertion vrmdfval I V U = j I ⟨“ j ”⟩

Proof

Step Hyp Ref Expression
1 vrmdfval.u U = var FMnd I
2 df-vrmd var FMnd = i V j i ⟨“ j ”⟩
3 mpteq1 i = I j i ⟨“ j ”⟩ = j I ⟨“ j ”⟩
4 elex I V I V
5 mptexg I V j I ⟨“ j ”⟩ V
6 2 3 4 5 fvmptd3 I V var FMnd I = j I ⟨“ j ”⟩
7 1 6 syl5eq I V U = j I ⟨“ j ”⟩