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 oGrp oMnd

Proof of Theorem isogrp
StepHypRef Expression
1 df-ogrp 28456 . 2 oGrp oMnd
21elin2 3620 1 oGrp oMnd
 Colors of variables: wff setvar class Syntax hints:   wb 188   wa 371   wcel 1886  cgrp 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