Definition df-vrgp 18839

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 18836	. 2 class varFGrp
2		vi	. . 3 setvar 𝑖
3		cvv 3496	. . 3 class V
4		vj	. . . 4 setvar 𝑗
5	2	cv 1536	. . . 4 class 𝑖
6	4	cv 1536	. . . . . . 7 class 𝑗
7		c0 4293	. . . . . . 7 class ∅
8	6, 7	cop 4575	. . . . . 6 class ⟨𝑗, ∅⟩
9	8	cs1 13951	. . . . 5 class ⟨“⟨𝑗, ∅⟩”⟩
10		cefg 18834	. . . . . 6 class ~FG
11	5, 10	cfv 6357	. . . . 5 class ( ~FG ‘𝑖)
12	9, 11	cec 8289	. . . 4 class [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖)
13	4, 5, 12	cmpt 5148	. . 3 class (𝑗 ∈ 𝑖 ↦ [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖))
14	2, 3, 13	cmpt 5148	. 2 class (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖)))
15	1, 14	wceq 1537	1 wff varFGrp = (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖)))

This definition is referenced by:  vrgpfval  18894