Theorem vrmdf

Description: The mapping from the index set to the generators is a function into the free monoid. (Contributed by Mario Carneiro, 27-Feb-2016)

	Ref	Expression
Hypothesis	vrmdfval.u	⊢ 𝑈 = ( varFMnd ‘ 𝐼 )
Assertion	vrmdf	⊢ ( 𝐼 ∈ 𝑉 → 𝑈 : 𝐼 ⟶ Word 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		vrmdfval.u	⊢ 𝑈 = ( varFMnd ‘ 𝐼 )
2	1	vrmdfval	⊢ ( 𝐼 ∈ 𝑉 → 𝑈 = ( 𝑗 ∈ 𝐼 ↦ ⟨“ 𝑗 ”⟩ ) )
3		s1cl	⊢ ( 𝑗 ∈ 𝐼 → ⟨“ 𝑗 ”⟩ ∈ Word 𝐼 )
4	3	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐼 ) → ⟨“ 𝑗 ”⟩ ∈ Word 𝐼 )
5	2 4	fmpt3d	⊢ ( 𝐼 ∈ 𝑉 → 𝑈 : 𝐼 ⟶ Word 𝐼 )