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

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