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\in \mathrm{Met}\left(X\right)\to \left(D\ne \varnothing \leftrightarrow X\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		metf	$$⊢D\in \mathrm{Met}\left(X\right)\to D:X\times X⟶ℝ$$
2		frel	$$⊢D:X\times X⟶ℝ\to \mathrm{Rel}D$$
3		reldm0	$$⊢\mathrm{Rel}D\to \left(D=\varnothing \leftrightarrow \mathrm{dom}D=\varnothing \right)$$
4	1 2 3	3syl	$$⊢D\in \mathrm{Met}\left(X\right)\to \left(D=\varnothing \leftrightarrow \mathrm{dom}D=\varnothing \right)$$
5	1	fdmd	$$⊢D\in \mathrm{Met}\left(X\right)\to \mathrm{dom}D=X\times X$$
6	5	eqeq1d	$$⊢D\in \mathrm{Met}\left(X\right)\to \left(\mathrm{dom}D=\varnothing \leftrightarrow X\times X=\varnothing \right)$$
7	4 6	bitrd	$$⊢D\in \mathrm{Met}\left(X\right)\to \left(D=\varnothing \leftrightarrow X\times X=\varnothing \right)$$
8		xpeq0	$$⊢X\times X=\varnothing \leftrightarrow \left(X=\varnothing \vee X=\varnothing \right)$$
9		oridm	$$⊢\left(X=\varnothing \vee X=\varnothing \right)\leftrightarrow X=\varnothing$$
10	8 9	bitri	$$⊢X\times X=\varnothing \leftrightarrow X=\varnothing$$
11	7 10	bitrdi	$$⊢D\in \mathrm{Met}\left(X\right)\to \left(D=\varnothing \leftrightarrow X=\varnothing \right)$$
12	11	necon3bid	$$⊢D\in \mathrm{Met}\left(X\right)\to \left(D\ne \varnothing \leftrightarrow X\ne \varnothing \right)$$