Definition df-frmd

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-frmd	$$⊢\mathrm{freeMnd}=\left(i\in \mathrm{V}⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}i⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}i\times \mathrm{Word}i\right)}⟩\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfrmd	$$class\mathrm{freeMnd}$$
1		vi	$$setvari$$
2		cvv	$$class\mathrm{V}$$
3		cbs	$$class\mathrm{Base}$$
4		cnx	$$class\mathrm{ndx}$$
5	4 3	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
6	1	cv	$$setvari$$
7	6	cword	$$class\mathrm{Word}i$$
8	5 7	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}i⟩$$
9		cplusg	$$class{+}_{𝑔}$$
10	4 9	cfv	$$class{+}_{\mathrm{ndx}}$$
11		cconcat	$$class\mathrm{++}$$
12	7 7	cxp	$$class\left(\mathrm{Word}i\times \mathrm{Word}i\right)$$
13	11 12	cres	$$class\left({\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}i\times \mathrm{Word}i\right)}\right)$$
14	10 13	cop	$$class⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}i\times \mathrm{Word}i\right)}⟩$$
15	8 14	cpr	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}i⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}i\times \mathrm{Word}i\right)}⟩\right\}$$
16	1 2 15	cmpt	$$class\left(i\in \mathrm{V}⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}i⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}i\times \mathrm{Word}i\right)}⟩\right\}\right)$$
17	0 16	wceq	$$wff\mathrm{freeMnd}=\left(i\in \mathrm{V}⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}i⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}i\times \mathrm{Word}i\right)}⟩\right\}\right)$$