Theorem omndtos

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

	Ref	Expression
Assertion	omndtos	$$⊢M\in \mathrm{oMnd}\to M\in \mathrm{Toset}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
2		eqid	$$⊢{+}_M={+}_M$$
3		eqid	$$⊢{\le }_M={\le }_M$$
4	1 2 3	isomnd	$$⊢M\in \mathrm{oMnd}\leftrightarrow \left(M\in \mathrm{Mnd}\wedge M\in \mathrm{Toset}\wedge \forall a\in {\mathrm{Base}}_M\forall b\in {\mathrm{Base}}_M\forall c\in {\mathrm{Base}}_M\left(a{\le }_{M}b\to \left(a{+}_{M}c\right){\le }_M\left(b{+}_{M}c\right)\right)\right)$$
5	4	simp2bi	$$⊢M\in \mathrm{oMnd}\to M\in \mathrm{Toset}$$