Theorem flddmn

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

	Ref	Expression
Assertion	flddmn	⊢ ( 𝐾 ∈ Fld → 𝐾 ∈ Dmn )

Proof

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