Theorem isogrp 20053

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  Grpcgrp 18863  oMndcomnd 20048  oGrpcogrp 20049

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-ogrp 20051

This theorem is referenced by:  ogrpgrp  20054  ogrpinv0le  20065  ogrpsub  20066  ogrpaddlt  20067  orngsqr  20799  ornglmulle  20800  orngrmulle  20801  ofldtos  20806  suborng  20809  zsoring  28405  isarchi3  33269  archirng  33270  archirngz  33271  archiabllem1a  33273  archiabllem1b  33274  archiabllem2a  33276  archiabllem2c  33277  archiabllem2b  33278  archiabl  33280  reofld  33424  nn0omnd  33425