This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 oGrp \leftrightarrow (G \in Grp \land G \in oMnd)$

Step	Hyp	Ref	Expression
1		df-ogrp	$⊢ oGrp = Grp \cap oMnd$
2	1	elin2	$⊢ G \in oGrp \leftrightarrow (G \in Grp \land G \in oMnd)$