Definition df-vrgp 18124

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

Assertion

Ref	Expression
df-vrgp	⊢ varFGrp = (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖)))

Distinct variable group:   𝑖,𝑗

Detailed syntax breakdown of Definition df-vrgp

Step	Hyp	Ref	Expression
1		cvrgp 18121	. 2 class varFGrp
2		vi	. . 3 setvar 𝑖
3		cvv 3200	. . 3 class V
4		vj	. . . 4 setvar 𝑗
5	2	cv 1482	. . . 4 class 𝑖
6	4	cv 1482	. . . . . . 7 class 𝑗
7		c0 3915	. . . . . . 7 class ∅
8	6, 7	cop 4183	. . . . . 6 class ⟨𝑗, ∅⟩
9	8	cs1 13294	. . . . 5 class ⟨“⟨𝑗, ∅⟩”⟩
10		cefg 18119	. . . . . 6 class ~FG
11	5, 10	cfv 5888	. . . . 5 class ( ~FG ‘𝑖)
12	9, 11	cec 7740	. . . 4 class [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖)
13	4, 5, 12	cmpt 4729	. . 3 class (𝑗 ∈ 𝑖 ↦ [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖))
14	2, 3, 13	cmpt 4729	. 2 class (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖)))
15	1, 14	wceq 1483	1 wff varFGrp = (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖)))

This definition is referenced by:  vrgpfval  18179