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