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 simpr 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> d = D )
3 2 dmeqd 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> dom d = dom D )
4 3 dmeqd 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> dom dom d = dom dom D )
5 psmetdmdm 
 |-  ( D e. ( PsMet ` X ) -> X = dom dom D )
6 5 adantr 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> X = dom dom D )
7 4 6 eqtr4d 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> dom dom d = X )
8 7 eleq2d 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( x e. dom dom d <-> x e. X ) )
9 7 eleq2d 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( y e. dom dom d <-> y e. X ) )
10 8 9 anbi12d 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( ( x e. dom dom d /\ y e. dom dom d ) <-> ( x e. X /\ y e. X ) ) )
11 2 oveqd 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( x d y ) = ( x D y ) )
12 11 eqeq1d 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( ( x d y ) = 0 <-> ( x D y ) = 0 ) )
13 10 12 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 ) ) )
14 13 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 ) } )
15 elfvunirn 
 |-  ( D e. ( PsMet ` X ) -> D e. U. ran PsMet )
16 opabssxp 
 |-  { <. x , y >. | ( ( x e. X /\ y e. X ) /\ ( x D y ) = 0 ) } C_ ( X X. X )
17 elfvex 
 |-  ( D e. ( PsMet ` X ) -> X e. _V )
18 17 17 xpexd 
 |-  ( D e. ( PsMet ` X ) -> ( X X. X ) e. _V )
19 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 )
20 16 18 19 sylancr 
 |-  ( D e. ( PsMet ` X ) -> { <. x , y >. | ( ( x e. X /\ y e. X ) /\ ( x D y ) = 0 ) } e. _V )
21 1 14 15 20 fvmptd2 
 |-  ( D e. ( PsMet ` X ) -> ( ~Met ` D ) = { <. x , y >. | ( ( x e. X /\ y e. X ) /\ ( x D y ) = 0 ) } )