Theorem isogrp 32989

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  Grpcgrp 18841  oMndcomnd 32984  oGrpcogrp 32985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918  df-ogrp 32987

This theorem is referenced by:  ogrpgrp  32990  ogrpinv0le  33002  ogrpsub  33003  ogrpaddlt  33004  isarchi3  33114  archirng  33115  archirngz  33116  archiabllem1a  33118  archiabllem1b  33119  archiabllem2a  33121  archiabllem2c  33122  archiabllem2b  33123  archiabl  33125  orngsqr  33255  ornglmulle  33256  orngrmulle  33257  ofldtos  33262  suborng  33266  reofld  33288  nn0omnd  33289