Metamath Proof Explorer

Theorem psmetdmdm

Description: Recover the base set from a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion psmetdmdm 
|- ( D e. ( PsMet ` X ) -> X = dom dom D )

Proof

Step Hyp Ref Expression
1 elfvex 
 |-  ( D e. ( PsMet ` X ) -> X e. _V )
2 ispsmet 
 |-  ( X e. _V -> ( D e. ( PsMet ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X ( ( x D x ) = 0 /\ A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
3 2 biimpa 
 |-  ( ( X e. _V /\ D e. ( PsMet ` X ) ) -> ( D : ( X X. X ) --> RR* /\ A. x e. X ( ( x D x ) = 0 /\ A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) )
4 1 3 mpancom 
 |-  ( D e. ( PsMet ` X ) -> ( D : ( X X. X ) --> RR* /\ A. x e. X ( ( x D x ) = 0 /\ A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) )
5 4 simpld 
 |-  ( D e. ( PsMet ` X ) -> D : ( X X. X ) --> RR* )
6 fdm 
 |-  ( D : ( X X. X ) --> RR* -> dom D = ( X X. X ) )
7 6 dmeqd 
 |-  ( D : ( X X. X ) --> RR* -> dom dom D = dom ( X X. X ) )
8 5 7 syl 
 |-  ( D e. ( PsMet ` X ) -> dom dom D = dom ( X X. X ) )
9 dmxpid 
 |-  dom ( X X. X ) = X
10 8 9 eqtr2di 
 |-  ( D e. ( PsMet ` X ) -> X = dom dom D )