Theorem isogrp 29702

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

Assertion

Ref	Expression
isogrp	|- ( G e. oGrp <-> ( G e. Grp /\ G e. oMnd ) )

Proof of Theorem isogrp

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

Syntax hints:   <-> wb 196   /\ wa 384   e. wcel 1990   Grpcgrp 17422  oMndcomnd 29697  oGrpcogrp 29698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ogrp 29700

This theorem is referenced by:  ogrpgrp  29703  ogrpinvOLD  29715  ogrpinv0le  29716  ogrpsub  29717  ogrpaddlt  29718  isarchi3  29741  archirng  29742  archirngz  29743  archiabllem1a  29745  archiabllem1b  29746  archiabllem2a  29748  archiabllem2c  29749  archiabllem2b  29750  archiabl  29752  orngsqr  29804  ornglmulle  29805  orngrmulle  29806  ofldtos  29811  suborng  29815  reofld  29840  nn0omnd  29841