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