Theorem omndtos

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

	Ref	Expression
Assertion	omndtos	|- ( M e. oMnd -> M e. Toset )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Base ` M ) = ( Base ` M )
2		eqid	|- ( +g ` M ) = ( +g ` M )
3		eqid	|- ( le ` M ) = ( le ` M )
4	1 2 3	isomnd	|- ( M e. oMnd <-> ( M e. Mnd /\ M e. Toset /\ A. a e. ( Base ` M ) A. b e. ( Base ` M ) A. c e. ( Base ` M ) ( a ( le ` M ) b -> ( a ( +g ` M ) c ) ( le ` M ) ( b ( +g ` M ) c ) ) ) )
5	4	simp2bi	|- ( M e. oMnd -> M e. Toset )