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⁡I
vrgpfval.u ⊢U=varFGrp⁡I
vrgpf.m ⊢G=freeGrp⁡I
vrgpf.x ⊢X=BaseG
Assertion vrgpf ⊢I∈V→U:I⟶X

Proof

Step Hyp Ref Expression
1 vrgpfval.r ⊢∼˙=~FG⁡I
2 vrgpfval.u ⊢U=varFGrp⁡I
3 vrgpf.m ⊢G=freeGrp⁡I
4 vrgpf.x ⊢X=BaseG
5 1 2 vrgpfval ⊢I∈V→U=j∈I⟼⟨“j∅”⟩∼˙
6 0ex ⊢∅∈V
7 6 prid1 ⊢∅∈∅1𝑜
8 df2o3 ⊢2𝑜=∅1𝑜
9 7 8 eleqtrri ⊢∅∈2𝑜
10 opelxpi ⊢j∈I∧∅∈2𝑜→j∅∈I×2𝑜
11 9 10 mpan2 ⊢j∈I→j∅∈I×2𝑜
12 11 adantl ⊢I∈V∧j∈I→j∅∈I×2𝑜
13 12 s1cld ⊢I∈V∧j∈I→⟨“j∅”⟩∈WordI×2𝑜
14 2on ⊢2𝑜∈On
15 xpexg ⊢I∈V∧2𝑜∈On→I×2𝑜∈V
16 14 15 mpan2 ⊢I∈V→I×2𝑜∈V
17 16 adantr ⊢I∈V∧j∈I→I×2𝑜∈V
18 wrdexg ⊢I×2𝑜∈V→WordI×2𝑜∈V
19 fvi ⊢WordI×2𝑜∈V→I⁡WordI×2𝑜=WordI×2𝑜
20 17 18 19 3syl ⊢I∈V∧j∈I→I⁡WordI×2𝑜=WordI×2𝑜
21 13 20 eleqtrrd ⊢I∈V∧j∈I→⟨“j∅”⟩∈I⁡WordI×2𝑜
22 eqid ⊢I⁡WordI×2𝑜=I⁡WordI×2𝑜
23 3 1 22 4 frgpeccl ⊢⟨“j∅”⟩∈I⁡WordI×2𝑜→⟨“j∅”⟩∼˙∈X
24 21 23 syl ⊢I∈V∧j∈I→⟨“j∅”⟩∼˙∈X
25 5 24 fmpt3d ⊢I∈V→U:I⟶X