# Metamath Proof Explorer

## Theorem frgpeccl

Description: Closure of the quotient map in a free group. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypotheses frgp0.m ${⊢}{G}=\mathrm{freeGrp}\left({I}\right)$
frgp0.r
frgpeccl.w ${⊢}{W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
frgpeccl.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
Assertion frgpeccl

### Proof

Step Hyp Ref Expression
1 frgp0.m ${⊢}{G}=\mathrm{freeGrp}\left({I}\right)$
2 frgp0.r
3 frgpeccl.w ${⊢}{W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
4 frgpeccl.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
5 2 fvexi
6 5 ecelqsi
7 3 efgrcl ${⊢}{X}\in {W}\to \left({I}\in \mathrm{V}\wedge {W}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
8 7 simpld ${⊢}{X}\in {W}\to {I}\in \mathrm{V}$
9 eqid ${⊢}\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)=\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)$
10 1 9 2 frgpval
11 8 10 syl
12 7 simprd ${⊢}{X}\in {W}\to {W}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
13 2on ${⊢}{2}_{𝑜}\in \mathrm{On}$
14 xpexg ${⊢}\left({I}\in \mathrm{V}\wedge {2}_{𝑜}\in \mathrm{On}\right)\to {I}×{2}_{𝑜}\in \mathrm{V}$
15 8 13 14 sylancl ${⊢}{X}\in {W}\to {I}×{2}_{𝑜}\in \mathrm{V}$
16 eqid ${⊢}{\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}={\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
17 9 16 frmdbas ${⊢}{I}×{2}_{𝑜}\in \mathrm{V}\to {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
18 15 17 syl ${⊢}{X}\in {W}\to {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
19 12 18 eqtr4d ${⊢}{X}\in {W}\to {W}={\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
20 5 a1i
21 fvexd ${⊢}{X}\in {W}\to \mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)\in \mathrm{V}$
22 11 19 20 21 qusbas
23 22 4 syl6eqr
24 6 23 eleqtrd