Theorem elcntzsn

Description: Value of the centralizer of a singleton. (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypotheses	cntzfval.b	$$⊢B={\mathrm{Base}}_M$$
	cntzfval.p	$$⊢\underset{\dot{}}{+}={+}_M$$
	cntzfval.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
Assertion	elcntzsn	$$⊢Y\in B\to \left(X\in Z\left(\left\{Y\right\}\right)\leftrightarrow \left(X\in B\wedge X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cntzfval.b	$$⊢B={\mathrm{Base}}_M$$
2		cntzfval.p	$$⊢\underset{\dot{}}{+}={+}_M$$
3		cntzfval.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
4	1 2 3	cntzsnval	$$⊢Y\in B\to Z\left(\left\{Y\right\}\right)=\left\{x\in B|x\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}x\right\}$$
5	4	eleq2d	$$⊢Y\in B\to \left(X\in Z\left(\left\{Y\right\}\right)\leftrightarrow X\in \left\{x\in B|x\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}x\right\}\right)$$
6		oveq1	$$⊢x=X\to x\underset{\dot{}}{+}Y=X\underset{\dot{}}{+}Y$$
7		oveq2	$$⊢x=X\to Y\underset{\dot{}}{+}x=Y\underset{\dot{}}{+}X$$
8	6 7	eqeq12d	$$⊢x=X\to \left(x\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}x\leftrightarrow X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\right)$$
9	8	elrab	$$⊢X\in \left\{x\in B|x\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}x\right\}\leftrightarrow \left(X\in B\wedge X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\right)$$
10	5 9	bitrdi	$$⊢Y\in B\to \left(X\in Z\left(\left\{Y\right\}\right)\leftrightarrow \left(X\in B\wedge X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\right)\right)$$