Theorem cntzcmnss

Description: Any subset in a commutative monoid is a subset of its centralizer. (Contributed by AV, 12-Jan-2019)

	Ref	Expression
Hypotheses	cntzcmnss.b	|- B = ( Base ` G )
	cntzcmnss.z	|- Z = ( Cntz ` G )
Assertion	cntzcmnss	|- ( ( G e. CMnd /\ S C_ B ) -> S C_ ( Z ` S ) )

Proof

Step	Hyp	Ref	Expression
1		cntzcmnss.b	|- B = ( Base ` G )
2		cntzcmnss.z	|- Z = ( Cntz ` G )
3	1 2	cntzcmn	|- ( ( G e. CMnd /\ S C_ B ) -> ( Z ` S ) = B )
4		sseq2	|- ( B = ( Z ` S ) -> ( S C_ B <-> S C_ ( Z ` S ) ) )
5	4	eqcoms	|- ( ( Z ` S ) = B -> ( S C_ B <-> S C_ ( Z ` S ) ) )
6	5	biimpd	|- ( ( Z ` S ) = B -> ( S C_ B -> S C_ ( Z ` S ) ) )
7	6	adantld	|- ( ( Z ` S ) = B -> ( ( G e. CMnd /\ S C_ B ) -> S C_ ( Z ` S ) ) )
8	3 7	mpcom	|- ( ( G e. CMnd /\ S C_ B ) -> S C_ ( Z ` S ) )