Theorem isogrp 20193

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

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2149  Grpcgrp 18999  oMndcomnd 20188  oGrpcogrp 20189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-ogrp 20191

This theorem is referenced by:  ogrpgrp  20194  ogrpinv0le  20205  ogrpsub  20206  ogrpaddlt  20207  orngsqr  20946  ornglmulle  20947  orngrmulle  20948  ofldtos  20953  suborng  20956  zsoring  28567  isarchi3  33447  archirng  33448  archirngz  33449  archiabllem1a  33451  archiabllem1b  33452  archiabllem2a  33454  archiabllem2c  33455  archiabllem2b  33456  archiabl  33458  reofld  33605  nn0omnd  33606