Metamath Proof Explorer


Theorem isofld

Description: An ordered field is a field with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018)

Ref Expression
Assertion isofld F oField F Field F oRing

Proof

Step Hyp Ref Expression
1 df-ofld oField = Field oRing
2 1 elin2 F oField F Field F oRing