Theorem isogrp 20252

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 20250	. 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 19058  oMndcomnd 20247  oGrpcogrp 20248

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906  df-ogrp 20250

This theorem is used by:  ogrpgrp  20253  ogrpinv0le  20264  ogrpsub  20265  ogrpaddlt  20266  orngsqr  21033  ornglmulle  21034  orngrmulle  21035  ofldtos  21040  suborng  21043  zsoring  28675  isarchi3  33628  archirng  33629  archirngz  33630  archiabllem1a  33632  archiabllem1b  33633  archiabllem2a  33635  archiabllem2c  33636  archiabllem2b  33637  archiabl  33639  reofld  33784  nn0omnd  33785