Theorem isogrp 20338

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2144  Grpcgrp 19144  oMndcomnd 20333  oGrpcogrp 20334

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4091  df-ogrp 20336

This theorem is used by:  ogrpgrp  20339  ogrpinv0le  20350  ogrpsub  20351  ogrpaddlt  20352  orngsqr  21123  ornglmulle  21124  orngrmulle  21125  ofldtos  21130  suborng  21133  zsoring  28795  isarchi3  33748  archirng  33749  archirngz  33750  archiabllem1a  33752  archiabllem1b  33753  archiabllem2a  33755  archiabllem2c  33756  archiabllem2b  33757  archiabl  33759  reofld  33904  nn0omnd  33905