This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ var FGrp = i ∈ V ⟼ j ∈ i ⟼ ⟨“ j ∅ ”⟩ ~ FG ⁡ i

Detailed syntax breakdown

Step Hyp Ref Expression
0 cvrgp class var FGrp
1 vi setvar i
2 cvv class V
3 vj setvar j
4 1 cv setvar i
5 3 cv setvar j
6 c0 class ∅
7 5 6 cop class j ∅
8 7 cs1 class ⟨“ j ∅ ”⟩
9 cefg class ~ FG
10 4 9 cfv class ~ FG ⁡ i
11 8 10 cec class ⟨“ j ∅ ”⟩ ~ FG ⁡ i
12 3 4 11 cmpt class j ∈ i ⟼ ⟨“ j ∅ ”⟩ ~ FG ⁡ i
13 1 2 12 cmpt class i ∈ V ⟼ j ∈ i ⟼ ⟨“ j ∅ ”⟩ ~ FG ⁡ i
14 0 13 wceq wff var FGrp = i ∈ V ⟼ j ∈ i ⟼ ⟨“ j ∅ ”⟩ ~ FG ⁡ i