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	$$⊢\mathrm{Cntr}=\left(m\in \mathrm{V}⟼\mathrm{Cntz}\left(m\right)\left({\mathrm{Base}}_m\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccntr	$$class\mathrm{Cntr}$$
1		vm	$$setvarm$$
2		cvv	$$class\mathrm{V}$$
3		ccntz	$$class\mathrm{Cntz}$$
4	1	cv	$$setvarm$$
5	4 3	cfv	$$class\mathrm{Cntz}\left(m\right)$$
6		cbs	$$class\mathrm{Base}$$
7	4 6	cfv	$$class{\mathrm{Base}}_m$$
8	7 5	cfv	$$class\mathrm{Cntz}\left(m\right)\left({\mathrm{Base}}_m\right)$$
9	1 2 8	cmpt	$$class\left(m\in \mathrm{V}⟼\mathrm{Cntz}\left(m\right)\left({\mathrm{Base}}_m\right)\right)$$
10	0 9	wceq	$$wff\mathrm{Cntr}=\left(m\in \mathrm{V}⟼\mathrm{Cntz}\left(m\right)\left({\mathrm{Base}}_m\right)\right)$$