Theorem isogrp

Description: A (left-)ordered group is a group with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018)

	Ref	Expression
Assertion	isogrp	$$⊢G\in \mathrm{oGrp}\leftrightarrow \left(G\in \mathrm{Grp}\wedge G\in \mathrm{oMnd}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ogrp	$$⊢\mathrm{oGrp}=\mathrm{Grp}\cap \mathrm{oMnd}$$
2	1	elin2	$$⊢G\in \mathrm{oGrp}\leftrightarrow \left(G\in \mathrm{Grp}\wedge G\in \mathrm{oMnd}\right)$$