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

Proof

Step	Hyp	Ref	Expression
1		vrgpfval.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
2		vrgpfval.u	⊢ 𝑈 = ( varFGrp ‘ 𝐼 )
3		elex	⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ V )
4		id	⊢ ( 𝑖 = 𝐼 → 𝑖 = 𝐼 )
5		fveq2	⊢ ( 𝑖 = 𝐼 → ( ~FG ‘ 𝑖 ) = ( ~FG ‘ 𝐼 ) )
6	5 1	eqtr4di	⊢ ( 𝑖 = 𝐼 → ( ~FG ‘ 𝑖 ) = ∼ )
7	6	eceq2d	⊢ ( 𝑖 = 𝐼 → [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ( ~FG ‘ 𝑖 ) = [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ )
8	4 7	mpteq12dv	⊢ ( 𝑖 = 𝐼 → ( 𝑗 ∈ 𝑖 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ( ~FG ‘ 𝑖 ) ) = ( 𝑗 ∈ 𝐼 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ ) )
9		df-vrgp	⊢ varFGrp = ( 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ( ~FG ‘ 𝑖 ) ) )
10		vex	⊢ 𝑖 ∈ V
11	10	mptex	⊢ ( 𝑗 ∈ 𝑖 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ( ~FG ‘ 𝑖 ) ) ∈ V
12	8 9 11	fvmpt3i	⊢ ( 𝐼 ∈ V → ( varFGrp ‘ 𝐼 ) = ( 𝑗 ∈ 𝐼 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ ) )
13	3 12	syl	⊢ ( 𝐼 ∈ 𝑉 → ( varFGrp ‘ 𝐼 ) = ( 𝑗 ∈ 𝐼 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ ) )
14	2 13	syl5eq	⊢ ( 𝐼 ∈ 𝑉 → 𝑈 = ( 𝑗 ∈ 𝐼 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ ) )