This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mndcl

Description: Closure of the operation of a monoid. (Contributed by NM, 14-Aug-2011) (Revised by Mario Carneiro, 6-Jan-2015) (Proof shortened by AV, 8-Feb-2020)

	Ref	Expression
Hypotheses	mndcl.b	$⊢ B = {Base}_{G}$
	mndcl.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	mndcl	$⊢ (G \in Mnd \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$

Proof

Step	Hyp	Ref	Expression
1		mndcl.b	$⊢ B = {Base}_{G}$
2		mndcl.p	$⊢ \underset{˙}{+} = +_{G}$
3		mndmgm	$⊢ G \in Mnd \to G \in Mgm$
4	1 2	mgmcl	$⊢ (G \in Mgm \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$
5	3 4	syl3an1	$⊢ (G \in Mnd \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$