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

Theorem isogrp 30617
 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 ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))

Proof of Theorem isogrp
StepHypRef Expression
1 df-ogrp 30615 . 2 oGrp = (Grp ∩ oMnd)
21elin2 4178 1 (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 207   ∧ wa 396   ∈ wcel 2107  Grpcgrp 18033  oMndcomnd 30612  oGrpcogrp 30613 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-in 3947  df-ogrp 30615 This theorem is referenced by:  ogrpgrp  30618  ogrpinv0le  30630  ogrpsub  30631  ogrpaddlt  30632  isarchi3  30730  archirng  30731  archirngz  30732  archiabllem1a  30734  archiabllem1b  30735  archiabllem2a  30737  archiabllem2c  30738  archiabllem2b  30739  archiabl  30741  orngsqr  30791  ornglmulle  30792  orngrmulle  30793  ofldtos  30798  suborng  30802  reofld  30827  nn0omnd  30828
 Copyright terms: Public domain W3C validator