Theorem omndtos 20093

Description: A left-ordered monoid is a totally ordered set. (Contributed by Thierry Arnoux, 13-Mar-2018.)

Assertion

Ref	Expression
omndtos	⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset)

Proof of Theorem omndtos

Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2739	. . 3 ⊢ (Base‘𝑀) = (Base‘𝑀)
2		eqid 2739	. . 3 ⊢ (+g‘𝑀) = (+g‘𝑀)
3		eqid 2739	. . 3 ⊢ (le‘𝑀) = (le‘𝑀)
4	1, 2, 3	isomnd 20089	. 2 ⊢ (𝑀 ∈ oMnd ↔ (𝑀 ∈ Mnd ∧ 𝑀 ∈ Toset ∧ ∀𝑎 ∈ (Base‘𝑀)∀𝑏 ∈ (Base‘𝑀)∀𝑐 ∈ (Base‘𝑀)(𝑎(le‘𝑀)𝑏 → (𝑎(+g‘𝑀)𝑐)(le‘𝑀)(𝑏(+g‘𝑀)𝑐))))
5	4	simp2bi 1152	1 ⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset)

Syntax hints:   → wi 4   ∈ wcel 2119  ∀wral 3053   class class class wbr 5072  ‘cfv 6485  (class class class)co 7356  Basecbs 17170  +_gcplusg 17211  lecple 17218  Tosetctos 18371  Mndcmnd 18693  oMndcomnd 20085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-nul 5228

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359  df-omnd 20087

This theorem is referenced by:  omndadd2d  20096  omndadd2rd  20097  submomnd  20098  omndmul2  20099  omndmul  20101  gsumle  20111  orngsqr  20838  ofldtos  20845  isarchi3  33268  archirng  33269  archirngz  33270  archiabllem1a  33272  archiabllem1b  33273  archiabllem2a  33275  archiabllem2c  33276  archiabllem2b  33277  archiabl  33279