Theorem isogrp 20164

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

Syntax hints:   ↔ wb 208   ∧ wa 399   ∈ wcel 2142  Grpcgrp 18975  oMndcomnd 20159  oGrpcogrp 20160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911  df-ogrp 20162

This theorem is referenced by:  ogrpgrp  20165  ogrpinv0le  20176  ogrpsub  20177  ogrpaddlt  20178  orngsqr  20915  ornglmulle  20916  orngrmulle  20917  ofldtos  20922  suborng  20925  zsoring  28502  isarchi3  33367  archirng  33368  archirngz  33369  archiabllem1a  33371  archiabllem1b  33372  archiabllem2a  33374  archiabllem2c  33375  archiabllem2b  33376  archiabl  33378  reofld  33529  nn0omnd  33530