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

Theorem isogrp 28458
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 28456 . 2  |- oGrp  =  ( Grp  i^i oMnd )
21elin2 3620 1  |-  ( G  e. oGrp 
<->  ( G  e.  Grp  /\  G  e. oMnd ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    /\ wa 371    e. wcel 1886   Grpcgrp 16662  oMndcomnd 28453  oGrpcogrp 28454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-v 3046  df-in 3410  df-ogrp 28456
This theorem is referenced by:  ogrpgrp  28459  ogrpinvOLD  28471  ogrpinv0le  28472  ogrpsub  28473  ogrpaddlt  28474  isarchi3  28497  archirng  28498  archirngz  28499  archiabllem1a  28501  archiabllem1b  28502  archiabllem2a  28504  archiabllem2c  28505  archiabllem2b  28506  archiabl  28508  orngsqr  28560  ornglmulle  28561  orngrmulle  28562  ofldtos  28567  suborng  28571  reofld  28596  nn0omnd  28597
  Copyright terms: Public domain W3C validator