Definition df-efg 17051

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.)

Assertion

Ref	Expression
df-efg	|- ~FG = ( i e. _V |-> |^| { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } )

Distinct variable group:   i, n, r, x, y, z

Detailed syntax breakdown of Definition df-efg

Step	Hyp	Ref	Expression
1		cefg 17048	. 2 class ~FG
2		vi	. . 3 setvar i
3		cvv 3059	. . 3 class _V
4	2	cv 1404	. . . . . . . . 9 class i
5		c2o 7161	. . . . . . . . 9 class 2o
6	4, 5	cxp 4821	. . . . . . . 8 class ( i X. 2o )
7	6	cword 12583	. . . . . . 7 class Word ( i X. 2o )
8		vr	. . . . . . . 8 setvar r
9	8	cv 1404	. . . . . . 7 class r
10	7, 9	wer 7345	. . . . . 6 wff r Er Word ( i X. 2o )
11		vx	. . . . . . . . . . . 12 setvar x
12	11	cv 1404	. . . . . . . . . . 11 class x
13		vn	. . . . . . . . . . . . . 14 setvar n
14	13	cv 1404	. . . . . . . . . . . . 13 class n
15		vy	. . . . . . . . . . . . . . . 16 setvar y
16	15	cv 1404	. . . . . . . . . . . . . . 15 class y
17		vz	. . . . . . . . . . . . . . . 16 setvar z
18	17	cv 1404	. . . . . . . . . . . . . . 15 class z
19	16, 18	cop 3978	. . . . . . . . . . . . . 14 class <. y , z >.
20		c1o 7160	. . . . . . . . . . . . . . . 16 class 1o
21	20, 18	cdif 3411	. . . . . . . . . . . . . . 15 class ( 1o \ z )
22	16, 21	cop 3978	. . . . . . . . . . . . . 14 class <. y , ( 1o \ z ) >.
23	19, 22	cs2 12862	. . . . . . . . . . . . 13 class <" <. y , z >. <. y , ( 1o \ z ) >. ">
24	14, 14, 23	cotp 3980	. . . . . . . . . . . 12 class <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >.
25		csplice 12588	. . . . . . . . . . . 12 class splice
26	12, 24, 25	co 6278	. . . . . . . . . . 11 class ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. )
27	12, 26, 9	wbr 4395	. . . . . . . . . 10 wff x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. )
28	27, 17, 5	wral 2754	. . . . . . . . 9 wff A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. )
29	28, 15, 4	wral 2754	. . . . . . . 8 wff A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. )
30		cc0 9522	. . . . . . . . 9 class 0
31		chash 12452	. . . . . . . . . 10 class #
32	12, 31	cfv 5569	. . . . . . . . 9 class ( # ` x )
33		cfz 11726	. . . . . . . . 9 class ...
34	30, 32, 33	co 6278	. . . . . . . 8 class ( 0 ... ( # ` x ) )
35	29, 13, 34	wral 2754	. . . . . . 7 wff A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. )
36	35, 11, 7	wral 2754	. . . . . 6 wff A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. )
37	10, 36	wa 367	. . . . 5 wff ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) )
38	37, 8	cab 2387	. . . 4 class { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) }
39	38	cint 4227	. . 3 class |^| { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) }
40	2, 3, 39	cmpt 4453	. 2 class ( i e. _V |-> |^| { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } )
41	1, 40	wceq 1405	1 wff ~FG = ( i e. _V |-> |^| { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } )

This definition is referenced by:  efgval  17059