Theorem isogrp 20090

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

Syntax hints:   ↔ wb 207   ∧ wa 396   ∈ wcel 2119  Grpcgrp 18900  oMndcomnd 20085  oGrpcogrp 20086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890  df-ogrp 20088

This theorem is referenced by:  ogrpgrp  20091  ogrpinv0le  20102  ogrpsub  20103  ogrpaddlt  20104  orngsqr  20838  ornglmulle  20839  orngrmulle  20840  ofldtos  20845  suborng  20848  zsoring  28419  isarchi3  33268  archirng  33269  archirngz  33270  archiabllem1a  33272  archiabllem1b  33273  archiabllem2a  33275  archiabllem2c  33276  archiabllem2b  33277  archiabl  33279  reofld  33426  nn0omnd  33427