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 e. oGrp <-> ( G e. Grp /\ G e. oMnd ) )

Proof

Step Hyp Ref Expression
1 df-ogrp 
 |-  oGrp = ( Grp i^i oMnd )
2 1 elin2 
 |-  ( G e. oGrp <-> ( G e. Grp /\ G e. oMnd ) )