Theorem isogrp 30705

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

Syntax hints:   ↔ wb 208   ∧ wa 398   ∈ wcel 2114  Grpcgrp 18105  oMndcomnd 30700  oGrpcogrp 30701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ogrp 30703

This theorem is referenced by:  ogrpgrp  30706  ogrpinv0le  30718  ogrpsub  30719  ogrpaddlt  30720  isarchi3  30818  archirng  30819  archirngz  30820  archiabllem1a  30822  archiabllem1b  30823  archiabllem2a  30825  archiabllem2c  30826  archiabllem2b  30827  archiabl  30829  orngsqr  30879  ornglmulle  30880  orngrmulle  30881  ofldtos  30886  suborng  30890  reofld  30915  nn0omnd  30916