Theorem isogrp 20339

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  Grpcgrp 19145  oMndcomnd 20334  oGrpcogrp 20335

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3904  df-ogrp 20337

This theorem is used by:  ogrpgrp  20340  ogrpinv0le  20351  ogrpsub  20352  ogrpaddlt  20353  orngsqr  21124  ornglmulle  21125  orngrmulle  21126  ofldtos  21131  suborng  21134  zsoring  28796  isarchi3  33749  archirng  33750  archirngz  33751  archiabllem1a  33753  archiabllem1b  33754  archiabllem2a  33756  archiabllem2c  33757  archiabllem2b  33758  archiabl  33760  reofld  33905  nn0omnd  33906