Metamath Proof Explorer


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𝑖 ) ) )