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

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

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