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	⊢ ( 𝐺 ∈ oGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd ) )

Proof

Step	Hyp	Ref	Expression
1		df-ogrp	⊢ oGrp = ( Grp ∩ oMnd )
2	1	elin2	⊢ ( 𝐺 ∈ oGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd ) )