Theorem isogrp 20051

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  Grpcgrp 18861  oMndcomnd 20046  oGrpcogrp 20047

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906  df-ogrp 20049

This theorem is referenced by:  ogrpgrp  20052  ogrpinv0le  20063  ogrpsub  20064  ogrpaddlt  20065  orngsqr  20797  ornglmulle  20798  orngrmulle  20799  ofldtos  20804  suborng  20807  zsoring  28367  isarchi3  33218  archirng  33219  archirngz  33220  archiabllem1a  33222  archiabllem1b  33223  archiabllem2a  33225  archiabllem2c  33226  archiabllem2b  33227  archiabl  33229  reofld  33373  nn0omnd  33374