Theorem isogrp 30703

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 30701	. 2 ⊢ oGrp = (Grp ∩ oMnd)
2	1	elin2 4174	1 ⊢ (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))

Syntax hints:   ↔ wb 208   ∧ wa 398   ∈ wcel 2114  Grpcgrp 18103  oMndcomnd 30698  oGrpcogrp 30699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ogrp 30701

This theorem is referenced by:  ogrpgrp  30704  ogrpinv0le  30716  ogrpsub  30717  ogrpaddlt  30718  isarchi3  30816  archirng  30817  archirngz  30818  archiabllem1a  30820  archiabllem1b  30821  archiabllem2a  30823  archiabllem2c  30824  archiabllem2b  30825  archiabl  30827  orngsqr  30877  ornglmulle  30878  orngrmulle  30879  ofldtos  30884  suborng  30888  reofld  30913  nn0omnd  30914