This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ass

Description: A device to add associativity to various sorts of internal operations. The definition is meaningful when g is a magma at least. (Contributed by FL, 1-Nov-2009) (New usage is discouraged.)

Ref Expression
Assertion df-ass Ass = { 𝑔 ∣ ∀ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ∀ 𝑧 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cass ⊢ Ass
1 vg ⊢ 𝑔
2 vx ⊢ 𝑥
3 1 cv ⊢ 𝑔
4 3 cdm ⊢ dom 𝑔
5 4 cdm ⊢ dom dom 𝑔
6 vy ⊢ 𝑦
7 vz ⊢ 𝑧
8 2 cv ⊢ 𝑥
9 6 cv ⊢ 𝑦
10 8 9 3 co ⊢ ( 𝑥 𝑔 𝑦 )
11 7 cv ⊢ 𝑧
12 10 11 3 co ⊢ ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 )
13 9 11 3 co ⊢ ( 𝑦 𝑔 𝑧 )
14 8 13 3 co ⊢ ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) )
15 12 14 wceq ⊢ ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) )
16 15 7 5 wral ⊢ ∀ 𝑧 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) )
17 16 6 5 wral ⊢ ∀ 𝑦 ∈ dom dom 𝑔 ∀ 𝑧 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) )
18 17 2 5 wral ⊢ ∀ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ∀ 𝑧 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) )
19 18 1 cab ⊢ { 𝑔 ∣ ∀ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ∀ 𝑧 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) }
20 0 19 wceq ⊢ Ass = { 𝑔 ∣ ∀ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ∀ 𝑧 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) }