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 = var FGrp I
vrgpf.m G = freeGrp I
vrgpf.x X = Base G
Assertion vrgpf I V U : I X

Proof

Step Hyp Ref Expression
1 vrgpfval.r ˙ = ~ FG I
2 vrgpfval.u U = var FGrp I
3 vrgpf.m G = freeGrp I
4 vrgpf.x X = Base G
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 ”⟩ Word I × 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 Word I × 2 𝑜 V
19 fvi Word I × 2 𝑜 V I Word I × 2 𝑜 = Word I × 2 𝑜
20 17 18 19 3syl I V j I I Word I × 2 𝑜 = Word I × 2 𝑜
21 13 20 eleqtrrd I V j I ⟨“ j ”⟩ I Word I × 2 𝑜
22 eqid I Word I × 2 𝑜 = I Word I × 2 𝑜
23 3 1 22 4 frgpeccl ⟨“ j ”⟩ I Word I × 2 𝑜 ⟨“ j ”⟩ ˙ X
24 21 23 syl I V j I ⟨“ j ”⟩ ˙ X
25 5 24 fmpt3d I V U : I X