Theorem isogrp 33075

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  Grpcgrp 18921  oMndcomnd 33070  oGrpcogrp 33071

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-in 3938  df-ogrp 33073

This theorem is referenced by:  ogrpgrp  33076  ogrpinv0le  33088  ogrpsub  33089  ogrpaddlt  33090  isarchi3  33190  archirng  33191  archirngz  33192  archiabllem1a  33194  archiabllem1b  33195  archiabllem2a  33197  archiabllem2c  33198  archiabllem2b  33199  archiabl  33201  orngsqr  33331  ornglmulle  33332  orngrmulle  33333  ofldtos  33338  suborng  33342  reofld  33364  nn0omnd  33365