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	$$⊢\mathrm{oGrp}=\mathrm{Grp}\cap \mathrm{oMnd}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cogrp	$$class\mathrm{oGrp}$$
1		cgrp	$$class\mathrm{Grp}$$
2		comnd	$$class\mathrm{oMnd}$$
3	1 2	cin	$$class\left(\mathrm{Grp}\cap \mathrm{oMnd}\right)$$
4	0 3	wceq	$$wff\mathrm{oGrp}=\mathrm{Grp}\cap \mathrm{oMnd}$$