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 𝑈 = ( varFMnd𝐼 )
Assertion vrmdfval ( 𝐼𝑉𝑈 = ( 𝑗𝐼 ↦ ⟨“ 𝑗 ”⟩ ) )

Proof

Step Hyp Ref Expression
1 vrmdfval.u 𝑈 = ( varFMnd𝐼 )
2 df-vrmd varFMnd = ( 𝑖 ∈ V ↦ ( 𝑗𝑖 ↦ ⟨“ 𝑗 ”⟩ ) )
3 mpteq1 ( 𝑖 = 𝐼 → ( 𝑗𝑖 ↦ ⟨“ 𝑗 ”⟩ ) = ( 𝑗𝐼 ↦ ⟨“ 𝑗 ”⟩ ) )
4 elex ( 𝐼𝑉𝐼 ∈ V )
5 mptexg ( 𝐼𝑉 → ( 𝑗𝐼 ↦ ⟨“ 𝑗 ”⟩ ) ∈ V )
6 2 3 4 5 fvmptd3 ( 𝐼𝑉 → ( varFMnd𝐼 ) = ( 𝑗𝐼 ↦ ⟨“ 𝑗 ”⟩ ) )
7 1 6 syl5eq ( 𝐼𝑉𝑈 = ( 𝑗𝐼 ↦ ⟨“ 𝑗 ”⟩ ) )