Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  omndtos Structured version   Unicode version

Theorem omndtos 26304
Description: A left ordered monoid is a totally ordered set. (Contributed by Thierry Arnoux, 13-Mar-2018.)
Assertion
Ref Expression
omndtos  |-  ( M  e. oMnd  ->  M  e. Toset )

Proof of Theorem omndtos
Dummy variables  a 
b  c are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2451 . . 3  |-  ( Base `  M )  =  (
Base `  M )
2 eqid 2451 . . 3  |-  ( +g  `  M )  =  ( +g  `  M )
3 eqid 2451 . . 3  |-  ( le
`  M )  =  ( le `  M
)
41, 2, 3isomnd 26300 . 2  |-  ( M  e. oMnd 
<->  ( M  e.  Mnd  /\  M  e. Toset  /\  A. a  e.  ( Base `  M
) A. b  e.  ( Base `  M
) A. c  e.  ( Base `  M
) ( a ( le `  M ) b  ->  ( a
( +g  `  M ) c ) ( le
`  M ) ( b ( +g  `  M
) c ) ) ) )
54simp2bi 1004 1  |-  ( M  e. oMnd  ->  M  e. Toset )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   A.wral 2795   class class class wbr 4392   ` cfv 5518  (class class class)co 6192   Basecbs 14278   +g cplusg 14342   lecple 14349  Tosetctos 15307   Mndcmnd 15513  oMndcomnd 26296
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-nul 4521
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3072  df-sbc 3287  df-dif 3431  df-un 3433  df-in 3435  df-ss 3442  df-nul 3738  df-if 3892  df-sn 3978  df-pr 3980  df-op 3984  df-uni 4192  df-br 4393  df-iota 5481  df-fv 5526  df-ov 6195  df-omnd 26298
This theorem is referenced by:  omndadd2d  26307  omndadd2rd  26308  submomnd  26309  omndmul2  26311  omndmul  26313  isarchi3  26340  archirng  26341  archirngz  26342  archiabllem1a  26344  archiabllem1b  26345  archiabllem2a  26347  archiabllem2c  26348  archiabllem2b  26349  archiabl  26351  gsumle  26382  orngsqr  26408  ofldtos  26415
  Copyright terms: Public domain W3C validator