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

Metamath Proof Explorer

Theorem vrgpval

Description: The value of the generating elements of a free group. (Contributed by Mario Carneiro, 2-Oct-2015)

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

Proof

Step Hyp Ref Expression
1 vrgpfval.r ⊢ ∼ ˙ = ~ FG ⁡ I
2 vrgpfval.u ⊢ U = var FGrp ⁡ I
3 1 2 vrgpfval ⊢ I ∈ V → U = j ∈ I ⟼ ⟨“ j ∅ ”⟩ ∼ ˙
4 3 fveq1d ⊢ I ∈ V → U ⁡ A = j ∈ I ⟼ ⟨“ j ∅ ”⟩ ∼ ˙ ⁡ A
5 opeq1 ⊢ j = A → j ∅ = A ∅
6 5 s1eqd ⊢ j = A → ⟨“ j ∅ ”⟩ = ⟨“ A ∅ ”⟩
7 6 eceq1d ⊢ j = A → ⟨“ j ∅ ”⟩ ∼ ˙ = ⟨“ A ∅ ”⟩ ∼ ˙
8 eqid ⊢ j ∈ I ⟼ ⟨“ j ∅ ”⟩ ∼ ˙ = j ∈ I ⟼ ⟨“ j ∅ ”⟩ ∼ ˙
9 1 fvexi ⊢ ∼ ˙ ∈ V
10 ecexg ⊢ ∼ ˙ ∈ V → ⟨“ A ∅ ”⟩ ∼ ˙ ∈ V
11 9 10 ax-mp ⊢ ⟨“ A ∅ ”⟩ ∼ ˙ ∈ V
12 7 8 11 fvmpt ⊢ A ∈ I → j ∈ I ⟼ ⟨“ j ∅ ”⟩ ∼ ˙ ⁡ A = ⟨“ A ∅ ”⟩ ∼ ˙
13 4 12 sylan9eq ⊢ I ∈ V ∧ A ∈ I → U ⁡ A = ⟨“ A ∅ ”⟩ ∼ ˙