Definition df-efg

Description: Define the free group equivalence relation, which is the smallest equivalence relation ~ such that for any words A , B and formal symbol x with inverse invg x , A B ~A x ( invg x ) B . (Contributed by Mario Carneiro, 1-Oct-2015)

	Ref	Expression
Assertion	df-efg	$$⊢{~}_{\mathit{FG}}=\left(i\in \mathrm{V}⟼\bigcap \left\{r|\left(r\mathrm{Er}\mathrm{Word}\left(i\times 2_{𝑜}\right)\wedge \forall x\in \mathrm{Word}\left(i\times 2_{𝑜}\right)\forall n\in \left(0\dots \left|x\right|\right)\forall y\in i\forall z\in 2_{𝑜}xr\left(x\mathrm{splice}⟨n,n,⟨“⟨y,z⟩⟨y,1_{𝑜}\setminus z⟩”⟩⟩\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cefg	$$class{~}_{\mathit{FG}}$$
1		vi	$$setvari$$
2		cvv	$$class\mathrm{V}$$
3		vr	$$setvarr$$
4	3	cv	$$setvarr$$
5	1	cv	$$setvari$$
6		c2o	$$class{2}_{𝑜}$$
7	5 6	cxp	$$class\left(i\times 2_{𝑜}\right)$$
8	7	cword	$$class\mathrm{Word}\left(i\times 2_{𝑜}\right)$$
9	8 4	wer	$$wffr\mathrm{Er}\mathrm{Word}\left(i\times 2_{𝑜}\right)$$
10		vx	$$setvarx$$
11		vn	$$setvarn$$
12		cc0	$$class0$$
13		cfz	$$class\dots$$
14		chash	$$class\left|.\right|$$
15	10	cv	$$setvarx$$
16	15 14	cfv	$$class\left|x\right|$$
17	12 16 13	co	$$class\left(0\dots \left|x\right|\right)$$
18		vy	$$setvary$$
19		vz	$$setvarz$$
20		csplice	$$class\mathrm{splice}$$
21	11	cv	$$setvarn$$
22	18	cv	$$setvary$$
23	19	cv	$$setvarz$$
24	22 23	cop	$$class⟨y,z⟩$$
25		c1o	$$class{1}_{𝑜}$$
26	25 23	cdif	$$class\left(1_{𝑜}\setminus z\right)$$
27	22 26	cop	$$class⟨y,1_{𝑜}\setminus z⟩$$
28	24 27	cs2	$$class⟨“⟨y,z⟩⟨y,1_{𝑜}\setminus z⟩”⟩$$
29	21 21 28	cotp	$$class⟨n,n,⟨“⟨y,z⟩⟨y,1_{𝑜}\setminus z⟩”⟩⟩$$
30	15 29 20	co	$$class\left(x\mathrm{splice}⟨n,n,⟨“⟨y,z⟩⟨y,1_{𝑜}\setminus z⟩”⟩⟩\right)$$
31	15 30 4	wbr	$$wffxr\left(x\mathrm{splice}⟨n,n,⟨“⟨y,z⟩⟨y,1_{𝑜}\setminus z⟩”⟩⟩\right)$$
32	31 19 6	wral	$$wff\forall z\in 2_{𝑜}xr\left(x\mathrm{splice}⟨n,n,⟨“⟨y,z⟩⟨y,1_{𝑜}\setminus z⟩”⟩⟩\right)$$
33	32 18 5	wral	$$wff\forall y\in i\forall z\in 2_{𝑜}xr\left(x\mathrm{splice}⟨n,n,⟨“⟨y,z⟩⟨y,1_{𝑜}\setminus z⟩”⟩⟩\right)$$
34	33 11 17	wral	$$wff\forall n\in \left(0\dots \left|x\right|\right)\forall y\in i\forall z\in 2_{𝑜}xr\left(x\mathrm{splice}⟨n,n,⟨“⟨y,z⟩⟨y,1_{𝑜}\setminus z⟩”⟩⟩\right)$$
35	34 10 8	wral	$$wff\forall x\in \mathrm{Word}\left(i\times 2_{𝑜}\right)\forall n\in \left(0\dots \left|x\right|\right)\forall y\in i\forall z\in 2_{𝑜}xr\left(x\mathrm{splice}⟨n,n,⟨“⟨y,z⟩⟨y,1_{𝑜}\setminus z⟩”⟩⟩\right)$$
36	9 35	wa	$$wff\left(r\mathrm{Er}\mathrm{Word}\left(i\times 2_{𝑜}\right)\wedge \forall x\in \mathrm{Word}\left(i\times 2_{𝑜}\right)\forall n\in \left(0\dots \left|x\right|\right)\forall y\in i\forall z\in 2_{𝑜}xr\left(x\mathrm{splice}⟨n,n,⟨“⟨y,z⟩⟨y,1_{𝑜}\setminus z⟩”⟩⟩\right)\right)$$
37	36 3	cab	$$class\left\{r|\left(r\mathrm{Er}\mathrm{Word}\left(i\times 2_{𝑜}\right)\wedge \forall x\in \mathrm{Word}\left(i\times 2_{𝑜}\right)\forall n\in \left(0\dots \left|x\right|\right)\forall y\in i\forall z\in 2_{𝑜}xr\left(x\mathrm{splice}⟨n,n,⟨“⟨y,z⟩⟨y,1_{𝑜}\setminus z⟩”⟩⟩\right)\right)\right\}$$
38	37	cint	$$class\bigcap \left\{r|\left(r\mathrm{Er}\mathrm{Word}\left(i\times 2_{𝑜}\right)\wedge \forall x\in \mathrm{Word}\left(i\times 2_{𝑜}\right)\forall n\in \left(0\dots \left|x\right|\right)\forall y\in i\forall z\in 2_{𝑜}xr\left(x\mathrm{splice}⟨n,n,⟨“⟨y,z⟩⟨y,1_{𝑜}\setminus z⟩”⟩⟩\right)\right)\right\}$$
39	1 2 38	cmpt	$$class\left(i\in \mathrm{V}⟼\bigcap \left\{r|\left(r\mathrm{Er}\mathrm{Word}\left(i\times 2_{𝑜}\right)\wedge \forall x\in \mathrm{Word}\left(i\times 2_{𝑜}\right)\forall n\in \left(0\dots \left|x\right|\right)\forall y\in i\forall z\in 2_{𝑜}xr\left(x\mathrm{splice}⟨n,n,⟨“⟨y,z⟩⟨y,1_{𝑜}\setminus z⟩”⟩⟩\right)\right)\right\}\right)$$
40	0 39	wceq	$$wff{~}_{\mathit{FG}}=\left(i\in \mathrm{V}⟼\bigcap \left\{r|\left(r\mathrm{Er}\mathrm{Word}\left(i\times 2_{𝑜}\right)\wedge \forall x\in \mathrm{Word}\left(i\times 2_{𝑜}\right)\forall n\in \left(0\dots \left|x\right|\right)\forall y\in i\forall z\in 2_{𝑜}xr\left(x\mathrm{splice}⟨n,n,⟨“⟨y,z⟩⟨y,1_{𝑜}\setminus z⟩”⟩⟩\right)\right)\right\}\right)$$