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 ‘ 𝐼 )
	vrgpfval.u	⊢ 𝑈 = ( varFGrp ‘ 𝐼 )
Assertion	vrgpval	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐴 ) = [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ )

Proof

Step	Hyp	Ref	Expression
1		vrgpfval.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
2		vrgpfval.u	⊢ 𝑈 = ( varFGrp ‘ 𝐼 )
3	1 2	vrgpfval	⊢ ( 𝐼 ∈ 𝑉 → 𝑈 = ( 𝑗 ∈ 𝐼 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ ) )
4	3	fveq1d	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑈 ‘ 𝐴 ) = ( ( 𝑗 ∈ 𝐼 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ ) ‘ 𝐴 ) )
5		opeq1	⊢ ( 𝑗 = 𝐴 → ⟨ 𝑗 , ∅ ⟩ = ⟨ 𝐴 , ∅ ⟩ )
6	5	s1eqd	⊢ ( 𝑗 = 𝐴 → ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ = ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ )
7	6	eceq1d	⊢ ( 𝑗 = 𝐴 → [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ = [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ )
8		eqid	⊢ ( 𝑗 ∈ 𝐼 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ ) = ( 𝑗 ∈ 𝐼 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ )
9	1	fvexi	⊢ ∼ ∈ V
10		ecexg	⊢ ( ∼ ∈ V → [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ ∈ V )
11	9 10	ax-mp	⊢ [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ ∈ V
12	7 8 11	fvmpt	⊢ ( 𝐴 ∈ 𝐼 → ( ( 𝑗 ∈ 𝐼 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ ) ‘ 𝐴 ) = [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ )
13	4 12	sylan9eq	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐴 ) = [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ )