Definition df-vrmd

Description: Define a free monoid over a set i of generators, defined as the set of finite strings on I with the operation of concatenation. (Contributed by Mario Carneiro, 27-Sep-2015)

	Ref	Expression
Assertion	df-vrmd	⊢ varFMnd = ( 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ ⟨“ 𝑗 ”⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvrmd	⊢ varFMnd
1		vi	⊢ 𝑖
2		cvv	⊢ V
3		vj	⊢ 𝑗
4	1	cv	⊢ 𝑖
5	3	cv	⊢ 𝑗
6	5	cs1	⊢ ⟨“ 𝑗 ”⟩
7	3 4 6	cmpt	⊢ ( 𝑗 ∈ 𝑖 ↦ ⟨“ 𝑗 ”⟩ )
8	1 2 7	cmpt	⊢ ( 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ ⟨“ 𝑗 ”⟩ ) )
9	0 8	wceq	⊢ varFMnd = ( 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ ⟨“ 𝑗 ”⟩ ) )