Theorem isogrp 33023

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  Grpcgrp 18872  oMndcomnd 33018  oGrpcogrp 33019

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924  df-ogrp 33021

This theorem is referenced by:  ogrpgrp  33024  ogrpinv0le  33036  ogrpsub  33037  ogrpaddlt  33038  isarchi3  33148  archirng  33149  archirngz  33150  archiabllem1a  33152  archiabllem1b  33153  archiabllem2a  33155  archiabllem2c  33156  archiabllem2b  33157  archiabl  33159  orngsqr  33289  ornglmulle  33290  orngrmulle  33291  ofldtos  33296  suborng  33300  reofld  33322  nn0omnd  33323