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 ( 𝐷 ∈ ( Met ‘ 𝑋 ) → ( 𝐷 ≠ ∅ ↔ 𝑋 ≠ ∅ ) )

Proof

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