This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem omndtos

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

Ref Expression
Assertion omndtos ⊢ M ∈ oMnd → M ∈ Toset

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base M = Base M
2 eqid ⊢ + M = + M
3 eqid ⊢ ≤ M = ≤ M
4 1 2 3 isomnd ⊢ M ∈ oMnd ↔ M ∈ Mnd ∧ M ∈ Toset ∧ ∀ a ∈ Base M ∀ b ∈ Base M ∀ c ∈ Base M a ≤ M b → a + M c ≤ M b + M c
5 4 simp2bi ⊢ M ∈ oMnd → M ∈ Toset