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 ) |
| 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 | omndtos | |- ( F e. oMnd -> F e. Toset ) |
|
| 7 | 2 3 5 6 | 4syl | |- ( F e. oField -> F e. Toset ) |