Metamath Proof Explorer

Theorem metn0

Description: A metric space is nonempty iff its base set is nonempty. (Contributed by NM, 4-Oct-2007) (Revised by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion metn0 ⊢ D ∈ Met ⁡ X → D ≠ ∅ ↔ X ≠ ∅

Proof

Step Hyp Ref Expression
1 metf ⊢ D ∈ Met ⁡ X → D : X × X ⟶ ℝ
2 frel ⊢ D : X × X ⟶ ℝ → Rel ⁡ D
3 reldm0 ⊢ Rel ⁡ D → D = ∅ ↔ dom ⁡ D = ∅
4 1 2 3 3syl ⊢ D ∈ Met ⁡ X → D = ∅ ↔ dom ⁡ D = ∅
5 1 fdmd ⊢ D ∈ Met ⁡ X → dom ⁡ D = X × X
6 5 eqeq1d ⊢ D ∈ Met ⁡ X → dom ⁡ D = ∅ ↔ X × X = ∅
7 4 6 bitrd ⊢ D ∈ Met ⁡ X → D = ∅ ↔ X × X = ∅
8 xpeq0 ⊢ X × X = ∅ ↔ X = ∅ ∨ X = ∅
9 oridm ⊢ X = ∅ ∨ X = ∅ ↔ X = ∅
10 8 9 bitri ⊢ X × X = ∅ ↔ X = ∅
11 7 10 bitrdi ⊢ D ∈ Met ⁡ X → D = ∅ ↔ X = ∅
12 11 necon3bid ⊢ D ∈ Met ⁡ X → D ≠ ∅ ↔ X ≠ ∅