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 18043
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 18040 . 2 class ~FG
2 vi . . 3 setvar 𝑖
3 cvv 3186 . . 3 class V
42cv 1479 . . . . . . . . 9 class 𝑖
5 c2o 7499 . . . . . . . . 9 class 2𝑜
64, 5cxp 5072 . . . . . . . 8 class (𝑖 × 2𝑜)
76cword 13230 . . . . . . 7 class Word (𝑖 × 2𝑜)
8 vr . . . . . . . 8 setvar 𝑟
98cv 1479 . . . . . . 7 class 𝑟
107, 9wer 7684 . . . . . 6 wff 𝑟 Er Word (𝑖 × 2𝑜)
11 vx . . . . . . . . . . . 12 setvar 𝑥
1211cv 1479 . . . . . . . . . . 11 class 𝑥
13 vn . . . . . . . . . . . . . 14 setvar 𝑛
1413cv 1479 . . . . . . . . . . . . 13 class 𝑛
15 vy . . . . . . . . . . . . . . . 16 setvar 𝑦
1615cv 1479 . . . . . . . . . . . . . . 15 class 𝑦
17 vz . . . . . . . . . . . . . . . 16 setvar 𝑧
1817cv 1479 . . . . . . . . . . . . . . 15 class 𝑧
1916, 18cop 4154 . . . . . . . . . . . . . 14 class 𝑦, 𝑧
20 c1o 7498 . . . . . . . . . . . . . . . 16 class 1𝑜
2120, 18cdif 3552 . . . . . . . . . . . . . . 15 class (1𝑜𝑧)
2216, 21cop 4154 . . . . . . . . . . . . . 14 class 𝑦, (1𝑜𝑧)⟩
2319, 22cs2 13523 . . . . . . . . . . . . 13 class ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩
2414, 14, 23cotp 4156 . . . . . . . . . . . 12 class 𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩
25 csplice 13235 . . . . . . . . . . . 12 class splice
2612, 24, 25co 6604 . . . . . . . . . . 11 class (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩)
2712, 26, 9wbr 4613 . . . . . . . . . 10 wff 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩)
2827, 17, 5wral 2907 . . . . . . . . 9 wff 𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩)
2928, 15, 4wral 2907 . . . . . . . 8 wff 𝑦𝑖𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩)
30 cc0 9880 . . . . . . . . 9 class 0
31 chash 13057 . . . . . . . . . 10 class #
3212, 31cfv 5847 . . . . . . . . 9 class (#‘𝑥)
33 cfz 12268 . . . . . . . . 9 class ...
3430, 32, 33co 6604 . . . . . . . 8 class (0...(#‘𝑥))
3529, 13, 34wral 2907 . . . . . . 7 wff 𝑛 ∈ (0...(#‘𝑥))∀𝑦𝑖𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩)
3635, 11, 7wral 2907 . . . . . 6 wff 𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦𝑖𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩)
3710, 36wa 384 . . . . 5 wff (𝑟 Er Word (𝑖 × 2𝑜) ∧ ∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦𝑖𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩))
3837, 8cab 2607 . . . 4 class {𝑟 ∣ (𝑟 Er Word (𝑖 × 2𝑜) ∧ ∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦𝑖𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩))}
3938cint 4440 . . 3 class {𝑟 ∣ (𝑟 Er Word (𝑖 × 2𝑜) ∧ ∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦𝑖𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩))}
402, 3, 39cmpt 4673 . 2 class (𝑖 ∈ V ↦ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2𝑜) ∧ ∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦𝑖𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1𝑜𝑧)⟩”⟩⟩))})
411, 40wceq 1480 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  18051
  Copyright terms: Public domain W3C validator