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

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