Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isogrp Structured version   Unicode version

Theorem isogrp 27340
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
StepHypRef Expression
1 df-ogrp 27338 . 2  |- oGrp  =  ( Grp  i^i oMnd )
21elin2 3682 1  |-  ( G  e. oGrp 
<->  ( G  e.  Grp  /\  G  e. oMnd ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    e. wcel 1762   Grpcgrp 15716  oMndcomnd 27335  oGrpcogrp 27336
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-in 3476  df-ogrp 27338
This theorem is referenced by:  ogrpgrp  27341  ogrpinvOLD  27353  ogrpinv0le  27354  ogrpsub  27355  ogrpaddlt  27356  isarchi3  27379  archirng  27380  archirngz  27381  archiabllem1a  27383  archiabllem1b  27384  archiabllem1  27385  archiabllem2a  27386  archiabllem2c  27387  archiabllem2b  27388  archiabllem2  27389  archiabl  27390  orngsqr  27443  ornglmulle  27444  orngrmulle  27445  ofldtos  27450  suborng  27454  reofld  27479  nn0omnd  27480
  Copyright terms: Public domain W3C validator