Theorem isogrp 30753

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

Syntax hints:   ↔ wb 209   ∧ wa 399   ∈ wcel 2111  Grpcgrp 18095  oMndcomnd 30748  oGrpcogrp 30749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ogrp 30751

This theorem is referenced by:  ogrpgrp  30754  ogrpinv0le  30766  ogrpsub  30767  ogrpaddlt  30768  isarchi3  30866  archirng  30867  archirngz  30868  archiabllem1a  30870  archiabllem1b  30871  archiabllem2a  30873  archiabllem2c  30874  archiabllem2b  30875  archiabl  30877  orngsqr  30928  ornglmulle  30929  orngrmulle  30930  ofldtos  30935  suborng  30939  reofld  30964  nn0omnd  30965