Theorem ofldtos

Description: An ordered field is a totally ordered set. (Contributed by Thierry Arnoux, 20-Jan-2018)

	Ref	Expression
Assertion	ofldtos	⊢ ( 𝐹 ∈ oField → 𝐹 ∈ Toset )

Proof

Step	Hyp	Ref	Expression
1		isofld	⊢ ( 𝐹 ∈ oField ↔ ( 𝐹 ∈ Field ∧ 𝐹 ∈ oRing ) )
2	1	simprbi	⊢ ( 𝐹 ∈ oField → 𝐹 ∈ oRing )
3		orngogrp	⊢ ( 𝐹 ∈ oRing → 𝐹 ∈ oGrp )
4		isogrp	⊢ ( 𝐹 ∈ oGrp ↔ ( 𝐹 ∈ Grp ∧ 𝐹 ∈ oMnd ) )
5	4	simprbi	⊢ ( 𝐹 ∈ oGrp → 𝐹 ∈ oMnd )
6	2 3 5	3syl	⊢ ( 𝐹 ∈ oField → 𝐹 ∈ oMnd )
7		omndtos	⊢ ( 𝐹 ∈ oMnd → 𝐹 ∈ Toset )
8	6 7	syl	⊢ ( 𝐹 ∈ oField → 𝐹 ∈ Toset )