Metamath Proof Explorer


Theorem sgrpcl

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

Ref Expression
Hypotheses sgrpass.b
|- B = ( Base ` G )
sgrpass.o
|- .o. = ( +g ` G )
Assertion sgrpcl
|- ( ( G e. Smgrp /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B )

Proof

Step Hyp Ref Expression
1 sgrpass.b
 |-  B = ( Base ` G )
2 sgrpass.o
 |-  .o. = ( +g ` G )
3 sgrpmgm
 |-  ( G e. Smgrp -> G e. Mgm )
4 1 2 mgmcl
 |-  ( ( G e. Mgm /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B )
5 3 4 syl3an1
 |-  ( ( G e. Smgrp /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B )