ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ismet Unicode version

Theorem ismet 13138
Description: Express the predicate " D is a metric". (Contributed by NM, 25-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
Assertion
Ref Expression
ismet  |-  ( X  e.  A  ->  ( D  e.  ( Met `  X )  <->  ( D : ( X  X.  X ) --> RR  /\  A. x  e.  X  A. y  e.  X  (
( ( x D y )  =  0  <-> 
x  =  y )  /\  A. z  e.  X  ( x D y )  <_  (
( z D x )  +  ( z D y ) ) ) ) ) )
Distinct variable groups:    x, y, z, D    x, X, y, z
Allowed substitution hints:    A( x, y, z)

Proof of Theorem ismet
Dummy variables  d  t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 2741 . . . . 5  |-  ( X  e.  A  ->  X  e.  _V )
2 fnmap 6633 . . . . . . . 8  |-  ^m  Fn  ( _V  X.  _V )
3 reex 7908 . . . . . . . 8  |-  RR  e.  _V
4 sqxpexg 4727 . . . . . . . 8  |-  ( X  e.  _V  ->  ( X  X.  X )  e. 
_V )
5 fnovex 5886 . . . . . . . 8  |-  ( (  ^m  Fn  ( _V 
X.  _V )  /\  RR  e.  _V  /\  ( X  X.  X )  e. 
_V )  ->  ( RR  ^m  ( X  X.  X ) )  e. 
_V )
62, 3, 4, 5mp3an12i 1336 . . . . . . 7  |-  ( X  e.  _V  ->  ( RR  ^m  ( X  X.  X ) )  e. 
_V )
7 rabexg 4132 . . . . . . 7  |-  ( ( RR  ^m  ( X  X.  X ) )  e.  _V  ->  { d  e.  ( RR  ^m  ( X  X.  X
) )  |  A. x  e.  X  A. y  e.  X  (
( ( x d y )  =  0  <-> 
x  =  y )  /\  A. z  e.  X  ( x d y )  <_  (
( z d x )  +  ( z d y ) ) ) }  e.  _V )
86, 7syl 14 . . . . . 6  |-  ( X  e.  _V  ->  { d  e.  ( RR  ^m  ( X  X.  X
) )  |  A. x  e.  X  A. y  e.  X  (
( ( x d y )  =  0  <-> 
x  =  y )  /\  A. z  e.  X  ( x d y )  <_  (
( z d x )  +  ( z d y ) ) ) }  e.  _V )
9 xpeq12 4630 . . . . . . . . . 10  |-  ( ( t  =  X  /\  t  =  X )  ->  ( t  X.  t
)  =  ( X  X.  X ) )
109anidms 395 . . . . . . . . 9  |-  ( t  =  X  ->  (
t  X.  t )  =  ( X  X.  X ) )
1110oveq2d 5869 . . . . . . . 8  |-  ( t  =  X  ->  ( RR  ^m  ( t  X.  t ) )  =  ( RR  ^m  ( X  X.  X ) ) )
12 raleq 2665 . . . . . . . . . . 11  |-  ( t  =  X  ->  ( A. z  e.  t 
( x d y )  <_  ( (
z d x )  +  ( z d y ) )  <->  A. z  e.  X  ( x
d y )  <_ 
( ( z d x )  +  ( z d y ) ) ) )
1312anbi2d 461 . . . . . . . . . 10  |-  ( t  =  X  ->  (
( ( ( x d y )  =  0  <->  x  =  y
)  /\  A. z  e.  t  ( x
d y )  <_ 
( ( z d x )  +  ( z d y ) ) )  <->  ( (
( x d y )  =  0  <->  x  =  y )  /\  A. z  e.  X  ( x d y )  <_  ( ( z d x )  +  ( z d y ) ) ) ) )
1413raleqbi1dv 2673 . . . . . . . . 9  |-  ( t  =  X  ->  ( A. y  e.  t 
( ( ( x d y )  =  0  <->  x  =  y
)  /\  A. z  e.  t  ( x
d y )  <_ 
( ( z d x )  +  ( z d y ) ) )  <->  A. y  e.  X  ( (
( x d y )  =  0  <->  x  =  y )  /\  A. z  e.  X  ( x d y )  <_  ( ( z d x )  +  ( z d y ) ) ) ) )
1514raleqbi1dv 2673 . . . . . . . 8  |-  ( t  =  X  ->  ( A. x  e.  t  A. y  e.  t 
( ( ( x d y )  =  0  <->  x  =  y
)  /\  A. z  e.  t  ( x
d y )  <_ 
( ( z d x )  +  ( z d y ) ) )  <->  A. x  e.  X  A. y  e.  X  ( (
( x d y )  =  0  <->  x  =  y )  /\  A. z  e.  X  ( x d y )  <_  ( ( z d x )  +  ( z d y ) ) ) ) )
1611, 15rabeqbidv 2725 . . . . . . 7  |-  ( t  =  X  ->  { d  e.  ( RR  ^m  ( t  X.  t
) )  |  A. x  e.  t  A. y  e.  t  (
( ( x d y )  =  0  <-> 
x  =  y )  /\  A. z  e.  t  ( x d y )  <_  (
( z d x )  +  ( z d y ) ) ) }  =  {
d  e.  ( RR 
^m  ( X  X.  X ) )  | 
A. x  e.  X  A. y  e.  X  ( ( ( x d y )  =  0  <->  x  =  y
)  /\  A. z  e.  X  ( x
d y )  <_ 
( ( z d x )  +  ( z d y ) ) ) } )
17 df-met 12783 . . . . . . 7  |-  Met  =  ( t  e.  _V  |->  { d  e.  ( RR  ^m  ( t  X.  t ) )  |  A. x  e.  t  A. y  e.  t  ( ( ( x d y )  =  0  <->  x  =  y )  /\  A. z  e.  t  (
x d y )  <_  ( ( z d x )  +  ( z d y ) ) ) } )
1816, 17fvmptg 5572 . . . . . 6  |-  ( ( X  e.  _V  /\  { d  e.  ( RR 
^m  ( X  X.  X ) )  | 
A. x  e.  X  A. y  e.  X  ( ( ( x d y )  =  0  <->  x  =  y
)  /\  A. z  e.  X  ( x
d y )  <_ 
( ( z d x )  +  ( z d y ) ) ) }  e.  _V )  ->  ( Met `  X )  =  {
d  e.  ( RR 
^m  ( X  X.  X ) )  | 
A. x  e.  X  A. y  e.  X  ( ( ( x d y )  =  0  <->  x  =  y
)  /\  A. z  e.  X  ( x
d y )  <_ 
( ( z d x )  +  ( z d y ) ) ) } )
198, 18mpdan 419 . . . . 5  |-  ( X  e.  _V  ->  ( Met `  X )  =  { d  e.  ( RR  ^m  ( X  X.  X ) )  |  A. x  e.  X  A. y  e.  X  ( ( ( x d y )  =  0  <->  x  =  y )  /\  A. z  e.  X  (
x d y )  <_  ( ( z d x )  +  ( z d y ) ) ) } )
201, 19syl 14 . . . 4  |-  ( X  e.  A  ->  ( Met `  X )  =  { d  e.  ( RR  ^m  ( X  X.  X ) )  |  A. x  e.  X  A. y  e.  X  ( ( ( x d y )  =  0  <->  x  =  y )  /\  A. z  e.  X  (
x d y )  <_  ( ( z d x )  +  ( z d y ) ) ) } )
2120eleq2d 2240 . . 3  |-  ( X  e.  A  ->  ( D  e.  ( Met `  X )  <->  D  e.  { d  e.  ( RR 
^m  ( X  X.  X ) )  | 
A. x  e.  X  A. y  e.  X  ( ( ( x d y )  =  0  <->  x  =  y
)  /\  A. z  e.  X  ( x
d y )  <_ 
( ( z d x )  +  ( z d y ) ) ) } ) )
22 oveq 5859 . . . . . . . 8  |-  ( d  =  D  ->  (
x d y )  =  ( x D y ) )
2322eqeq1d 2179 . . . . . . 7  |-  ( d  =  D  ->  (
( x d y )  =  0  <->  (
x D y )  =  0 ) )
2423bibi1d 232 . . . . . 6  |-  ( d  =  D  ->  (
( ( x d y )  =  0  <-> 
x  =  y )  <-> 
( ( x D y )  =  0  <-> 
x  =  y ) ) )
25 oveq 5859 . . . . . . . . 9  |-  ( d  =  D  ->  (
z d x )  =  ( z D x ) )
26 oveq 5859 . . . . . . . . 9  |-  ( d  =  D  ->  (
z d y )  =  ( z D y ) )
2725, 26oveq12d 5871 . . . . . . . 8  |-  ( d  =  D  ->  (
( z d x )  +  ( z d y ) )  =  ( ( z D x )  +  ( z D y ) ) )
2822, 27breq12d 4002 . . . . . . 7  |-  ( d  =  D  ->  (
( x d y )  <_  ( (
z d x )  +  ( z d y ) )  <->  ( x D y )  <_ 
( ( z D x )  +  ( z D y ) ) ) )
2928ralbidv 2470 . . . . . 6  |-  ( d  =  D  ->  ( A. z  e.  X  ( x d y )  <_  ( (
z d x )  +  ( z d y ) )  <->  A. z  e.  X  ( x D y )  <_ 
( ( z D x )  +  ( z D y ) ) ) )
3024, 29anbi12d 470 . . . . 5  |-  ( d  =  D  ->  (
( ( ( x d y )  =  0  <->  x  =  y
)  /\  A. z  e.  X  ( x
d y )  <_ 
( ( z d x )  +  ( z d y ) ) )  <->  ( (
( x D y )  =  0  <->  x  =  y )  /\  A. z  e.  X  ( x D y )  <_  ( ( z D x )  +  ( z D y ) ) ) ) )
31302ralbidv 2494 . . . 4  |-  ( d  =  D  ->  ( A. x  e.  X  A. y  e.  X  ( ( ( x d y )  =  0  <->  x  =  y
)  /\  A. z  e.  X  ( x
d y )  <_ 
( ( z d x )  +  ( z d y ) ) )  <->  A. x  e.  X  A. y  e.  X  ( (
( x D y )  =  0  <->  x  =  y )  /\  A. z  e.  X  ( x D y )  <_  ( ( z D x )  +  ( z D y ) ) ) ) )
3231elrab 2886 . . 3  |-  ( D  e.  { d  e.  ( RR  ^m  ( X  X.  X ) )  |  A. x  e.  X  A. y  e.  X  ( ( ( x d y )  =  0  <->  x  =  y )  /\  A. z  e.  X  (
x d y )  <_  ( ( z d x )  +  ( z d y ) ) ) }  <-> 
( D  e.  ( RR  ^m  ( X  X.  X ) )  /\  A. x  e.  X  A. y  e.  X  ( ( ( x D y )  =  0  <->  x  =  y )  /\  A. z  e.  X  (
x D y )  <_  ( ( z D x )  +  ( z D y ) ) ) ) )
3321, 32bitrdi 195 . 2  |-  ( X  e.  A  ->  ( D  e.  ( Met `  X )  <->  ( D  e.  ( RR  ^m  ( X  X.  X ) )  /\  A. x  e.  X  A. y  e.  X  ( ( ( x D y )  =  0  <->  x  =  y )  /\  A. z  e.  X  (
x D y )  <_  ( ( z D x )  +  ( z D y ) ) ) ) ) )
34 sqxpexg 4727 . . . 4  |-  ( X  e.  A  ->  ( X  X.  X )  e. 
_V )
35 elmapg 6639 . . . 4  |-  ( ( RR  e.  _V  /\  ( X  X.  X
)  e.  _V )  ->  ( D  e.  ( RR  ^m  ( X  X.  X ) )  <-> 
D : ( X  X.  X ) --> RR ) )
363, 34, 35sylancr 412 . . 3  |-  ( X  e.  A  ->  ( D  e.  ( RR  ^m  ( X  X.  X
) )  <->  D :
( X  X.  X
) --> RR ) )
3736anbi1d 462 . 2  |-  ( X  e.  A  ->  (
( D  e.  ( RR  ^m  ( X  X.  X ) )  /\  A. x  e.  X  A. y  e.  X  ( ( ( x D y )  =  0  <->  x  =  y )  /\  A. z  e.  X  (
x D y )  <_  ( ( z D x )  +  ( z D y ) ) ) )  <-> 
( D : ( X  X.  X ) --> RR  /\  A. x  e.  X  A. y  e.  X  ( (
( x D y )  =  0  <->  x  =  y )  /\  A. z  e.  X  ( x D y )  <_  ( ( z D x )  +  ( z D y ) ) ) ) ) )
3833, 37bitrd 187 1  |-  ( X  e.  A  ->  ( D  e.  ( Met `  X )  <->  ( D : ( X  X.  X ) --> RR  /\  A. x  e.  X  A. y  e.  X  (
( ( x D y )  =  0  <-> 
x  =  y )  /\  A. z  e.  X  ( x D y )  <_  (
( z D x )  +  ( z D y ) ) ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1348    e. wcel 2141   A.wral 2448   {crab 2452   _Vcvv 2730   class class class wbr 3989    X. cxp 4609    Fn wfn 5193   -->wf 5194   ` cfv 5198  (class class class)co 5853    ^m cmap 6626   RRcr 7773   0cc0 7774    + caddc 7777    <_ cle 7955   Metcmet 12775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-cnex 7865  ax-resscn 7866
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-id 4278  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-fv 5206  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-map 6628  df-met 12783
This theorem is referenced by:  ismeti  13140  metflem  13143  ismet2  13148
  Copyright terms: Public domain W3C validator