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	|- freeMnd = ( i e. _V |-> { <. ( Base ` ndx ) , Word i >. , <. ( +g ` ndx ) , ( ++ |` ( Word i X. Word i ) ) >. } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfrmd	|- freeMnd
1		vi	|- i
2		cvv	|- _V
3		cbs	|- Base
4		cnx	|- ndx
5	4 3	cfv	|- ( Base ` ndx )
6	1	cv	|- i
7	6	cword	|- Word i
8	5 7	cop	|- <. ( Base ` ndx ) , Word i >.
9		cplusg	|- +g
10	4 9	cfv	|- ( +g ` ndx )
11		cconcat	|- ++
12	7 7	cxp	|- ( Word i X. Word i )
13	11 12	cres	|- ( ++ |` ( Word i X. Word i ) )
14	10 13	cop	|- <. ( +g ` ndx ) , ( ++ |` ( Word i X. Word i ) ) >.
15	8 14	cpr	|- { <. ( Base ` ndx ) , Word i >. , <. ( +g ` ndx ) , ( ++ |` ( Word i X. Word i ) ) >. }
16	1 2 15	cmpt	|- ( i e. _V |-> { <. ( Base ` ndx ) , Word i >. , <. ( +g ` ndx ) , ( ++ |` ( Word i X. Word i ) ) >. } )
17	0 16	wceq	|- freeMnd = ( i e. _V |-> { <. ( Base ` ndx ) , Word i >. , <. ( +g ` ndx ) , ( ++ |` ( Word i X. Word i ) ) >. } )