Definition df-vrgp

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)

	Ref	Expression
Assertion	df-vrgp	$$⊢{var}_{\mathit{FGrp}}=\left(i\in \mathrm{V}⟼\left(j\in i⟼\left[⟨“⟨j,\varnothing ⟩”⟩\right]{~}_{\mathit{FG}}\left(i\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvrgp	$$class{var}_{\mathit{FGrp}}$$
1		vi	$$setvari$$
2		cvv	$$class\mathrm{V}$$
3		vj	$$setvarj$$
4	1	cv	$$setvari$$
5	3	cv	$$setvarj$$
6		c0	$$class\varnothing$$
7	5 6	cop	$$class⟨j,\varnothing ⟩$$
8	7	cs1	$$class⟨“⟨j,\varnothing ⟩”⟩$$
9		cefg	$$class{~}_{\mathit{FG}}$$
10	4 9	cfv	$$class{~}_{\mathit{FG}}\left(i\right)$$
11	8 10	cec	$$class\left[⟨“⟨j,\varnothing ⟩”⟩\right]{~}_{\mathit{FG}}\left(i\right)$$
12	3 4 11	cmpt	$$class\left(j\in i⟼\left[⟨“⟨j,\varnothing ⟩”⟩\right]{~}_{\mathit{FG}}\left(i\right)\right)$$
13	1 2 12	cmpt	$$class\left(i\in \mathrm{V}⟼\left(j\in i⟼\left[⟨“⟨j,\varnothing ⟩”⟩\right]{~}_{\mathit{FG}}\left(i\right)\right)\right)$$
14	0 13	wceq	$$wff{var}_{\mathit{FGrp}}=\left(i\in \mathrm{V}⟼\left(j\in i⟼\left[⟨“⟨j,\varnothing ⟩”⟩\right]{~}_{\mathit{FG}}\left(i\right)\right)\right)$$