Definition df-efg 19700

Description: Define the free group equivalence relation, which is the smallest equivalence relation ≈ such that for any words 𝐴, 𝐵 and formal symbol 𝑥 with inverse inv_g𝑥, 𝐴𝐵 ≈ 𝐴𝑥(inv_g𝑥)𝐵. (Contributed by Mario Carneiro, 1-Oct-2015.)

Assertion

Ref	Expression
df-efg	⊢ ~FG = (𝑖 ∈ V ↦ ∩ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))})

Distinct variable group:   𝑖,𝑛,𝑟,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-efg

Step	Hyp	Ref	Expression
1		cefg 19697	. 2 class ~FG
2		vi	. . 3 setvar 𝑖
3		cvv 3464	. . 3 class V
4	2	cv 1538	. . . . . . . . 9 class 𝑖
5		c2o 8483	. . . . . . . . 9 class 2o
6	4, 5	cxp 5665	. . . . . . . 8 class (𝑖 × 2o)
7	6	cword 14535	. . . . . . 7 class Word (𝑖 × 2o)
8		vr	. . . . . . . 8 setvar 𝑟
9	8	cv 1538	. . . . . . 7 class 𝑟
10	7, 9	wer 8725	. . . . . 6 wff 𝑟 Er Word (𝑖 × 2o)
11		vx	. . . . . . . . . . . 12 setvar 𝑥
12	11	cv 1538	. . . . . . . . . . 11 class 𝑥
13		vn	. . . . . . . . . . . . . 14 setvar 𝑛
14	13	cv 1538	. . . . . . . . . . . . 13 class 𝑛
15		vy	. . . . . . . . . . . . . . . 16 setvar 𝑦
16	15	cv 1538	. . . . . . . . . . . . . . 15 class 𝑦
17		vz	. . . . . . . . . . . . . . . 16 setvar 𝑧
18	17	cv 1538	. . . . . . . . . . . . . . 15 class 𝑧
19	16, 18	cop 4614	. . . . . . . . . . . . . 14 class ⟨𝑦, 𝑧⟩
20		c1o 8482	. . . . . . . . . . . . . . . 16 class 1o
21	20, 18	cdif 3930	. . . . . . . . . . . . . . 15 class (1o ∖ 𝑧)
22	16, 21	cop 4614	. . . . . . . . . . . . . 14 class ⟨𝑦, (1o ∖ 𝑧)⟩
23	19, 22	cs2 14863	. . . . . . . . . . . . 13 class ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩
24	14, 14, 23	cotp 4616	. . . . . . . . . . . 12 class ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩
25		csplice 14770	. . . . . . . . . . . 12 class splice
26	12, 24, 25	co 7414	. . . . . . . . . . 11 class (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩)
27	12, 26, 9	wbr 5125	. . . . . . . . . 10 wff 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩)
28	27, 17, 5	wral 3050	. . . . . . . . 9 wff ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩)
29	28, 15, 4	wral 3050	. . . . . . . 8 wff ∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩)
30		cc0 11138	. . . . . . . . 9 class 0
31		chash 14352	. . . . . . . . . 10 class ♯
32	12, 31	cfv 6542	. . . . . . . . 9 class (♯‘𝑥)
33		cfz 13530	. . . . . . . . 9 class ...
34	30, 32, 33	co 7414	. . . . . . . 8 class (0...(♯‘𝑥))
35	29, 13, 34	wral 3050	. . . . . . 7 wff ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩)
36	35, 11, 7	wral 3050	. . . . . 6 wff ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩)
37	10, 36	wa 395	. . . . 5 wff (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))
38	37, 8	cab 2712	. . . 4 class {𝑟 ∣ (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))}
39	38	cint 4928	. . 3 class ∩ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))}
40	2, 3, 39	cmpt 5207	. 2 class (𝑖 ∈ V ↦ ∩ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))})
41	1, 40	wceq 1539	1 wff ~FG = (𝑖 ∈ V ↦ ∩ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))})

This definition is referenced by:  efgval  19708