Metamath Proof Explorer

Theorem blfvalps

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)

Ref Expression
Assertion blfvalps 
|- ( D e. ( PsMet ` X ) -> ( ball ` D ) = ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) )

Proof

Step Hyp Ref Expression
1 df-bl 
 |-  ball = ( d e. _V |-> ( x e. dom dom d , r e. RR* |-> { y e. dom dom d | ( x d y ) < r } ) )
2 dmeq 
 |-  ( d = D -> dom d = dom D )
3 2 dmeqd 
 |-  ( d = D -> dom dom d = dom dom D )
4 psmetdmdm 
 |-  ( D e. ( PsMet ` X ) -> X = dom dom D )
5 4 eqcomd 
 |-  ( D e. ( PsMet ` X ) -> dom dom D = X )
6 3 5 sylan9eqr 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> dom dom d = X )
7 eqidd 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> RR* = RR* )
8 simpr 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> d = D )
9 8 oveqd 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( x d y ) = ( x D y ) )
10 9 breq1d 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( ( x d y ) < r <-> ( x D y ) < r ) )
11 6 10 rabeqbidv 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> { y e. dom dom d | ( x d y ) < r } = { y e. X | ( x D y ) < r } )
12 6 7 11 mpoeq123dv 
 |-  ( ( 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 } ) )
13 elex 
 |-  ( D e. ( PsMet ` X ) -> D e. _V )
14 ssrab2 
 |-  { y e. X | ( x D y ) < r } C_ X
15 elfvdm 
 |-  ( D e. ( PsMet ` X ) -> X e. dom PsMet )
16 15 adantr 
 |-  ( ( D e. ( PsMet ` X ) /\ ( x e. X /\ r e. RR* ) ) -> X e. dom PsMet )
17 elpw2g 
 |-  ( X e. dom PsMet -> ( { y e. X | ( x D y ) < r } e. ~P X <-> { y e. X | ( x D y ) < r } C_ X ) )
18 16 17 syl 
 |-  ( ( 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 ) )
19 14 18 mpbiri 
 |-  ( ( D e. ( PsMet ` X ) /\ ( x e. X /\ r e. RR* ) ) -> { y e. X | ( x D y ) < r } e. ~P X )
20 19 ralrimivva 
 |-  ( D e. ( PsMet ` X ) -> A. x e. X A. r e. RR* { y e. X | ( x D y ) < r } e. ~P X )
21 eqid 
 |-  ( 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 } )
22 21 fmpo 
 |-  ( 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 )
23 20 22 sylib 
 |-  ( D e. ( PsMet ` X ) -> ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) : ( X X. RR* ) --> ~P X )
24 xrex 
 |-  RR* e. _V
25 xpexg 
 |-  ( ( X e. dom PsMet /\ RR* e. _V ) -> ( X X. RR* ) e. _V )
26 15 24 25 sylancl 
 |-  ( D e. ( PsMet ` X ) -> ( X X. RR* ) e. _V )
27 15 pwexd 
 |-  ( D e. ( PsMet ` X ) -> ~P X e. _V )
28 fex2 
 |-  ( ( ( 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 )
29 23 26 27 28 syl3anc 
 |-  ( D e. ( PsMet ` X ) -> ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) e. _V )
30 1 12 13 29 fvmptd2 
 |-  ( D e. ( PsMet ` X ) -> ( ball ` D ) = ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) )