Metamath Proof Explorer


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=BaseG
cntzcmnss.z Z=CntzG
Assertion cntzcmnss GCMndSBSZS

Proof

Step Hyp Ref Expression
1 cntzcmnss.b B=BaseG
2 cntzcmnss.z Z=CntzG
3 1 2 cntzcmn GCMndSBZS=B
4 sseq2 B=ZSSBSZS
5 4 eqcoms ZS=BSBSZS
6 5 biimpd ZS=BSBSZS
7 6 adantld ZS=BGCMndSBSZS
8 3 7 mpcom GCMndSBSZS