Metamath Proof Explorer

Theorem metidval

Description: Value of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion metidval 
|- ( D e. ( PsMet ` X ) -> ( ~Met ` D ) = { <. x , y >. | ( ( x e. X /\ y e. X ) /\ ( x D y ) = 0 ) } )

Proof

Step Hyp Ref Expression
1 df-metid 
 |-  ~Met = ( d e. U. ran PsMet |-> { <. x , y >. | ( ( x e. dom dom d /\ y e. dom dom d ) /\ ( x d y ) = 0 ) } )
2 1 a1i 
 |-  ( D e. ( PsMet ` X ) -> ~Met = ( d e. U. ran PsMet |-> { <. x , y >. | ( ( x e. dom dom d /\ y e. dom dom d ) /\ ( x d y ) = 0 ) } ) )
3 simpr 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> d = D )
4 3 dmeqd 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> dom d = dom D )
5 4 dmeqd 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> dom dom d = dom dom D )
6 psmetdmdm 
 |-  ( D e. ( PsMet ` X ) -> X = dom dom D )
7 6 adantr 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> X = dom dom D )
8 5 7 eqtr4d 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> dom dom d = X )
9 8 eleq2d 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( x e. dom dom d <-> x e. X ) )
10 8 eleq2d 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( y e. dom dom d <-> y e. X ) )
11 9 10 anbi12d 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( ( x e. dom dom d /\ y e. dom dom d ) <-> ( x e. X /\ y e. X ) ) )
12 3 oveqd 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( x d y ) = ( x D y ) )
13 12 eqeq1d 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( ( x d y ) = 0 <-> ( x D y ) = 0 ) )
14 11 13 anbi12d 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( ( ( x e. dom dom d /\ y e. dom dom d ) /\ ( x d y ) = 0 ) <-> ( ( x e. X /\ y e. X ) /\ ( x D y ) = 0 ) ) )
15 14 opabbidv 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> { <. x , y >. | ( ( x e. dom dom d /\ y e. dom dom d ) /\ ( x d y ) = 0 ) } = { <. x , y >. | ( ( x e. X /\ y e. X ) /\ ( x D y ) = 0 ) } )
16 elfvdm 
 |-  ( D e. ( PsMet ` X ) -> X e. dom PsMet )
17 fveq2 
 |-  ( x = X -> ( PsMet ` x ) = ( PsMet ` X ) )
18 17 eleq2d 
 |-  ( x = X -> ( D e. ( PsMet ` x ) <-> D e. ( PsMet ` X ) ) )
19 18 rspcev 
 |-  ( ( X e. dom PsMet /\ D e. ( PsMet ` X ) ) -> E. x e. dom PsMet D e. ( PsMet ` x ) )
20 16 19 mpancom 
 |-  ( D e. ( PsMet ` X ) -> E. x e. dom PsMet D e. ( PsMet ` x ) )
21 df-psmet 
 |-  PsMet = ( x e. _V |-> { d e. ( RR* ^m ( x X. x ) ) | A. y e. x ( ( y d y ) = 0 /\ A. z e. x A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } )
22 21 funmpt2 
 |-  Fun PsMet
23 elunirn 
 |-  ( Fun PsMet -> ( D e. U. ran PsMet <-> E. x e. dom PsMet D e. ( PsMet ` x ) ) )
24 22 23 ax-mp 
 |-  ( D e. U. ran PsMet <-> E. x e. dom PsMet D e. ( PsMet ` x ) )
25 20 24 sylibr 
 |-  ( D e. ( PsMet ` X ) -> D e. U. ran PsMet )
26 opabssxp 
 |-  { <. x , y >. | ( ( x e. X /\ y e. X ) /\ ( x D y ) = 0 ) } C_ ( X X. X )
27 elfvex 
 |-  ( D e. ( PsMet ` X ) -> X e. _V )
28 27 27 xpexd 
 |-  ( D e. ( PsMet ` X ) -> ( X X. X ) e. _V )
29 ssexg 
 |-  ( ( { <. x , y >. | ( ( x e. X /\ y e. X ) /\ ( x D y ) = 0 ) } C_ ( X X. X ) /\ ( X X. X ) e. _V ) -> { <. x , y >. | ( ( x e. X /\ y e. X ) /\ ( x D y ) = 0 ) } e. _V )
30 26 28 29 sylancr 
 |-  ( D e. ( PsMet ` X ) -> { <. x , y >. | ( ( x e. X /\ y e. X ) /\ ( x D y ) = 0 ) } e. _V )
31 2 15 25 30 fvmptd 
 |-  ( D e. ( PsMet ` X ) -> ( ~Met ` D ) = { <. x , y >. | ( ( x e. X /\ y e. X ) /\ ( x D y ) = 0 ) } )