This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ¬ x ∈ ∅
7 6 pm2.21i ⊢ x ∈ ∅ → x ∅ y = 0 ↔ x = y
8 7 adantr ⊢ x ∈ ∅ ∧ y ∈ ∅ → x ∅ y = 0 ↔ x = y
9 6 pm2.21i ⊢ x ∈ ∅ → x ∅ y ≤ z ∅ x + z ∅ y
10 9 3ad2ant1 ⊢ x ∈ ∅ ∧ y ∈ ∅ ∧ z ∈ ∅ → x ∅ y ≤ z ∅ x + z ∅ y
11 1 5 8 10 ismeti ⊢ ∅ ∈ Met ⁡ ∅