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