Metamath Proof Explorer


Theorem sgrpcl

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

Ref Expression
Hypotheses sgrpass.b 𝐵 = ( Base ‘ 𝐺 )
sgrpass.o = ( +g𝐺 )
Assertion sgrpcl ( ( 𝐺 ∈ Smgrp ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 sgrpass.b 𝐵 = ( Base ‘ 𝐺 )
2 sgrpass.o = ( +g𝐺 )
3 sgrpmgm ( 𝐺 ∈ Smgrp → 𝐺 ∈ Mgm )
4 1 2 mgmcl ( ( 𝐺 ∈ Mgm ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) ∈ 𝐵 )
5 3 4 syl3an1 ( ( 𝐺 ∈ Smgrp ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) ∈ 𝐵 )