Metamath Proof Explorer

Theorem xmetdmdm

Description: Recover the base set from an extended metric. (Contributed by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion xmetdmdm 
|- ( D e. ( *Met ` X ) -> X = dom dom D )

Proof

Step Hyp Ref Expression
1 xmetf 
 |-  ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* )
2 1 fdmd 
 |-  ( D e. ( *Met ` X ) -> dom D = ( X X. X ) )
3 2 dmeqd 
 |-  ( D e. ( *Met ` X ) -> dom dom D = dom ( X X. X ) )
4 dmxpid 
 |-  dom ( X X. X ) = X
5 3 4 eqtr2di 
 |-  ( D e. ( *Met ` X ) -> X = dom dom D )