Definition df-ogrp

Description: Define class of all ordered groups. An ordered group is a group with a total ordering compatible with its operation. (Contributed by Thierry Arnoux, 13-Mar-2018)

	Ref	Expression
Assertion	df-ogrp	⊢ oGrp = ( Grp ∩ oMnd )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cogrp	⊢ oGrp
1		cgrp	⊢ Grp
2		comnd	⊢ oMnd
3	1 2	cin	⊢ ( Grp ∩ oMnd )
4	0 3	wceq	⊢ oGrp = ( Grp ∩ oMnd )