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 33079
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 33077 . 2 oGrp = (Grp ∩ oMnd)
21elin2 4203 1 (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wcel 2108  Grpcgrp 18951  oMndcomnd 33074  oGrpcogrp 33075
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-ogrp 33077
This theorem is referenced by:  ogrpgrp  33080  ogrpinv0le  33092  ogrpsub  33093  ogrpaddlt  33094  isarchi3  33194  archirng  33195  archirngz  33196  archiabllem1a  33198  archiabllem1b  33199  archiabllem2a  33201  archiabllem2c  33202  archiabllem2b  33203  archiabl  33205  orngsqr  33334  ornglmulle  33335  orngrmulle  33336  ofldtos  33341  suborng  33345  reofld  33372  nn0omnd  33373
  Copyright terms: Public domain W3C validator