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 18827
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 (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦𝑖𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o𝑧)⟩”⟩⟩))})
Distinct variable group:   𝑖,𝑛,𝑟,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-efg
StepHypRef Expression
1 cefg 18824 . 2 class ~FG
2 vi . . 3 setvar 𝑖
3 cvv 3493 . . 3 class V
42cv 1529 . . . . . . . . 9 class 𝑖
5 c2o 8088 . . . . . . . . 9 class 2o
64, 5cxp 5546 . . . . . . . 8 class (𝑖 × 2o)
76cword 13853 . . . . . . 7 class Word (𝑖 × 2o)
8 vr . . . . . . . 8 setvar 𝑟
98cv 1529 . . . . . . 7 class 𝑟
107, 9wer 8278 . . . . . 6 wff 𝑟 Er Word (𝑖 × 2o)
11 vx . . . . . . . . . . . 12 setvar 𝑥
1211cv 1529 . . . . . . . . . . 11 class 𝑥
13 vn . . . . . . . . . . . . . 14 setvar 𝑛
1413cv 1529 . . . . . . . . . . . . 13 class 𝑛
15 vy . . . . . . . . . . . . . . . 16 setvar 𝑦
1615cv 1529 . . . . . . . . . . . . . . 15 class 𝑦
17 vz . . . . . . . . . . . . . . . 16 setvar 𝑧
1817cv 1529 . . . . . . . . . . . . . . 15 class 𝑧
1916, 18cop 4565 . . . . . . . . . . . . . 14 class 𝑦, 𝑧
20 c1o 8087 . . . . . . . . . . . . . . . 16 class 1o
2120, 18cdif 3931 . . . . . . . . . . . . . . 15 class (1o𝑧)
2216, 21cop 4565 . . . . . . . . . . . . . 14 class 𝑦, (1o𝑧)⟩
2319, 22cs2 14195 . . . . . . . . . . . . 13 class ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o𝑧)⟩”⟩
2414, 14, 23cotp 4567 . . . . . . . . . . . 12 class 𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o𝑧)⟩”⟩⟩
25 csplice 14103 . . . . . . . . . . . 12 class splice
2612, 24, 25co 7148 . . . . . . . . . . 11 class (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o𝑧)⟩”⟩⟩)
2712, 26, 9wbr 5057 . . . . . . . . . 10 wff 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o𝑧)⟩”⟩⟩)
2827, 17, 5wral 3136 . . . . . . . . 9 wff 𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o𝑧)⟩”⟩⟩)
2928, 15, 4wral 3136 . . . . . . . 8 wff 𝑦𝑖𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o𝑧)⟩”⟩⟩)
30 cc0 10529 . . . . . . . . 9 class 0
31 chash 13682 . . . . . . . . . 10 class
3212, 31cfv 6348 . . . . . . . . 9 class (♯‘𝑥)
33 cfz 12884 . . . . . . . . 9 class ...
3430, 32, 33co 7148 . . . . . . . 8 class (0...(♯‘𝑥))
3529, 13, 34wral 3136 . . . . . . 7 wff 𝑛 ∈ (0...(♯‘𝑥))∀𝑦𝑖𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o𝑧)⟩”⟩⟩)
3635, 11, 7wral 3136 . . . . . 6 wff 𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦𝑖𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o𝑧)⟩”⟩⟩)
3710, 36wa 398 . . . . 5 wff (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦𝑖𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o𝑧)⟩”⟩⟩))
3837, 8cab 2797 . . . 4 class {𝑟 ∣ (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦𝑖𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o𝑧)⟩”⟩⟩))}
3938cint 4867 . . 3 class {𝑟 ∣ (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦𝑖𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o𝑧)⟩”⟩⟩))}
402, 3, 39cmpt 5137 . 2 class (𝑖 ∈ V ↦ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦𝑖𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o𝑧)⟩”⟩⟩))})
411, 40wceq 1530 1 wff ~FG = (𝑖 ∈ V ↦ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦𝑖𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o𝑧)⟩”⟩⟩))})
Colors of variables: wff setvar class
This definition is referenced by:  efgval  18835
  Copyright terms: Public domain W3C validator