Theorem omndtos 33019

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 2729	. . 3 ⊢ (Base‘𝑀) = (Base‘𝑀)
2		eqid 2729	. . 3 ⊢ (+g‘𝑀) = (+g‘𝑀)
3		eqid 2729	. . 3 ⊢ (le‘𝑀) = (le‘𝑀)
4	1, 2, 3	isomnd 33015	. 2 ⊢ (𝑀 ∈ oMnd ↔ (𝑀 ∈ Mnd ∧ 𝑀 ∈ Toset ∧ ∀𝑎 ∈ (Base‘𝑀)∀𝑏 ∈ (Base‘𝑀)∀𝑐 ∈ (Base‘𝑀)(𝑎(le‘𝑀)𝑏 → (𝑎(+g‘𝑀)𝑐)(le‘𝑀)(𝑏(+g‘𝑀)𝑐))))
5	4	simp2bi 1146	1 ⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset)

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044   class class class wbr 5107  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  +_gcplusg 17220  lecple 17227  Tosetctos 18375  Mndcmnd 18661  oMndcomnd 33011

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-omnd 33013

This theorem is referenced by:  omndadd2d  33022  omndadd2rd  33023  submomnd  33024  omndmul2  33026  omndmul  33028  gsumle  33038  isarchi3  33141  archirng  33142  archirngz  33143  archiabllem1a  33145  archiabllem1b  33146  archiabllem2a  33148  archiabllem2c  33149  archiabllem2b  33150  archiabl  33152  orngsqr  33282  ofldtos  33289