Theorem isogrp 33052

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  Grpcgrp 18973  oMndcomnd 33047  oGrpcogrp 33048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-ogrp 33050

This theorem is referenced by:  ogrpgrp  33053  ogrpinv0le  33065  ogrpsub  33066  ogrpaddlt  33067  isarchi3  33167  archirng  33168  archirngz  33169  archiabllem1a  33171  archiabllem1b  33172  archiabllem2a  33174  archiabllem2c  33175  archiabllem2b  33176  archiabl  33178  orngsqr  33299  ornglmulle  33300  orngrmulle  33301  ofldtos  33306  suborng  33310  reofld  33337  nn0omnd  33338