Theorem isogrp 20003

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  Grpcgrp 18812  oMndcomnd 19998  oGrpcogrp 19999

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-in 3910  df-ogrp 20001

This theorem is referenced by:  ogrpgrp  20004  ogrpinv0le  20015  ogrpsub  20016  ogrpaddlt  20017  orngsqr  20751  ornglmulle  20752  orngrmulle  20753  ofldtos  20758  suborng  20761  zsoring  28301  isarchi3  33129  archirng  33130  archirngz  33131  archiabllem1a  33133  archiabllem1b  33134  archiabllem2a  33136  archiabllem2c  33137  archiabllem2b  33138  archiabl  33140  reofld  33281  nn0omnd  33282