Metamath Proof Explorer

Theorem flddmn

Description: A field is a domain. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Assertion flddmn ⊢ K ∈ Fld → K ∈ Dmn

Proof

Step Hyp Ref Expression
1 divrngpr ⊢ K ∈ DivRingOps → K ∈ PrRing
2 1 anim1i ⊢ K ∈ DivRingOps ∧ K ∈ CRingOps → K ∈ PrRing ∧ K ∈ CRingOps
3 isfld2 ⊢ K ∈ Fld ↔ K ∈ DivRingOps ∧ K ∈ CRingOps
4 isdmn2 ⊢ K ∈ Dmn ↔ K ∈ PrRing ∧ K ∈ CRingOps
5 2 3 4 3imtr4i ⊢ K ∈ Fld → K ∈ Dmn