Theorem sgrpcl

Description: Closure of the operation of a semigroup. (Contributed by AV, 15-Feb-2025)

	Ref	Expression
Hypotheses	sgrpass.b	$$⊢B={\mathrm{Base}}_G$$
	sgrpass.o	No typesetting found for |- .o. = ( +g ` G ) with typecode |-
Assertion	sgrpcl	Could not format assertion : No typesetting found for |- ( ( G e. Smgrp /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		sgrpass.b	$$⊢B={\mathrm{Base}}_G$$
2		sgrpass.o	Could not format .o. = ( +g ` G ) : No typesetting found for |- .o. = ( +g ` G ) with typecode |-
3		sgrpmgm	$$⊢G\in \mathrm{Smgrp}\to G\in \mathrm{Mgm}$$
4	1 2	mgmcl	Could not format ( ( G e. Mgm /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B ) : No typesetting found for |- ( ( G e. Mgm /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B ) with typecode |-
5	3 4	syl3an1	Could not format ( ( G e. Smgrp /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B ) : No typesetting found for |- ( ( G e. Smgrp /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B ) with typecode |-