Theorem ofldtos

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

	Ref	Expression
Assertion	ofldtos	|- ( F e. oField -> F e. Toset )

Proof

Step	Hyp	Ref	Expression
1		isofld	|- ( F e. oField <-> ( F e. Field /\ F e. oRing ) )
2	1	simprbi	|- ( F e. oField -> F e. oRing )
3		orngogrp	|- ( F e. oRing -> F e. oGrp )
4		isogrp	|- ( F e. oGrp <-> ( F e. Grp /\ F e. oMnd ) )
5	4	simprbi	|- ( F e. oGrp -> F e. oMnd )
6	2 3 5	3syl	|- ( F e. oField -> F e. oMnd )
7		omndtos	|- ( F e. oMnd -> F e. Toset )
8	6 7	syl	|- ( F e. oField -> F e. Toset )