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	⊢ varFGrp = ( 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ( ~FG ‘ 𝑖 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvrgp	⊢ varFGrp
1		vi	⊢ 𝑖
2		cvv	⊢ V
3		vj	⊢ 𝑗
4	1	cv	⊢ 𝑖
5	3	cv	⊢ 𝑗
6		c0	⊢ ∅
7	5 6	cop	⊢ ⟨ 𝑗 , ∅ ⟩
8	7	cs1	⊢ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩
9		cefg	⊢ ~FG
10	4 9	cfv	⊢ ( ~FG ‘ 𝑖 )
11	8 10	cec	⊢ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ( ~FG ‘ 𝑖 )
12	3 4 11	cmpt	⊢ ( 𝑗 ∈ 𝑖 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ( ~FG ‘ 𝑖 ) )
13	1 2 12	cmpt	⊢ ( 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ( ~FG ‘ 𝑖 ) ) )
14	0 13	wceq	⊢ varFGrp = ( 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ( ~FG ‘ 𝑖 ) ) )