Definition df-cntr

Description: Define thecenter of a magma, which is the elements that commute with all others. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Assertion	df-cntr	⊢ Cntr = ( 𝑚 ∈ V ↦ ( ( Cntz ‘ 𝑚 ) ‘ ( Base ‘ 𝑚 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccntr	⊢ Cntr
1		vm	⊢ 𝑚
2		cvv	⊢ V
3		ccntz	⊢ Cntz
4	1	cv	⊢ 𝑚
5	4 3	cfv	⊢ ( Cntz ‘ 𝑚 )
6		cbs	⊢ Base
7	4 6	cfv	⊢ ( Base ‘ 𝑚 )
8	7 5	cfv	⊢ ( ( Cntz ‘ 𝑚 ) ‘ ( Base ‘ 𝑚 ) )
9	1 2 8	cmpt	⊢ ( 𝑚 ∈ V ↦ ( ( Cntz ‘ 𝑚 ) ‘ ( Base ‘ 𝑚 ) ) )
10	0 9	wceq	⊢ Cntr = ( 𝑚 ∈ V ↦ ( ( Cntz ‘ 𝑚 ) ‘ ( Base ‘ 𝑚 ) ) )