|   | Mathbox for Thierry Arnoux | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > isogrp | Structured version Visualization version GIF version | ||
| Description: A (left-)ordered group is a group with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.) | 
| Ref | Expression | 
|---|---|
| isogrp | ⊢ (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | df-ogrp 33077 | . 2 ⊢ oGrp = (Grp ∩ oMnd) | |
| 2 | 1 | elin2 4203 | 1 ⊢ (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∧ wa 395 ∈ wcel 2108 Grpcgrp 18951 oMndcomnd 33074 oGrpcogrp 33075 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-in 3958 df-ogrp 33077 | 
| This theorem is referenced by: ogrpgrp 33080 ogrpinv0le 33092 ogrpsub 33093 ogrpaddlt 33094 isarchi3 33194 archirng 33195 archirngz 33196 archiabllem1a 33198 archiabllem1b 33199 archiabllem2a 33201 archiabllem2c 33202 archiabllem2b 33203 archiabl 33205 orngsqr 33334 ornglmulle 33335 orngrmulle 33336 ofldtos 33341 suborng 33345 reofld 33372 nn0omnd 33373 | 
| Copyright terms: Public domain | W3C validator |