Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pstmfval Structured version   Visualization version   Unicode version

Theorem pstmfval 28699
Description: Function value of the metric induced by a pseudometric  D (Contributed by Thierry Arnoux, 11-Feb-2018.)
Hypothesis
Ref Expression
pstmval.1  |-  .~  =  (~Met `  D )
Assertion
Ref Expression
pstmfval  |-  ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  ->  ( [ A ]  .~  (pstoMet `  D ) [ B ]  .~  )  =  ( A D B ) )

Proof of Theorem pstmfval
Dummy variables  a 
b  x  y  z  e  f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pstmval.1 . . . . 5  |-  .~  =  (~Met `  D )
21pstmval 28698 . . . 4  |-  ( D  e.  (PsMet `  X
)  ->  (pstoMet `  D
)  =  ( x  e.  ( X /.  .~  ) ,  y  e.  ( X /.  .~  )  |->  U. { z  |  E. a  e.  x  E. b  e.  y 
z  =  ( a D b ) } ) )
323ad2ant1 1029 . . 3  |-  ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  ->  (pstoMet `  D )  =  ( x  e.  ( X /.  .~  ) ,  y  e.  ( X /.  .~  )  |->  U. { z  |  E. a  e.  x  E. b  e.  y  z  =  ( a D b ) } ) )
43oveqd 6307 . 2  |-  ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  ->  ( [ A ]  .~  (pstoMet `  D ) [ B ]  .~  )  =  ( [ A ]  .~  ( x  e.  ( X /.  .~  ) ,  y  e.  ( X /.  .~  )  |->  U. { z  |  E. a  e.  x  E. b  e.  y  z  =  ( a D b ) } ) [ B ]  .~  ) )
5 fvex 5875 . . . . . 6  |-  (~Met `  D )  e.  _V
61, 5eqeltri 2525 . . . . 5  |-  .~  e.  _V
76ecelqsi 7419 . . . 4  |-  ( A  e.  X  ->  [ A ]  .~  e.  ( X /.  .~  ) )
873ad2ant2 1030 . . 3  |-  ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  ->  [ A ]  .~  e.  ( X /.  .~  ) )
96ecelqsi 7419 . . . 4  |-  ( B  e.  X  ->  [ B ]  .~  e.  ( X /.  .~  ) )
1093ad2ant3 1031 . . 3  |-  ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  ->  [ B ]  .~  e.  ( X /.  .~  ) )
11 rexeq 2988 . . . . . 6  |-  ( x  =  [ A ]  .~  ->  ( E. a  e.  x  E. b  e.  y  z  =  ( a D b )  <->  E. a  e.  [  A ]  .~  E. b  e.  y  z  =  ( a D b ) ) )
1211abbidv 2569 . . . . 5  |-  ( x  =  [ A ]  .~  ->  { z  |  E. a  e.  x  E. b  e.  y 
z  =  ( a D b ) }  =  { z  |  E. a  e.  [  A ]  .~  E. b  e.  y  z  =  ( a D b ) } )
1312unieqd 4208 . . . 4  |-  ( x  =  [ A ]  .~  ->  U. { z  |  E. a  e.  x  E. b  e.  y 
z  =  ( a D b ) }  =  U. { z  |  E. a  e. 
[  A ]  .~  E. b  e.  y  z  =  ( a D b ) } )
14 rexeq 2988 . . . . . . 7  |-  ( y  =  [ B ]  .~  ->  ( E. b  e.  y  z  =  ( a D b )  <->  E. b  e.  [  B ]  .~  z  =  ( a D b ) ) )
1514rexbidv 2901 . . . . . 6  |-  ( y  =  [ B ]  .~  ->  ( E. a  e.  [  A ]  .~  E. b  e.  y  z  =  ( a D b )  <->  E. a  e.  [  A ]  .~  E. b  e.  [  B ]  .~  z  =  ( a D b ) ) )
1615abbidv 2569 . . . . 5  |-  ( y  =  [ B ]  .~  ->  { z  |  E. a  e.  [  A ]  .~  E. b  e.  y  z  =  ( a D b ) }  =  {
z  |  E. a  e.  [  A ]  .~  E. b  e.  [  B ]  .~  z  =  ( a D b ) } )
1716unieqd 4208 . . . 4  |-  ( y  =  [ B ]  .~  ->  U. { z  |  E. a  e.  [  A ]  .~  E. b  e.  y  z  =  ( a D b ) }  =  U. { z  |  E. a  e.  [  A ]  .~  E. b  e. 
[  B ]  .~  z  =  ( a D b ) } )
18 eqid 2451 . . . 4  |-  ( x  e.  ( X /.  .~  ) ,  y  e.  ( X /.  .~  )  |->  U. { z  |  E. a  e.  x  E. b  e.  y 
z  =  ( a D b ) } )  =  ( x  e.  ( X /.  .~  ) ,  y  e.  ( X /.  .~  )  |->  U. { z  |  E. a  e.  x  E. b  e.  y 
z  =  ( a D b ) } )
19 ecexg 7367 . . . . . . 7  |-  (  .~  e.  _V  ->  [ A ]  .~  e.  _V )
206, 19ax-mp 5 . . . . . 6  |-  [ A ]  .~  e.  _V
21 ecexg 7367 . . . . . . 7  |-  (  .~  e.  _V  ->  [ B ]  .~  e.  _V )
226, 21ax-mp 5 . . . . . 6  |-  [ B ]  .~  e.  _V
2320, 22ab2rexex 6784 . . . . 5  |-  { z  |  E. a  e. 
[  A ]  .~  E. b  e.  [  B ]  .~  z  =  ( a D b ) }  e.  _V
2423uniex 6587 . . . 4  |-  U. {
z  |  E. a  e.  [  A ]  .~  E. b  e.  [  B ]  .~  z  =  ( a D b ) }  e.  _V
2513, 17, 18, 24ovmpt2 6432 . . 3  |-  ( ( [ A ]  .~  e.  ( X /.  .~  )  /\  [ B ]  .~  e.  ( X /.  .~  ) )  ->  ( [ A ]  .~  (
x  e.  ( X /.  .~  ) ,  y  e.  ( X /.  .~  )  |->  U. { z  |  E. a  e.  x  E. b  e.  y  z  =  ( a D b ) } ) [ B ]  .~  )  =  U. { z  |  E. a  e. 
[  A ]  .~  E. b  e.  [  B ]  .~  z  =  ( a D b ) } )
268, 10, 25syl2anc 667 . 2  |-  ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  ->  ( [ A ]  .~  (
x  e.  ( X /.  .~  ) ,  y  e.  ( X /.  .~  )  |->  U. { z  |  E. a  e.  x  E. b  e.  y  z  =  ( a D b ) } ) [ B ]  .~  )  =  U. { z  |  E. a  e. 
[  A ]  .~  E. b  e.  [  B ]  .~  z  =  ( a D b ) } )
27 simpr3 1016 . . . . . . . . . . 11  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  (
e  e.  [ A ]  .~  /\  f  e. 
[ B ]  .~  /\  z  =  ( e D f ) ) )  ->  z  =  ( e D f ) )
28 simpl1 1011 . . . . . . . . . . . 12  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  (
e  e.  [ A ]  .~  /\  f  e. 
[ B ]  .~  /\  z  =  ( e D f ) ) )  ->  D  e.  (PsMet `  X ) )
29 simpr1 1014 . . . . . . . . . . . . . 14  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  (
e  e.  [ A ]  .~  /\  f  e. 
[ B ]  .~  /\  z  =  ( e D f ) ) )  ->  e  e.  [ A ]  .~  )
30 metidss 28694 . . . . . . . . . . . . . . . . . . . 20  |-  ( D  e.  (PsMet `  X
)  ->  (~Met `  D
)  C_  ( X  X.  X ) )
311, 30syl5eqss 3476 . . . . . . . . . . . . . . . . . . 19  |-  ( D  e.  (PsMet `  X
)  ->  .~  C_  ( X  X.  X ) )
32 xpss 4941 . . . . . . . . . . . . . . . . . . 19  |-  ( X  X.  X )  C_  ( _V  X.  _V )
3331, 32syl6ss 3444 . . . . . . . . . . . . . . . . . 18  |-  ( D  e.  (PsMet `  X
)  ->  .~  C_  ( _V  X.  _V ) )
34 df-rel 4841 . . . . . . . . . . . . . . . . . 18  |-  ( Rel 
.~ 
<->  .~  C_  ( _V  X.  _V ) )
3533, 34sylibr 216 . . . . . . . . . . . . . . . . 17  |-  ( D  e.  (PsMet `  X
)  ->  Rel  .~  )
36353ad2ant1 1029 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  ->  Rel  .~  )
3736adantr 467 . . . . . . . . . . . . . . 15  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  (
e  e.  [ A ]  .~  /\  f  e. 
[ B ]  .~  /\  z  =  ( e D f ) ) )  ->  Rel  .~  )
38 relelec 7404 . . . . . . . . . . . . . . 15  |-  ( Rel 
.~  ->  ( e  e. 
[ A ]  .~  <->  A  .~  e ) )
3937, 38syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  (
e  e.  [ A ]  .~  /\  f  e. 
[ B ]  .~  /\  z  =  ( e D f ) ) )  ->  ( e  e.  [ A ]  .~  <->  A  .~  e ) )
4029, 39mpbid 214 . . . . . . . . . . . . 13  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  (
e  e.  [ A ]  .~  /\  f  e. 
[ B ]  .~  /\  z  =  ( e D f ) ) )  ->  A  .~  e )
411breqi 4408 . . . . . . . . . . . . 13  |-  ( A  .~  e  <->  A (~Met `  D ) e )
4240, 41sylib 200 . . . . . . . . . . . 12  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  (
e  e.  [ A ]  .~  /\  f  e. 
[ B ]  .~  /\  z  =  ( e D f ) ) )  ->  A (~Met `  D ) e )
43 simpr2 1015 . . . . . . . . . . . . . 14  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  (
e  e.  [ A ]  .~  /\  f  e. 
[ B ]  .~  /\  z  =  ( e D f ) ) )  ->  f  e.  [ B ]  .~  )
44 relelec 7404 . . . . . . . . . . . . . . 15  |-  ( Rel 
.~  ->  ( f  e. 
[ B ]  .~  <->  B  .~  f ) )
4537, 44syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  (
e  e.  [ A ]  .~  /\  f  e. 
[ B ]  .~  /\  z  =  ( e D f ) ) )  ->  ( f  e.  [ B ]  .~  <->  B  .~  f ) )
4643, 45mpbid 214 . . . . . . . . . . . . 13  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  (
e  e.  [ A ]  .~  /\  f  e. 
[ B ]  .~  /\  z  =  ( e D f ) ) )  ->  B  .~  f )
471breqi 4408 . . . . . . . . . . . . 13  |-  ( B  .~  f  <->  B (~Met `  D ) f )
4846, 47sylib 200 . . . . . . . . . . . 12  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  (
e  e.  [ A ]  .~  /\  f  e. 
[ B ]  .~  /\  z  =  ( e D f ) ) )  ->  B (~Met `  D ) f )
49 metideq 28696 . . . . . . . . . . . 12  |-  ( ( D  e.  (PsMet `  X )  /\  ( A (~Met `  D )
e  /\  B (~Met `  D ) f ) )  ->  ( A D B )  =  ( e D f ) )
5028, 42, 48, 49syl12anc 1266 . . . . . . . . . . 11  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  (
e  e.  [ A ]  .~  /\  f  e. 
[ B ]  .~  /\  z  =  ( e D f ) ) )  ->  ( A D B )  =  ( e D f ) )
5127, 50eqtr4d 2488 . . . . . . . . . 10  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  (
e  e.  [ A ]  .~  /\  f  e. 
[ B ]  .~  /\  z  =  ( e D f ) ) )  ->  z  =  ( A D B ) )
5251adantlr 721 . . . . . . . . 9  |-  ( ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X
)  /\  E. a  e.  [  A ]  .~  E. b  e.  [  B ]  .~  z  =  ( a D b ) )  /\  ( e  e.  [ A ]  .~  /\  f  e.  [ B ]  .~  /\  z  =  ( e D f ) ) )  ->  z  =  ( A D B ) )
53523anassrs 1232 . . . . . . . 8  |-  ( ( ( ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  E. a  e.  [  A ]  .~  E. b  e. 
[  B ]  .~  z  =  ( a D b ) )  /\  e  e.  [ A ]  .~  )  /\  f  e.  [ B ]  .~  )  /\  z  =  ( e D f ) )  -> 
z  =  ( A D B ) )
54 oveq1 6297 . . . . . . . . . . . 12  |-  ( a  =  e  ->  (
a D b )  =  ( e D b ) )
5554eqeq2d 2461 . . . . . . . . . . 11  |-  ( a  =  e  ->  (
z  =  ( a D b )  <->  z  =  ( e D b ) ) )
56 oveq2 6298 . . . . . . . . . . . 12  |-  ( b  =  f  ->  (
e D b )  =  ( e D f ) )
5756eqeq2d 2461 . . . . . . . . . . 11  |-  ( b  =  f  ->  (
z  =  ( e D b )  <->  z  =  ( e D f ) ) )
5855, 57cbvrex2v 3028 . . . . . . . . . 10  |-  ( E. a  e.  [  A ]  .~  E. b  e. 
[  B ]  .~  z  =  ( a D b )  <->  E. e  e.  [  A ]  .~  E. f  e.  [  B ]  .~  z  =  ( e D f ) )
5958biimpi 198 . . . . . . . . 9  |-  ( E. a  e.  [  A ]  .~  E. b  e. 
[  B ]  .~  z  =  ( a D b )  ->  E. e  e.  [  A ]  .~  E. f  e. 
[  B ]  .~  z  =  ( e D f ) )
6059adantl 468 . . . . . . . 8  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  E. a  e.  [  A ]  .~  E. b  e. 
[  B ]  .~  z  =  ( a D b ) )  ->  E. e  e.  [  A ]  .~  E. f  e.  [  B ]  .~  z  =  ( e D f ) )
6153, 60r19.29vva 2934 . . . . . . 7  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  E. a  e.  [  A ]  .~  E. b  e. 
[  B ]  .~  z  =  ( a D b ) )  ->  z  =  ( A D B ) )
62 simpl1 1011 . . . . . . . . . 10  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  ->  D  e.  (PsMet `  X
) )
63 simpl2 1012 . . . . . . . . . 10  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  ->  A  e.  X )
64 psmet0 21324 . . . . . . . . . 10  |-  ( ( D  e.  (PsMet `  X )  /\  A  e.  X )  ->  ( A D A )  =  0 )
6562, 63, 64syl2anc 667 . . . . . . . . 9  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  -> 
( A D A )  =  0 )
66 relelec 7404 . . . . . . . . . . 11  |-  ( Rel 
.~  ->  ( A  e. 
[ A ]  .~  <->  A  .~  A ) )
6762, 35, 663syl 18 . . . . . . . . . 10  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  -> 
( A  e.  [ A ]  .~  <->  A  .~  A ) )
681a1i 11 . . . . . . . . . . 11  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  ->  .~  =  (~Met `  D
) )
6968breqd 4413 . . . . . . . . . 10  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  -> 
( A  .~  A  <->  A (~Met `  D ) A ) )
70 metidv 28695 . . . . . . . . . . 11  |-  ( ( D  e.  (PsMet `  X )  /\  ( A  e.  X  /\  A  e.  X )
)  ->  ( A
(~Met `  D ) A 
<->  ( A D A )  =  0 ) )
7162, 63, 63, 70syl12anc 1266 . . . . . . . . . 10  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  -> 
( A (~Met `  D ) A  <->  ( A D A )  =  0 ) )
7267, 69, 713bitrd 283 . . . . . . . . 9  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  -> 
( A  e.  [ A ]  .~  <->  ( A D A )  =  0 ) )
7365, 72mpbird 236 . . . . . . . 8  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  ->  A  e.  [ A ]  .~  )
74 simpl3 1013 . . . . . . . . . 10  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  ->  B  e.  X )
75 psmet0 21324 . . . . . . . . . 10  |-  ( ( D  e.  (PsMet `  X )  /\  B  e.  X )  ->  ( B D B )  =  0 )
7662, 74, 75syl2anc 667 . . . . . . . . 9  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  -> 
( B D B )  =  0 )
77 relelec 7404 . . . . . . . . . . 11  |-  ( Rel 
.~  ->  ( B  e. 
[ B ]  .~  <->  B  .~  B ) )
7862, 35, 773syl 18 . . . . . . . . . 10  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  -> 
( B  e.  [ B ]  .~  <->  B  .~  B ) )
7968breqd 4413 . . . . . . . . . 10  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  -> 
( B  .~  B  <->  B (~Met `  D ) B ) )
80 metidv 28695 . . . . . . . . . . 11  |-  ( ( D  e.  (PsMet `  X )  /\  ( B  e.  X  /\  B  e.  X )
)  ->  ( B
(~Met `  D ) B 
<->  ( B D B )  =  0 ) )
8162, 74, 74, 80syl12anc 1266 . . . . . . . . . 10  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  -> 
( B (~Met `  D ) B  <->  ( B D B )  =  0 ) )
8278, 79, 813bitrd 283 . . . . . . . . 9  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  -> 
( B  e.  [ B ]  .~  <->  ( B D B )  =  0 ) )
8376, 82mpbird 236 . . . . . . . 8  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  ->  B  e.  [ B ]  .~  )
84 simpr 463 . . . . . . . 8  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  -> 
z  =  ( A D B ) )
85 rspceov 6329 . . . . . . . 8  |-  ( ( A  e.  [ A ]  .~  /\  B  e. 
[ B ]  .~  /\  z  =  ( A D B ) )  ->  E. a  e.  [  A ]  .~  E. b  e.  [  B ]  .~  z  =  ( a D b ) )
8673, 83, 84, 85syl3anc 1268 . . . . . . 7  |-  ( ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  /\  z  =  ( A D B ) )  ->  E. a  e.  [  A ]  .~  E. b  e. 
[  B ]  .~  z  =  ( a D b ) )
8761, 86impbida 843 . . . . . 6  |-  ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  ->  ( E. a  e.  [  A ]  .~  E. b  e. 
[  B ]  .~  z  =  ( a D b )  <->  z  =  ( A D B ) ) )
8887abbidv 2569 . . . . 5  |-  ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  ->  { z  |  E. a  e. 
[  A ]  .~  E. b  e.  [  B ]  .~  z  =  ( a D b ) }  =  { z  |  z  =  ( A D B ) } )
89 df-sn 3969 . . . . 5  |-  { ( A D B ) }  =  { z  |  z  =  ( A D B ) }
9088, 89syl6eqr 2503 . . . 4  |-  ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  ->  { z  |  E. a  e. 
[  A ]  .~  E. b  e.  [  B ]  .~  z  =  ( a D b ) }  =  { ( A D B ) } )
9190unieqd 4208 . . 3  |-  ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  ->  U. {
z  |  E. a  e.  [  A ]  .~  E. b  e.  [  B ]  .~  z  =  ( a D b ) }  =  U. {
( A D B ) } )
92 ovex 6318 . . . 4  |-  ( A D B )  e. 
_V
9392unisn 4213 . . 3  |-  U. {
( A D B ) }  =  ( A D B )
9491, 93syl6eq 2501 . 2  |-  ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  ->  U. {
z  |  E. a  e.  [  A ]  .~  E. b  e.  [  B ]  .~  z  =  ( a D b ) }  =  ( A D B ) )
954, 26, 943eqtrd 2489 1  |-  ( ( D  e.  (PsMet `  X )  /\  A  e.  X  /\  B  e.  X )  ->  ( [ A ]  .~  (pstoMet `  D ) [ B ]  .~  )  =  ( A D B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    /\ w3a 985    = wceq 1444    e. wcel 1887   {cab 2437   E.wrex 2738   _Vcvv 3045    C_ wss 3404   {csn 3968   U.cuni 4198   class class class wbr 4402    X. cxp 4832   Rel wrel 4839   ` cfv 5582  (class class class)co 6290    |-> cmpt2 6292   [cec 7361   /.cqs 7362   0cc0 9539  PsMetcpsmet 18954  ~Metcmetid 28689  pstoMetcpstm 28690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-po 4755  df-so 4756  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-1st 6793  df-2nd 6794  df-er 7363  df-ec 7365  df-qs 7369  df-map 7474  df-en 7570  df-dom 7571  df-sdom 7572  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-xadd 11410  df-psmet 18962  df-metid 28691  df-pstm 28692
This theorem is referenced by:  pstmxmet  28700
  Copyright terms: Public domain W3C validator