Theorem omndtos

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

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

Proof

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