Theorem 0met

Description: The empty metric. (Contributed by NM, 30-Aug-2006) (Revised by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	0met	⊢ ∅ ∈ ( Met ‘ ∅ )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		f0	⊢ ∅ : ∅ ⟶ ℝ
3		xp0	⊢ ( ∅ × ∅ ) = ∅
4	3	feq2i	⊢ ( ∅ : ( ∅ × ∅ ) ⟶ ℝ ↔ ∅ : ∅ ⟶ ℝ )
5	2 4	mpbir	⊢ ∅ : ( ∅ × ∅ ) ⟶ ℝ
6		noel	⊢ ¬ 𝑥 ∈ ∅
7	6	pm2.21i	⊢ ( 𝑥 ∈ ∅ → ( ( 𝑥 ∅ 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
8	7	adantr	⊢ ( ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ) → ( ( 𝑥 ∅ 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
9	6	pm2.21i	⊢ ( 𝑥 ∈ ∅ → ( 𝑥 ∅ 𝑦 ) ≤ ( ( 𝑧 ∅ 𝑥 ) + ( 𝑧 ∅ 𝑦 ) ) )
10	9	3ad2ant1	⊢ ( ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅ ) → ( 𝑥 ∅ 𝑦 ) ≤ ( ( 𝑧 ∅ 𝑥 ) + ( 𝑧 ∅ 𝑦 ) ) )
11	1 5 8 10	ismeti	⊢ ∅ ∈ ( Met ‘ ∅ )