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 𝑔 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) }