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

Theorem isogrp 26301
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 26299 . 2  |- oGrp  =  ( Grp  i^i oMnd )
21elin2 3641 1  |-  ( G  e. oGrp 
<->  ( G  e.  Grp  /\  G  e. oMnd ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    e. wcel 1758   Grpcgrp 15514  oMndcomnd 26296  oGrpcogrp 26297
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3072  df-in 3435  df-ogrp 26299
This theorem is referenced by:  ogrpgrp  26302  ogrpinvOLD  26314  ogrpinv0le  26315  ogrpsub  26316  ogrpaddlt  26317  isarchi3  26340  archirng  26341  archirngz  26342  archiabllem1a  26344  archiabllem1b  26345  archiabllem1  26346  archiabllem2a  26347  archiabllem2c  26348  archiabllem2b  26349  archiabllem2  26350  archiabl  26351  orngsqr  26408  ornglmulle  26409  orngrmulle  26410  ofldtos  26415  suborng  26419  reofld  26444  nn0omnd  26445
  Copyright terms: Public domain W3C validator