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	⊢ ( 𝐼 ∈ 𝑉 → 𝑈 = ( 𝑗 ∈ 𝐼 ↦ ⟨“ 𝑗 ”⟩ ) )