Theorem 0met

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

	Ref	Expression
Assertion	0met	|- (/) e. ( Met ` (/) )

Proof

Step	Hyp	Ref	Expression
1		0ex	|- (/) e. _V
2		f0	|- (/) : (/) --> RR
3		xp0	|- ( (/) X. (/) ) = (/)
4	3	feq2i	|- ( (/) : ( (/) X. (/) ) --> RR <-> (/) : (/) --> RR )
5	2 4	mpbir	|- (/) : ( (/) X. (/) ) --> RR
6		noel	|- -. x e. (/)
7	6	pm2.21i	|- ( x e. (/) -> ( ( x (/) y ) = 0 <-> x = y ) )
8	7	adantr	|- ( ( x e. (/) /\ y e. (/) ) -> ( ( x (/) y ) = 0 <-> x = y ) )
9	6	pm2.21i	|- ( x e. (/) -> ( x (/) y ) <_ ( ( z (/) x ) + ( z (/) y ) ) )
10	9	3ad2ant1	|- ( ( x e. (/) /\ y e. (/) /\ z e. (/) ) -> ( x (/) y ) <_ ( ( z (/) x ) + ( z (/) y ) ) )
11	1 5 8 10	ismeti	|- (/) e. ( Met ` (/) )