Definition df-vrmd 18017

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

Assertion

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

Distinct variable group:   𝑖,𝑗

Detailed syntax breakdown of Definition df-vrmd

Step	Hyp	Ref	Expression
1		cvrmd 18015	. 2 class varFMnd
2		vi	. . 3 setvar 𝑖
3		cvv 3496	. . 3 class V
4		vj	. . . 4 setvar 𝑗
5	2	cv 1536	. . . 4 class 𝑖
6	4	cv 1536	. . . . 5 class 𝑗
7	6	cs1 13951	. . . 4 class ⟨“𝑗”⟩
8	4, 5, 7	cmpt 5148	. . 3 class (𝑗 ∈ 𝑖 ↦ ⟨“𝑗”⟩)
9	2, 3, 8	cmpt 5148	. 2 class (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ ⟨“𝑗”⟩))
10	1, 9	wceq 1537	1 wff varFMnd = (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ ⟨“𝑗”⟩))

This definition is referenced by:  vrmdfval  18023