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 \in CMnd \land S \subseteq B) \to S \subseteq Z (S)$

Step	Hyp	Ref	Expression
1		cntzcmnss.b	$⊢ B = {Base}_{G}$
2		cntzcmnss.z	$⊢ Z = Cntz (G)$
3	1 2	cntzcmn	$⊢ (G \in CMnd \land S \subseteq B) \to Z (S) = B$
4		sseq2	$⊢ B = Z (S) \to (S \subseteq B \leftrightarrow S \subseteq Z (S))$
5	4	eqcoms	$⊢ Z (S) = B \to (S \subseteq B \leftrightarrow S \subseteq Z (S))$
6	5	biimpd	$⊢ Z (S) = B \to (S \subseteq B \to S \subseteq Z (S))$
7	6	adantld	$⊢ Z (S) = B \to ((G \in CMnd \land S \subseteq B) \to S \subseteq Z (S))$
8	3 7	mpcom	$⊢ (G \in CMnd \land S \subseteq B) \to S \subseteq Z (S)$

Metamath Proof Explorer