Theorem isogrp 20189

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

Step	Hyp	Ref	Expression
1		df-ogrp 20187	. 2 ⊢ oGrp = (Grp ∩ oMnd)
2	1	elin2 4156	1 ⊢ (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2143  Grpcgrp 18995  oMndcomnd 20184  oGrpcogrp 20185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-ogrp 20187

This theorem is referenced by:  ogrpgrp  20190  ogrpinv0le  20201  ogrpsub  20202  ogrpaddlt  20203  orngsqr  20969  ornglmulle  20970  orngrmulle  20971  ofldtos  20976  suborng  20979  zsoring  28602  isarchi3  33507  archirng  33508  archirngz  33509  archiabllem1a  33511  archiabllem1b  33512  archiabllem2a  33514  archiabllem2c  33515  archiabllem2b  33516  archiabl  33518  reofld  33663  nn0omnd  33664