# Metamath Proof Explorer

## Theorem efger

Description: Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses efgval.w ${⊢}{W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
efgval.r
Assertion efger

### Proof

Step Hyp Ref Expression
1 efgval.w ${⊢}{W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
2 efgval.r
3 1 efglem ${⊢}\exists {r}\phantom{\rule{.4em}{0ex}}\left({r}\mathrm{Er}{W}\wedge \forall {x}\in {W}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(0\dots \left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {z}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{x}{r}\left({x}\mathrm{splice}⟨{n},{n},⟨“⟨{y},{z}⟩⟨{y},{1}_{𝑜}\setminus {z}⟩”⟩⟩\right)\right)$
4 abn0 ${⊢}\left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {x}\in {W}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(0\dots \left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {z}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{x}{r}\left({x}\mathrm{splice}⟨{n},{n},⟨“⟨{y},{z}⟩⟨{y},{1}_{𝑜}\setminus {z}⟩”⟩⟩\right)\right)\right\}\ne \varnothing ↔\exists {r}\phantom{\rule{.4em}{0ex}}\left({r}\mathrm{Er}{W}\wedge \forall {x}\in {W}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(0\dots \left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {z}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{x}{r}\left({x}\mathrm{splice}⟨{n},{n},⟨“⟨{y},{z}⟩⟨{y},{1}_{𝑜}\setminus {z}⟩”⟩⟩\right)\right)$
5 3 4 mpbir ${⊢}\left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {x}\in {W}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(0\dots \left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {z}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{x}{r}\left({x}\mathrm{splice}⟨{n},{n},⟨“⟨{y},{z}⟩⟨{y},{1}_{𝑜}\setminus {z}⟩”⟩⟩\right)\right)\right\}\ne \varnothing$
6 ereq1 ${⊢}{w}={r}\to \left({w}\mathrm{Er}{W}↔{r}\mathrm{Er}{W}\right)$
7 6 ralab2 ${⊢}\forall {w}\in \left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {x}\in {W}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(0\dots \left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {z}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{x}{r}\left({x}\mathrm{splice}⟨{n},{n},⟨“⟨{y},{z}⟩⟨{y},{1}_{𝑜}\setminus {z}⟩”⟩⟩\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{w}\mathrm{Er}{W}↔\forall {r}\phantom{\rule{.4em}{0ex}}\left(\left({r}\mathrm{Er}{W}\wedge \forall {x}\in {W}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(0\dots \left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {z}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{x}{r}\left({x}\mathrm{splice}⟨{n},{n},⟨“⟨{y},{z}⟩⟨{y},{1}_{𝑜}\setminus {z}⟩”⟩⟩\right)\right)\to {r}\mathrm{Er}{W}\right)$
8 simpl ${⊢}\left({r}\mathrm{Er}{W}\wedge \forall {x}\in {W}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(0\dots \left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {z}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{x}{r}\left({x}\mathrm{splice}⟨{n},{n},⟨“⟨{y},{z}⟩⟨{y},{1}_{𝑜}\setminus {z}⟩”⟩⟩\right)\right)\to {r}\mathrm{Er}{W}$
9 7 8 mpgbir ${⊢}\forall {w}\in \left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {x}\in {W}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(0\dots \left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {z}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{x}{r}\left({x}\mathrm{splice}⟨{n},{n},⟨“⟨{y},{z}⟩⟨{y},{1}_{𝑜}\setminus {z}⟩”⟩⟩\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{w}\mathrm{Er}{W}$
10 iiner ${⊢}\left(\left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {x}\in {W}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(0\dots \left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {z}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{x}{r}\left({x}\mathrm{splice}⟨{n},{n},⟨“⟨{y},{z}⟩⟨{y},{1}_{𝑜}\setminus {z}⟩”⟩⟩\right)\right)\right\}\ne \varnothing \wedge \forall {w}\in \left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {x}\in {W}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(0\dots \left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {z}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{x}{r}\left({x}\mathrm{splice}⟨{n},{n},⟨“⟨{y},{z}⟩⟨{y},{1}_{𝑜}\setminus {z}⟩”⟩⟩\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{w}\mathrm{Er}{W}\right)\to \bigcap _{{w}\in \left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {x}\in {W}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(0\dots \left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {z}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{x}{r}\left({x}\mathrm{splice}⟨{n},{n},⟨“⟨{y},{z}⟩⟨{y},{1}_{𝑜}\setminus {z}⟩”⟩⟩\right)\right)\right\}}{w}\mathrm{Er}{W}$
11 5 9 10 mp2an ${⊢}\bigcap _{{w}\in \left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {x}\in {W}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(0\dots \left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {z}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{x}{r}\left({x}\mathrm{splice}⟨{n},{n},⟨“⟨{y},{z}⟩⟨{y},{1}_{𝑜}\setminus {z}⟩”⟩⟩\right)\right)\right\}}{w}\mathrm{Er}{W}$
12 1 2 efgval
13 intiin ${⊢}\bigcap \left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {x}\in {W}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(0\dots \left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {z}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{x}{r}\left({x}\mathrm{splice}⟨{n},{n},⟨“⟨{y},{z}⟩⟨{y},{1}_{𝑜}\setminus {z}⟩”⟩⟩\right)\right)\right\}=\bigcap _{{w}\in \left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {x}\in {W}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(0\dots \left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {z}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{x}{r}\left({x}\mathrm{splice}⟨{n},{n},⟨“⟨{y},{z}⟩⟨{y},{1}_{𝑜}\setminus {z}⟩”⟩⟩\right)\right)\right\}}{w}$
14 12 13 eqtri
15 ereq1
16 14 15 ax-mp
17 11 16 mpbir