Metamath Proof Explorer

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 e. ( Met ` X ) -> ( D =/= (/) <-> X =/= (/) ) )

Proof

Step Hyp Ref Expression
1 metf 
 |-  ( D e. ( Met ` X ) -> D : ( X X. X ) --> RR )
2 frel 
 |-  ( D : ( X X. X ) --> RR -> Rel D )
3 reldm0 
 |-  ( Rel D -> ( D = (/) <-> dom D = (/) ) )
4 1 2 3 3syl 
 |-  ( D e. ( Met ` X ) -> ( D = (/) <-> dom D = (/) ) )
5 1 fdmd 
 |-  ( D e. ( Met ` X ) -> dom D = ( X X. X ) )
6 5 eqeq1d 
 |-  ( D e. ( Met ` X ) -> ( dom D = (/) <-> ( X X. X ) = (/) ) )
7 4 6 bitrd 
 |-  ( D e. ( Met ` X ) -> ( D = (/) <-> ( X X. X ) = (/) ) )
8 xpeq0 
 |-  ( ( X X. X ) = (/) <-> ( X = (/) \/ X = (/) ) )
9 oridm 
 |-  ( ( X = (/) \/ X = (/) ) <-> X = (/) )
10 8 9 bitri 
 |-  ( ( X X. X ) = (/) <-> X = (/) )
11 7 10 bitrdi 
 |-  ( D e. ( Met ` X ) -> ( D = (/) <-> X = (/) ) )
12 11 necon3bid 
 |-  ( D e. ( Met ` X ) -> ( D =/= (/) <-> X =/= (/) ) )