Definition df-vrmd 17387

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.)

Assertion

Ref	Expression
df-vrmd	|- varFMnd = ( i e. _V |-> ( j e. i |-> <" j "> ) )

Distinct variable group:   i, j

Detailed syntax breakdown of Definition df-vrmd

Step	Hyp	Ref	Expression
1		cvrmd 17385	. 2 class varFMnd
2		vi	. . 3 setvar i
3		cvv 3200	. . 3 class _V
4		vj	. . . 4 setvar j
5	2	cv 1482	. . . 4 class i
6	4	cv 1482	. . . . 5 class j
7	6	cs1 13294	. . . 4 class <" j ">
8	4, 5, 7	cmpt 4729	. . 3 class ( j e. i |-> <" j "> )
9	2, 3, 8	cmpt 4729	. 2 class ( i e. _V |-> ( j e. i |-> <" j "> ) )
10	1, 9	wceq 1483	1 wff varFMnd = ( i e. _V |-> ( j e. i |-> <" j "> ) )

This definition is referenced by:  vrmdfval  17393