Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ass Structured version   Visualization version   GIF version

Definition df-ass 35624
Description: A device to add associativity to various sorts of internal operations. The definition is meaningful when 𝑔 is a magma at least. (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.)
Assertion
Ref Expression
df-ass Ass = {𝑔 ∣ ∀𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))}
Distinct variable group:   𝑥,𝑔,𝑦,𝑧

Detailed syntax breakdown of Definition df-ass
StepHypRef Expression
1 cass 35623 . 2 class Ass
2 vx . . . . . . . . . 10 setvar 𝑥
32cv 1541 . . . . . . . . 9 class 𝑥
4 vy . . . . . . . . . 10 setvar 𝑦
54cv 1541 . . . . . . . . 9 class 𝑦
6 vg . . . . . . . . . 10 setvar 𝑔
76cv 1541 . . . . . . . . 9 class 𝑔
83, 5, 7co 7170 . . . . . . . 8 class (𝑥𝑔𝑦)
9 vz . . . . . . . . 9 setvar 𝑧
109cv 1541 . . . . . . . 8 class 𝑧
118, 10, 7co 7170 . . . . . . 7 class ((𝑥𝑔𝑦)𝑔𝑧)
125, 10, 7co 7170 . . . . . . . 8 class (𝑦𝑔𝑧)
133, 12, 7co 7170 . . . . . . 7 class (𝑥𝑔(𝑦𝑔𝑧))
1411, 13wceq 1542 . . . . . 6 wff ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))
157cdm 5525 . . . . . . 7 class dom 𝑔
1615cdm 5525 . . . . . 6 class dom dom 𝑔
1714, 9, 16wral 3053 . . . . 5 wff 𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))
1817, 4, 16wral 3053 . . . 4 wff 𝑦 ∈ dom dom 𝑔𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))
1918, 2, 16wral 3053 . . 3 wff 𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))
2019, 6cab 2716 . 2 class {𝑔 ∣ ∀𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))}
211, 20wceq 1542 1 wff Ass = {𝑔 ∣ ∀𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))}
Colors of variables: wff setvar class
This definition is referenced by:  isass  35627
  Copyright terms: Public domain W3C validator