Theorem isogrp 32782

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

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2099  Grpcgrp 18889  oMndcomnd 32777  oGrpcogrp 32778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954  df-ogrp 32780

This theorem is referenced by:  ogrpgrp  32783  ogrpinv0le  32795  ogrpsub  32796  ogrpaddlt  32797  isarchi3  32895  archirng  32896  archirngz  32897  archiabllem1a  32899  archiabllem1b  32900  archiabllem2a  32902  archiabllem2c  32903  archiabllem2b  32904  archiabl  32906  orngsqr  33019  ornglmulle  33020  orngrmulle  33021  ofldtos  33026  suborng  33030  reofld  33056  nn0omnd  33057