Definition df-ogrp 31228

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.)

Assertion

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

Detailed syntax breakdown of Definition df-ogrp

Step	Hyp	Ref	Expression
1		cogrp 31226	. 2 class oGrp
2		cgrp 18492	. . 3 class Grp
3		comnd 31225	. . 3 class oMnd
4	2, 3	cin 3882	. 2 class (Grp ∩ oMnd)
5	1, 4	wceq 1539	1 wff oGrp = (Grp ∩ oMnd)

This definition is referenced by:  isogrp  31230