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

Theorem isogrp 29479
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 29477 . 2 oGrp = (Grp ∩ oMnd)
21elin2 3784 1 (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  wcel 1992  Grpcgrp 17338  oMndcomnd 29474  oGrpcogrp 29475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-v 3193  df-in 3567  df-ogrp 29477
This theorem is referenced by:  ogrpgrp  29480  ogrpinvOLD  29492  ogrpinv0le  29493  ogrpsub  29494  ogrpaddlt  29495  isarchi3  29518  archirng  29519  archirngz  29520  archiabllem1a  29522  archiabllem1b  29523  archiabllem2a  29525  archiabllem2c  29526  archiabllem2b  29527  archiabl  29529  orngsqr  29581  ornglmulle  29582  orngrmulle  29583  ofldtos  29588  suborng  29592  reofld  29617  nn0omnd  29618
  Copyright terms: Public domain W3C validator