Definition df-vrgp 19730

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 19727	. 2 class varFGrp
2		vi	. . 3 setvar 𝑖
3		cvv 3479	. . 3 class V
4		vj	. . . 4 setvar 𝑗
5	2	cv 1538	. . . 4 class 𝑖
6	4	cv 1538	. . . . . . 7 class 𝑗
7		c0 4332	. . . . . . 7 class ∅
8	6, 7	cop 4631	. . . . . 6 class ⟨𝑗, ∅⟩
9	8	cs1 14634	. . . . 5 class ⟨“⟨𝑗, ∅⟩”⟩
10		cefg 19725	. . . . . 6 class ~FG
11	5, 10	cfv 6560	. . . . 5 class ( ~FG ‘𝑖)
12	9, 11	cec 8744	. . . 4 class [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖)
13	4, 5, 12	cmpt 5224	. . 3 class (𝑗 ∈ 𝑖 ↦ [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖))
14	2, 3, 13	cmpt 5224	. 2 class (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖)))
15	1, 14	wceq 1539	1 wff varFGrp = (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖)))

This definition is referenced by:  vrgpfval  19785