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