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

Theorem isogrp 30854
 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 30852 . 2 oGrp = (Grp ∩ oMnd)
21elin2 4102 1 (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   ∈ wcel 2111  Grpcgrp 18169  oMndcomnd 30849  oGrpcogrp 30850 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ogrp 30852 This theorem is referenced by:  ogrpgrp  30855  ogrpinv0le  30867  ogrpsub  30868  ogrpaddlt  30869  isarchi3  30967  archirng  30968  archirngz  30969  archiabllem1a  30971  archiabllem1b  30972  archiabllem2a  30974  archiabllem2c  30975  archiabllem2b  30976  archiabl  30978  orngsqr  31029  ornglmulle  31030  orngrmulle  31031  ofldtos  31036  suborng  31040  reofld  31065  nn0omnd  31066
 Copyright terms: Public domain W3C validator