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	$$⊢{var}_{\mathit{FMnd}}=\left(i\in \mathrm{V}⟼\left(j\in i⟼⟨“j”⟩\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvrmd	$$class{var}_{\mathit{FMnd}}$$
1		vi	$$setvari$$
2		cvv	$$class\mathrm{V}$$
3		vj	$$setvarj$$
4	1	cv	$$setvari$$
5	3	cv	$$setvarj$$
6	5	cs1	$$class⟨“j”⟩$$
7	3 4 6	cmpt	$$class\left(j\in i⟼⟨“j”⟩\right)$$
8	1 2 7	cmpt	$$class\left(i\in \mathrm{V}⟼\left(j\in i⟼⟨“j”⟩\right)\right)$$
9	0 8	wceq	$$wff{var}_{\mathit{FMnd}}=\left(i\in \mathrm{V}⟼\left(j\in i⟼⟨“j”⟩\right)\right)$$