Metamath Proof Explorer


Definition df-ofld

Description: Define class of all ordered fields. An ordered field is a field with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 18-Jan-2018)

Ref Expression
Assertion df-ofld oField = ( Field ∩ oRing )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cofld oField
1 cfield Field
2 corng oRing
3 1 2 cin ( Field ∩ oRing )
4 0 3 wceq oField = ( Field ∩ oRing )