Definition df-sgrp2

Description: Asemigroup is a magma with an associative operation. Definition in section II.1 of Bruck p. 23, or of an "associative magma" in definition 5 of BourbakiAlg1 p. 4, or of a semigroup in section 1.3 of Hall p. 7. (Contributed by AV, 6-Jan-2020)

	Ref	Expression
Assertion	df-sgrp2	⊢ SGrpALT = { 𝑔 ∈ MgmALT ∣ ( +g ‘ 𝑔 ) assLaw ( Base ‘ 𝑔 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csgrp2	⊢ SGrpALT
1		vg	⊢ 𝑔
2		cmgm2	⊢ MgmALT
3		cplusg	⊢ +g
4	1	cv	⊢ 𝑔
5	4 3	cfv	⊢ ( +g ‘ 𝑔 )
6		casslaw	⊢ assLaw
7		cbs	⊢ Base
8	4 7	cfv	⊢ ( Base ‘ 𝑔 )
9	5 8 6	wbr	⊢ ( +g ‘ 𝑔 ) assLaw ( Base ‘ 𝑔 )
10	9 1 2	crab	⊢ { 𝑔 ∈ MgmALT ∣ ( +g ‘ 𝑔 ) assLaw ( Base ‘ 𝑔 ) }
11	0 10	wceq	⊢ SGrpALT = { 𝑔 ∈ MgmALT ∣ ( +g ‘ 𝑔 ) assLaw ( Base ‘ 𝑔 ) }