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

Metamath Proof Explorer

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 ` (/) )