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

Theorem isogrp 28144
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 28142 . 2  |- oGrp  =  ( Grp  i^i oMnd )
21elin2 3630 1  |-  ( G  e. oGrp 
<->  ( G  e.  Grp  /\  G  e. oMnd ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367    e. wcel 1842   Grpcgrp 16377  oMndcomnd 28139  oGrpcogrp 28140
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3061  df-in 3421  df-ogrp 28142
This theorem is referenced by:  ogrpgrp  28145  ogrpinvOLD  28157  ogrpinv0le  28158  ogrpsub  28159  ogrpaddlt  28160  isarchi3  28183  archirng  28184  archirngz  28185  archiabllem1a  28187  archiabllem1b  28188  archiabllem2a  28190  archiabllem2c  28191  archiabllem2b  28192  archiabl  28194  orngsqr  28247  ornglmulle  28248  orngrmulle  28249  ofldtos  28254  suborng  28258  reofld  28283  nn0omnd  28284
  Copyright terms: Public domain W3C validator