Theorem mndcld

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

	Ref	Expression
Hypotheses	mndcld.1	|- B = ( Base ` G )
	mndcld.2	|- .+ = ( +g ` G )
	mndcld.3	|- ( ph -> G e. Mnd )
	mndcld.4	|- ( ph -> X e. B )
	mndcld.5	|- ( ph -> Y e. B )
Assertion	mndcld	|- ( ph -> ( X .+ Y ) e. B )

Proof

Step	Hyp	Ref	Expression
1		mndcld.1	|- B = ( Base ` G )
2		mndcld.2	|- .+ = ( +g ` G )
3		mndcld.3	|- ( ph -> G e. Mnd )
4		mndcld.4	|- ( ph -> X e. B )
5		mndcld.5	|- ( ph -> Y e. B )
6	1 2	mndcl	|- ( ( G e. Mnd /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
7	3 4 5 6	syl3anc	|- ( ph -> ( X .+ Y ) e. B )