Definition df-vrgp 17947

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 17944	. 2 class varFGrp
2		vi	. . 3 setvar 𝑖
3		cvv 3173	. . 3 class V
4		vj	. . . 4 setvar 𝑗
5	2	cv 1474	. . . 4 class 𝑖
6	4	cv 1474	. . . . . . 7 class 𝑗
7		c0 3874	. . . . . . 7 class ∅
8	6, 7	cop 4131	. . . . . 6 class ⟨𝑗, ∅⟩
9	8	cs1 13149	. . . . 5 class ⟨“⟨𝑗, ∅⟩”⟩
10		cefg 17942	. . . . . 6 class ~FG
11	5, 10	cfv 5804	. . . . 5 class ( ~FG ‘𝑖)
12	9, 11	cec 7627	. . . 4 class [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖)
13	4, 5, 12	cmpt 4643	. . 3 class (𝑗 ∈ 𝑖 ↦ [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖))
14	2, 3, 13	cmpt 4643	. 2 class (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖)))
15	1, 14	wceq 1475	1 wff varFGrp = (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖)))

This definition is referenced by:  vrgpfval  18002