Theorem isogrp 20238

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2146  Grpcgrp 19044  oMndcomnd 20233  oGrpcogrp 20234

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913  df-ogrp 20236

This theorem is used by:  ogrpgrp  20239  ogrpinv0le  20250  ogrpsub  20251  ogrpaddlt  20252  orngsqr  21019  ornglmulle  21020  orngrmulle  21021  ofldtos  21026  suborng  21029  zsoring  28653  isarchi3  33571  archirng  33572  archirngz  33573  archiabllem1a  33575  archiabllem1b  33576  archiabllem2a  33578  archiabllem2c  33579  archiabllem2b  33580  archiabl  33582  reofld  33727  nn0omnd  33728