Theorem 0met

Description: The empty metric. (Contributed by NM, 30-Aug-2006) (Revised by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	0met	$$⊢\varnothing \in \mathrm{Met}\left(\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2		f0	$$⊢\varnothing :\varnothing ⟶ℝ$$
3		xp0	$$⊢\varnothing \times \varnothing =\varnothing$$
4	3	feq2i	$$⊢\varnothing :\varnothing \times \varnothing ⟶ℝ\leftrightarrow \varnothing :\varnothing ⟶ℝ$$
5	2 4	mpbir	$$⊢\varnothing :\varnothing \times \varnothing ⟶ℝ$$
6		noel	$$⊢\neg x\in \varnothing$$
7	6	pm2.21i	$$⊢x\in \varnothing \to \left(x\varnothing y=0\leftrightarrow x=y\right)$$
8	7	adantr	$$⊢\left(x\in \varnothing \wedge y\in \varnothing \right)\to \left(x\varnothing y=0\leftrightarrow x=y\right)$$
9	6	pm2.21i	$$⊢x\in \varnothing \to x\varnothing y\le \left(z\varnothing x\right)+\left(z\varnothing y\right)$$
10	9	3ad2ant1	$$⊢\left(x\in \varnothing \wedge y\in \varnothing \wedge z\in \varnothing \right)\to x\varnothing y\le \left(z\varnothing x\right)+\left(z\varnothing y\right)$$
11	1 5 8 10	ismeti	$$⊢\varnothing \in \mathrm{Met}\left(\varnothing \right)$$