Theorem isogrp 33079

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  Grpcgrp 18951  oMndcomnd 33074  oGrpcogrp 33075

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-ogrp 33077

This theorem is referenced by:  ogrpgrp  33080  ogrpinv0le  33092  ogrpsub  33093  ogrpaddlt  33094  isarchi3  33194  archirng  33195  archirngz  33196  archiabllem1a  33198  archiabllem1b  33199  archiabllem2a  33201  archiabllem2c  33202  archiabllem2b  33203  archiabl  33205  orngsqr  33334  ornglmulle  33335  orngrmulle  33336  ofldtos  33341  suborng  33345  reofld  33372  nn0omnd  33373