Metamath Proof Explorer
Description: A (left)ordered group is a group with a total ordering compatible with
its operations. (Contributed by Thierry Arnoux, 23Mar2018)


Ref 
Expression 

Assertion 
isogrp 
$${\u22a2}{G}\in \mathrm{oGrp}\leftrightarrow \left({G}\in \mathrm{Grp}\wedge {G}\in \mathrm{oMnd}\right)$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

dfogrp 
$${\u22a2}\mathrm{oGrp}=\mathrm{Grp}\cap \mathrm{oMnd}$$ 
2 
1

elin2 
$${\u22a2}{G}\in \mathrm{oGrp}\leftrightarrow \left({G}\in \mathrm{Grp}\wedge {G}\in \mathrm{oMnd}\right)$$ 