Theorem isogrp 33062

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2106  Grpcgrp 18964  oMndcomnd 33057  oGrpcogrp 33058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-in 3970  df-ogrp 33060

This theorem is referenced by:  ogrpgrp  33063  ogrpinv0le  33075  ogrpsub  33076  ogrpaddlt  33077  isarchi3  33177  archirng  33178  archirngz  33179  archiabllem1a  33181  archiabllem1b  33182  archiabllem2a  33184  archiabllem2c  33185  archiabllem2b  33186  archiabl  33188  orngsqr  33314  ornglmulle  33315  orngrmulle  33316  ofldtos  33321  suborng  33325  reofld  33352  nn0omnd  33353