Definition df-vrgp 18124

Description: Define the canonical injection from the generating set I into the base set of the free group. (Contributed by Mario Carneiro, 2-Oct-2015.)

Assertion

Ref	Expression
df-vrgp	|- varFGrp = ( i e. _V |-> ( j e. i |-> [ <" <. j , (/) >. "> ] ( ~FG ` i ) ) )

Distinct variable group:   i, j

Detailed syntax breakdown of Definition df-vrgp

Step	Hyp	Ref	Expression
1		cvrgp 18121	. 2 class varFGrp
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	. . . . . . 7 class j
7		c0 3915	. . . . . . 7 class (/)
8	6, 7	cop 4183	. . . . . 6 class <. j , (/) >.
9	8	cs1 13294	. . . . 5 class <" <. j , (/) >. ">
10		cefg 18119	. . . . . 6 class ~FG
11	5, 10	cfv 5888	. . . . 5 class ( ~FG ` i )
12	9, 11	cec 7740	. . . 4 class [ <" <. j , (/) >. "> ] ( ~FG ` i )
13	4, 5, 12	cmpt 4729	. . 3 class ( j e. i |-> [ <" <. j , (/) >. "> ] ( ~FG ` i ) )
14	2, 3, 13	cmpt 4729	. 2 class ( i e. _V |-> ( j e. i |-> [ <" <. j , (/) >. "> ] ( ~FG ` i ) ) )
15	1, 14	wceq 1483	1 wff varFGrp = ( i e. _V |-> ( j e. i |-> [ <" <. j , (/) >. "> ] ( ~FG ` i ) ) )

This definition is referenced by:  vrgpfval  18179