Theorem mndcld

Description: Closure of the operation of a monoid. (Contributed by Thierry Arnoux, 3-Aug-2025)

	Ref	Expression
Hypotheses	mndcld.1	$$⊢B={\mathrm{Base}}_G$$
	mndcld.2	$$⊢\underset{\dot{}}{+}={+}_G$$
	mndcld.3	$$⊢\phi \to G\in \mathrm{Mnd}$$
	mndcld.4	$$⊢\phi \to X\in B$$
	mndcld.5	$$⊢\phi \to Y\in B$$
Assertion	mndcld	$$⊢\phi \to X\underset{\dot{}}{+}Y\in B$$

Proof

Step	Hyp	Ref	Expression
1		mndcld.1	$$⊢B={\mathrm{Base}}_G$$
2		mndcld.2	$$⊢\underset{\dot{}}{+}={+}_G$$
3		mndcld.3	$$⊢\phi \to G\in \mathrm{Mnd}$$
4		mndcld.4	$$⊢\phi \to X\in B$$
5		mndcld.5	$$⊢\phi \to Y\in B$$
6	1 2	mndcl	$$⊢\left(G\in \mathrm{Mnd}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y\in B$$
7	3 4 5 6	syl3anc	$$⊢\phi \to X\underset{\dot{}}{+}Y\in B$$