Theorem omndtos 20254

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∀wral 3076   class class class wbr 5103  ‘cfv 6533  (class class class)co 7413  Basecbs 17301  +_gcplusg 17342  lecple 17349  Tosetctos 18502  Mndcmnd 18836  oMndcomnd 20246

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7416  df-omnd 20248

This theorem is used by:  omndadd2d  20257  omndadd2rd  20258  submomnd  20259  omndmul2  20260  omndmul  20262  gsumle  20272  orngsqr  21032  ofldtos  21039  isarchi3  33627  archirng  33628  archirngz  33629  archiabllem1a  33631  archiabllem1b  33632  archiabllem2a  33634  archiabllem2c  33635  archiabllem2b  33636  archiabl  33638