MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  blfvalps Unicode version

Theorem blfvalps 18366
Description: The value of the ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux, 11-Feb-2018.)
Assertion
Ref Expression
blfvalps  |-  ( D  e.  (PsMet `  X
)  ->  ( ball `  D )  =  ( x  e.  X , 
r  e.  RR*  |->  { y  e.  X  |  ( x D y )  <  r } ) )
Distinct variable groups:    x, r,
y, D    X, r, x, y

Proof of Theorem blfvalps
Dummy variable  d is distinct from all other variables.
StepHypRef Expression
1 df-bl 16652 . . 3  |-  ball  =  ( d  e.  _V  |->  ( x  e.  dom  dom  d ,  r  e. 
RR*  |->  { y  e. 
dom  dom  d  |  ( x d y )  <  r } ) )
21a1i 11 . 2  |-  ( D  e.  (PsMet `  X
)  ->  ball  =  ( d  e.  _V  |->  ( x  e.  dom  dom  d ,  r  e.  RR*  |->  { y  e.  dom  dom  d  |  ( x d y )  < 
r } ) ) )
3 dmeq 5029 . . . . 5  |-  ( d  =  D  ->  dom  d  =  dom  D )
43dmeqd 5031 . . . 4  |-  ( d  =  D  ->  dom  dom  d  =  dom  dom  D )
5 psmetdmdm 18289 . . . . 5  |-  ( D  e.  (PsMet `  X
)  ->  X  =  dom  dom  D )
65eqcomd 2409 . . . 4  |-  ( D  e.  (PsMet `  X
)  ->  dom  dom  D  =  X )
74, 6sylan9eqr 2458 . . 3  |-  ( ( D  e.  (PsMet `  X )  /\  d  =  D )  ->  dom  dom  d  =  X )
8 eqidd 2405 . . 3  |-  ( ( D  e.  (PsMet `  X )  /\  d  =  D )  ->  RR*  =  RR* )
9 simpr 448 . . . . . 6  |-  ( ( D  e.  (PsMet `  X )  /\  d  =  D )  ->  d  =  D )
109oveqd 6057 . . . . 5  |-  ( ( D  e.  (PsMet `  X )  /\  d  =  D )  ->  (
x d y )  =  ( x D y ) )
1110breq1d 4182 . . . 4  |-  ( ( D  e.  (PsMet `  X )  /\  d  =  D )  ->  (
( x d y )  <  r  <->  ( x D y )  < 
r ) )
127, 11rabeqbidv 2911 . . 3  |-  ( ( D  e.  (PsMet `  X )  /\  d  =  D )  ->  { y  e.  dom  dom  d  |  ( x d y )  <  r }  =  { y  e.  X  |  (
x D y )  <  r } )
137, 8, 12mpt2eq123dv 6095 . 2  |-  ( ( D  e.  (PsMet `  X )  /\  d  =  D )  ->  (
x  e.  dom  dom  d ,  r  e.  RR*  |->  { y  e.  dom  dom  d  |  ( x d y )  < 
r } )  =  ( x  e.  X ,  r  e.  RR*  |->  { y  e.  X  |  ( x D y )  <  r } ) )
14 elex 2924 . 2  |-  ( D  e.  (PsMet `  X
)  ->  D  e.  _V )
15 ssrab2 3388 . . . . . 6  |-  { y  e.  X  |  ( x D y )  <  r }  C_  X
16 elfvdm 5716 . . . . . . . 8  |-  ( D  e.  (PsMet `  X
)  ->  X  e.  dom PsMet )
1716adantr 452 . . . . . . 7  |-  ( ( D  e.  (PsMet `  X )  /\  (
x  e.  X  /\  r  e.  RR* ) )  ->  X  e.  dom PsMet )
18 elpw2g 4323 . . . . . . 7  |-  ( X  e.  dom PsMet  ->  ( { y  e.  X  | 
( x D y )  <  r }  e.  ~P X  <->  { y  e.  X  |  (
x D y )  <  r }  C_  X ) )
1917, 18syl 16 . . . . . 6  |-  ( ( D  e.  (PsMet `  X )  /\  (
x  e.  X  /\  r  e.  RR* ) )  ->  ( { y  e.  X  |  ( x D y )  <  r }  e.  ~P X  <->  { y  e.  X  |  ( x D y )  <  r }  C_  X ) )
2015, 19mpbiri 225 . . . . 5  |-  ( ( D  e.  (PsMet `  X )  /\  (
x  e.  X  /\  r  e.  RR* ) )  ->  { y  e.  X  |  ( x D y )  < 
r }  e.  ~P X )
2120ralrimivva 2758 . . . 4  |-  ( D  e.  (PsMet `  X
)  ->  A. x  e.  X  A. r  e.  RR*  { y  e.  X  |  ( x D y )  < 
r }  e.  ~P X )
22 eqid 2404 . . . . 5  |-  ( x  e.  X ,  r  e.  RR*  |->  { y  e.  X  |  ( x D y )  <  r } )  =  ( x  e.  X ,  r  e. 
RR*  |->  { y  e.  X  |  ( x D y )  < 
r } )
2322fmpt2 6377 . . . 4  |-  ( A. x  e.  X  A. r  e.  RR*  { y  e.  X  |  ( x D y )  <  r }  e.  ~P X  <->  ( x  e.  X ,  r  e. 
RR*  |->  { y  e.  X  |  ( x D y )  < 
r } ) : ( X  X.  RR* )
--> ~P X )
2421, 23sylib 189 . . 3  |-  ( D  e.  (PsMet `  X
)  ->  ( x  e.  X ,  r  e. 
RR*  |->  { y  e.  X  |  ( x D y )  < 
r } ) : ( X  X.  RR* )
--> ~P X )
25 xrex 10565 . . . 4  |-  RR*  e.  _V
26 xpexg 4948 . . . 4  |-  ( ( X  e.  dom PsMet  /\  RR*  e.  _V )  ->  ( X  X.  RR* )  e.  _V )
2716, 25, 26sylancl 644 . . 3  |-  ( D  e.  (PsMet `  X
)  ->  ( X  X.  RR* )  e.  _V )
28 pwexg 4343 . . . 4  |-  ( X  e.  dom PsMet  ->  ~P X  e.  _V )
2916, 28syl 16 . . 3  |-  ( D  e.  (PsMet `  X
)  ->  ~P X  e.  _V )
30 fex2 5562 . . 3  |-  ( ( ( x  e.  X ,  r  e.  RR*  |->  { y  e.  X  |  ( x D y )  <  r } ) : ( X  X.  RR* ) --> ~P X  /\  ( X  X.  RR* )  e.  _V  /\  ~P X  e.  _V )  ->  (
x  e.  X , 
r  e.  RR*  |->  { y  e.  X  |  ( x D y )  <  r } )  e.  _V )
3124, 27, 29, 30syl3anc 1184 . 2  |-  ( D  e.  (PsMet `  X
)  ->  ( x  e.  X ,  r  e. 
RR*  |->  { y  e.  X  |  ( x D y )  < 
r } )  e. 
_V )
322, 13, 14, 31fvmptd 5769 1  |-  ( D  e.  (PsMet `  X
)  ->  ( ball `  D )  =  ( x  e.  X , 
r  e.  RR*  |->  { y  e.  X  |  ( x D y )  <  r } ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1721   A.wral 2666   {crab 2670   _Vcvv 2916    C_ wss 3280   ~Pcpw 3759   class class class wbr 4172    e. cmpt 4226    X. cxp 4835   dom cdm 4837   -->wf 5409   ` cfv 5413  (class class class)co 6040    e. cmpt2 6042   RR*cxr 9075    < clt 9076  PsMetcpsmet 16640   ballcbl 16643
This theorem is referenced by:  blfval  18367  blvalps  18368  blfps  18389
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-map 6979  df-xr 9080  df-psmet 16649  df-bl 16652
  Copyright terms: Public domain W3C validator