Metamath Proof Explorer

Theorem vrgpfval

Description: The canonical injection from the generating set I to the base set of the free group. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses vrgpfval.r ⊢ ∼ ˙ = ~ FG ⁡ I
vrgpfval.u ⊢ U = var FGrp ⁡ I
Assertion vrgpfval ⊢ I ∈ V → U = j ∈ I ⟼ ⟨“ j ∅ ”⟩ ∼ ˙

Proof

Step Hyp Ref Expression
1 vrgpfval.r ⊢ ∼ ˙ = ~ FG ⁡ I
2 vrgpfval.u ⊢ U = var FGrp ⁡ I
3 elex ⊢ I ∈ V → I ∈ V
4 id ⊢ i = I → i = I
5 fveq2 ⊢ i = I → ~ FG ⁡ i = ~ FG ⁡ I
6 5 1 eqtr4di ⊢ i = I → ~ FG ⁡ i = ∼ ˙
7 6 eceq2d ⊢ i = I → ⟨“ j ∅ ”⟩ ~ FG ⁡ i = ⟨“ j ∅ ”⟩ ∼ ˙
8 4 7 mpteq12dv ⊢ i = I → j ∈ i ⟼ ⟨“ j ∅ ”⟩ ~ FG ⁡ i = j ∈ I ⟼ ⟨“ j ∅ ”⟩ ∼ ˙
9 df-vrgp ⊢ var FGrp = i ∈ V ⟼ j ∈ i ⟼ ⟨“ j ∅ ”⟩ ~ FG ⁡ i
10 vex ⊢ i ∈ V
11 10 mptex ⊢ j ∈ i ⟼ ⟨“ j ∅ ”⟩ ~ FG ⁡ i ∈ V
12 8 9 11 fvmpt3i ⊢ I ∈ V → var FGrp ⁡ I = j ∈ I ⟼ ⟨“ j ∅ ”⟩ ∼ ˙
13 3 12 syl ⊢ I ∈ V → var FGrp ⁡ I = j ∈ I ⟼ ⟨“ j ∅ ”⟩ ∼ ˙
14 2 13 eqtrid ⊢ I ∈ V → U = j ∈ I ⟼ ⟨“ j ∅ ”⟩ ∼ ˙