Theorem metflem

Description: Lemma for metf and others. (Contributed by NM, 30-Aug-2006) (Revised by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	metflem	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝑋 ∈ dom Met )
2		ismet	⊢ ( 𝑋 ∈ dom Met → ( 𝐷 ∈ ( Met ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
3	1 2	syl	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → ( 𝐷 ∈ ( Met ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
4	3	ibi	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) ) ) )