Definition df-efg 17945

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 (𝑖 × 2𝑜) ∧ ∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜 ∖ 𝑧)⟩”⟩⟩))})

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

Detailed syntax breakdown of Definition df-efg

Step	Hyp	Ref	Expression
1		cefg 17942	. 2 class ~FG
2		vi	. . 3 setvar 𝑖
3		cvv 3173	. . 3 class V
4	2	cv 1474	. . . . . . . . 9 class 𝑖
5		c2o 7441	. . . . . . . . 9 class 2𝑜
6	4, 5	cxp 5036	. . . . . . . 8 class (𝑖 × 2𝑜)
7	6	cword 13146	. . . . . . 7 class Word (𝑖 × 2𝑜)
8		vr	. . . . . . . 8 setvar 𝑟
9	8	cv 1474	. . . . . . 7 class 𝑟
10	7, 9	wer 7626	. . . . . 6 wff 𝑟 Er Word (𝑖 × 2𝑜)
11		vx	. . . . . . . . . . . 12 setvar 𝑥
12	11	cv 1474	. . . . . . . . . . 11 class 𝑥
13		vn	. . . . . . . . . . . . . 14 setvar 𝑛
14	13	cv 1474	. . . . . . . . . . . . 13 class 𝑛
15		vy	. . . . . . . . . . . . . . . 16 setvar 𝑦
16	15	cv 1474	. . . . . . . . . . . . . . 15 class 𝑦
17		vz	. . . . . . . . . . . . . . . 16 setvar 𝑧
18	17	cv 1474	. . . . . . . . . . . . . . 15 class 𝑧
19	16, 18	cop 4131	. . . . . . . . . . . . . 14 class ⟨𝑦, 𝑧⟩
20		c1o 7440	. . . . . . . . . . . . . . . 16 class 1𝑜
21	20, 18	cdif 3537	. . . . . . . . . . . . . . 15 class (1𝑜 ∖ 𝑧)
22	16, 21	cop 4131	. . . . . . . . . . . . . 14 class ⟨𝑦, (1𝑜 ∖ 𝑧)⟩
23	19, 22	cs2 13437	. . . . . . . . . . . . 13 class ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜 ∖ 𝑧)⟩”⟩
24	14, 14, 23	cotp 4133	. . . . . . . . . . . 12 class ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜 ∖ 𝑧)⟩”⟩⟩
25		csplice 13151	. . . . . . . . . . . 12 class splice
26	12, 24, 25	co 6549	. . . . . . . . . . 11 class (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜 ∖ 𝑧)⟩”⟩⟩)
27	12, 26, 9	wbr 4583	. . . . . . . . . 10 wff 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜 ∖ 𝑧)⟩”⟩⟩)
28	27, 17, 5	wral 2896	. . . . . . . . 9 wff ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜 ∖ 𝑧)⟩”⟩⟩)
29	28, 15, 4	wral 2896	. . . . . . . 8 wff ∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜 ∖ 𝑧)⟩”⟩⟩)
30		cc0 9815	. . . . . . . . 9 class 0
31		chash 12979	. . . . . . . . . 10 class #
32	12, 31	cfv 5804	. . . . . . . . 9 class (#‘𝑥)
33		cfz 12197	. . . . . . . . 9 class ...
34	30, 32, 33	co 6549	. . . . . . . 8 class (0...(#‘𝑥))
35	29, 13, 34	wral 2896	. . . . . . 7 wff ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜 ∖ 𝑧)⟩”⟩⟩)
36	35, 11, 7	wral 2896	. . . . . 6 wff ∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜 ∖ 𝑧)⟩”⟩⟩)
37	10, 36	wa 383	. . . . 5 wff (𝑟 Er Word (𝑖 × 2𝑜) ∧ ∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜 ∖ 𝑧)⟩”⟩⟩))
38	37, 8	cab 2596	. . . 4 class {𝑟 ∣ (𝑟 Er Word (𝑖 × 2𝑜) ∧ ∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜 ∖ 𝑧)⟩”⟩⟩))}
39	38	cint 4410	. . 3 class ∩ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2𝑜) ∧ ∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜 ∖ 𝑧)⟩”⟩⟩))}
40	2, 3, 39	cmpt 4643	. 2 class (𝑖 ∈ V ↦ ∩ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2𝑜) ∧ ∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜 ∖ 𝑧)⟩”⟩⟩))})
41	1, 40	wceq 1475	1 wff ~FG = (𝑖 ∈ V ↦ ∩ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2𝑜) ∧ ∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜 ∖ 𝑧)⟩”⟩⟩))})

This definition is referenced by:  efgval  17953