Theorem isogrp 31230

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

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2108  Grpcgrp 18492  oMndcomnd 31225  oGrpcogrp 31226

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ogrp 31228

This theorem is referenced by:  ogrpgrp  31231  ogrpinv0le  31243  ogrpsub  31244  ogrpaddlt  31245  isarchi3  31343  archirng  31344  archirngz  31345  archiabllem1a  31347  archiabllem1b  31348  archiabllem2a  31350  archiabllem2c  31351  archiabllem2b  31352  archiabl  31354  orngsqr  31405  ornglmulle  31406  orngrmulle  31407  ofldtos  31412  suborng  31416  reofld  31446  nn0omnd  31447