Metamath Proof Explorer


Theorem vrgpf

Description: The mapping from the index set to the generators is a function into the free group. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses vrgpfval.r = ( ~FG𝐼 )
vrgpfval.u 𝑈 = ( varFGrp𝐼 )
vrgpf.m 𝐺 = ( freeGrp ‘ 𝐼 )
vrgpf.x 𝑋 = ( Base ‘ 𝐺 )
Assertion vrgpf ( 𝐼𝑉𝑈 : 𝐼𝑋 )

Proof

Step Hyp Ref Expression
1 vrgpfval.r = ( ~FG𝐼 )
2 vrgpfval.u 𝑈 = ( varFGrp𝐼 )
3 vrgpf.m 𝐺 = ( freeGrp ‘ 𝐼 )
4 vrgpf.x 𝑋 = ( Base ‘ 𝐺 )
5 1 2 vrgpfval ( 𝐼𝑉𝑈 = ( 𝑗𝐼 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ) )
6 0ex ∅ ∈ V
7 6 prid1 ∅ ∈ { ∅ , 1o }
8 df2o3 2o = { ∅ , 1o }
9 7 8 eleqtrri ∅ ∈ 2o
10 opelxpi ( ( 𝑗𝐼 ∧ ∅ ∈ 2o ) → ⟨ 𝑗 , ∅ ⟩ ∈ ( 𝐼 × 2o ) )
11 9 10 mpan2 ( 𝑗𝐼 → ⟨ 𝑗 , ∅ ⟩ ∈ ( 𝐼 × 2o ) )
12 11 adantl ( ( 𝐼𝑉𝑗𝐼 ) → ⟨ 𝑗 , ∅ ⟩ ∈ ( 𝐼 × 2o ) )
13 12 s1cld ( ( 𝐼𝑉𝑗𝐼 ) → ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ∈ Word ( 𝐼 × 2o ) )
14 2on 2o ∈ On
15 xpexg ( ( 𝐼𝑉 ∧ 2o ∈ On ) → ( 𝐼 × 2o ) ∈ V )
16 14 15 mpan2 ( 𝐼𝑉 → ( 𝐼 × 2o ) ∈ V )
17 16 adantr ( ( 𝐼𝑉𝑗𝐼 ) → ( 𝐼 × 2o ) ∈ V )
18 wrdexg ( ( 𝐼 × 2o ) ∈ V → Word ( 𝐼 × 2o ) ∈ V )
19 fvi ( Word ( 𝐼 × 2o ) ∈ V → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
20 17 18 19 3syl ( ( 𝐼𝑉𝑗𝐼 ) → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
21 13 20 eleqtrrd ( ( 𝐼𝑉𝑗𝐼 ) → ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ∈ ( I ‘ Word ( 𝐼 × 2o ) ) )
22 eqid ( I ‘ Word ( 𝐼 × 2o ) ) = ( I ‘ Word ( 𝐼 × 2o ) )
23 3 1 22 4 frgpeccl ( ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ∈ ( I ‘ Word ( 𝐼 × 2o ) ) → [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] 𝑋 )
24 21 23 syl ( ( 𝐼𝑉𝑗𝐼 ) → [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] 𝑋 )
25 5 24 fmpt3d ( 𝐼𝑉𝑈 : 𝐼𝑋 )