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 e. oField <-> ( F e. Field /\ F e. oRing ) )

Proof

Step Hyp Ref Expression
1 df-ofld 
 |-  oField = ( Field i^i oRing )
2 1 elin2 
 |-  ( F e. oField <-> ( F e. Field /\ F e. oRing ) )