MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-efg Structured version   Visualization version   GIF version

Definition df-efg 18322
Description: Define the free group equivalence relation, which is the smallest equivalence relation such that for any words 𝐴, 𝐵 and formal symbol 𝑥 with inverse invg𝑥, 𝐴𝐵𝐴𝑥(invg𝑥)𝐵. (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
StepHypRef Expression
1 cefg 18319 . 2 class ~FG
2 vi . . 3 setvar 𝑖
3 cvv 3351 . . 3 class V
42cv 1630 . . . . . . . . 9 class 𝑖
5 c2o 7705 . . . . . . . . 9 class 2𝑜
64, 5cxp 5247 . . . . . . . 8 class (𝑖 × 2𝑜)
76cword 13480 . . . . . . 7 class Word (𝑖 × 2𝑜)
8 vr . . . . . . . 8 setvar 𝑟
98cv 1630 . . . . . . 7 class 𝑟
107, 9wer 7891 . . . . . 6 wff 𝑟 Er Word (𝑖 × 2𝑜)
11 vx . . . . . . . . . . . 12 setvar 𝑥
1211cv 1630 . . . . . . . . . . 11 class 𝑥
13 vn . . . . . . . . . . . . . 14 setvar 𝑛
1413cv 1630 . . . . . . . . . . . . 13 class 𝑛
15 vy . . . . . . . . . . . . . . . 16 setvar 𝑦
1615cv 1630 . . . . . . . . . . . . . . 15 class 𝑦
17 vz . . . . . . . . . . . . . . . 16 setvar 𝑧
1817cv 1630 . . . . . . . . . . . . . . 15 class 𝑧
1916, 18cop 4322 . . . . . . . . . . . . . 14 class 𝑦, 𝑧
20 c1o 7704 . . . . . . . . . . . . . . . 16 class 1𝑜
2120, 18cdif 3720 . . . . . . . . . . . . . . 15 class (1𝑜𝑧)
2216, 21cop 4322 . . . . . . . . . . . . . 14 class 𝑦, (1𝑜𝑧)⟩
2319, 22cs2 13788 . . . . . . . . . . . . 13 class ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩
2414, 14, 23cotp 4324 . . . . . . . . . . . 12 class 𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩
25 csplice 13485 . . . . . . . . . . . 12 class splice
2612, 24, 25co 6791 . . . . . . . . . . 11 class (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩)
2712, 26, 9wbr 4786 . . . . . . . . . 10 wff 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩)
2827, 17, 5wral 3061 . . . . . . . . 9 wff 𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩)
2928, 15, 4wral 3061 . . . . . . . 8 wff 𝑦𝑖𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩)
30 cc0 10136 . . . . . . . . 9 class 0
31 chash 13314 . . . . . . . . . 10 class
3212, 31cfv 6029 . . . . . . . . 9 class (♯‘𝑥)
33 cfz 12526 . . . . . . . . 9 class ...
3430, 32, 33co 6791 . . . . . . . 8 class (0...(♯‘𝑥))
3529, 13, 34wral 3061 . . . . . . 7 wff 𝑛 ∈ (0...(♯‘𝑥))∀𝑦𝑖𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩)
3635, 11, 7wral 3061 . . . . . 6 wff 𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦𝑖𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩)
3710, 36wa 382 . . . . 5 wff (𝑟 Er Word (𝑖 × 2𝑜) ∧ ∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦𝑖𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩))
3837, 8cab 2757 . . . 4 class {𝑟 ∣ (𝑟 Er Word (𝑖 × 2𝑜) ∧ ∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦𝑖𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩))}
3938cint 4611 . . 3 class {𝑟 ∣ (𝑟 Er Word (𝑖 × 2𝑜) ∧ ∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦𝑖𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩))}
402, 3, 39cmpt 4863 . 2 class (𝑖 ∈ V ↦ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2𝑜) ∧ ∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦𝑖𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩))})
411, 40wceq 1631 1 wff ~FG = (𝑖 ∈ V ↦ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2𝑜) ∧ ∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦𝑖𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩))})
Colors of variables: wff setvar class
This definition is referenced by:  efgval  18330
  Copyright terms: Public domain W3C validator