Definition df-efg 15296

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 inv g x, A B ~~ A x ( inv g 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 15293	. 2 class ~FG
2		vi	. . 3 set i
3		cvv 2916	. . 3 class _V
4	2	cv 1648	. . . . . . . . 9 class i
5		c2o 6677	. . . . . . . . 9 class 2o
6	4, 5	cxp 4835	. . . . . . . 8 class ( i X. 2o )
7	6	cword 11672	. . . . . . 7 class Word ( i X. 2o )
8		vr	. . . . . . . 8 set r
9	8	cv 1648	. . . . . . 7 class r
10	7, 9	wer 6861	. . . . . 6 wff r Er Word ( i X. 2o )
11		vx	. . . . . . . . . . . 12 set x
12	11	cv 1648	. . . . . . . . . . 11 class x
13		vn	. . . . . . . . . . . . . 14 set n
14	13	cv 1648	. . . . . . . . . . . . 13 class n
15		vy	. . . . . . . . . . . . . . . 16 set y
16	15	cv 1648	. . . . . . . . . . . . . . 15 class y
17		vz	. . . . . . . . . . . . . . . 16 set z
18	17	cv 1648	. . . . . . . . . . . . . . 15 class z
19	16, 18	cop 3777	. . . . . . . . . . . . . 14 class <. y , z >.
20		c1o 6676	. . . . . . . . . . . . . . . 16 class 1o
21	20, 18	cdif 3277	. . . . . . . . . . . . . . 15 class ( 1o \ z )
22	16, 21	cop 3777	. . . . . . . . . . . . . 14 class <. y , ( 1o \ z ) >.
23	19, 22	cs2 11760	. . . . . . . . . . . . 13 class <" <. y , z >. <. y , ( 1o \ z ) >. ">
24	14, 14, 23	cotp 3778	. . . . . . . . . . . 12 class <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >.
25		csplice 11676	. . . . . . . . . . . 12 class splice
26	12, 24, 25	co 6040	. . . . . . . . . . 11 class ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. )
27	12, 26, 9	wbr 4172	. . . . . . . . . 10 wff x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. )
28	27, 17, 5	wral 2666	. . . . . . . . 9 wff A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. )
29	28, 15, 4	wral 2666	. . . . . . . 8 wff A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. )
30		cc0 8946	. . . . . . . . 9 class 0
31		chash 11573	. . . . . . . . . 10 class #
32	12, 31	cfv 5413	. . . . . . . . 9 class ( # ` x )
33		cfz 10999	. . . . . . . . 9 class ...
34	30, 32, 33	co 6040	. . . . . . . 8 class ( 0 ... ( # ` x ) )
35	29, 13, 34	wral 2666	. . . . . . 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 2666	. . . . . 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 359	. . . . 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 2390	. . . 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 4010	. . 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 4226	. 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 1649	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  15304