Metamath Proof Explorer

Theorem metdsge

Description: The distance from the point A to the set S is greater than R iff the R -ball around A misses S . (Contributed by Mario Carneiro, 4-Sep-2015) (Proof shortened by AV, 30-Sep-2020)

Ref Expression
Hypothesis metdscn.f 
|- F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
Assertion metdsge 
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) -> ( R <_ ( F ` A ) <-> ( S i^i ( A ( ball ` D ) R ) ) = (/) ) )

Proof

Step Hyp Ref Expression
1 metdscn.f 
 |-  F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
2 simpl3 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) -> A e. X )
3 1 metdsval 
 |-  ( A e. X -> ( F ` A ) = inf ( ran ( y e. S |-> ( A D y ) ) , RR* , < ) )
4 2 3 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) -> ( F ` A ) = inf ( ran ( y e. S |-> ( A D y ) ) , RR* , < ) )
5 4 breq2d 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) -> ( R <_ ( F ` A ) <-> R <_ inf ( ran ( y e. S |-> ( A D y ) ) , RR* , < ) ) )
6 simpll1 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) /\ w e. S ) -> D e. ( *Met ` X ) )
7 2 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) /\ w e. S ) -> A e. X )
8 simpl2 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) -> S C_ X )
9 8 sselda 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) /\ w e. S ) -> w e. X )
10 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ w e. X ) -> ( A D w ) e. RR* )
11 6 7 9 10 syl3anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) /\ w e. S ) -> ( A D w ) e. RR* )
12 oveq2 
 |-  ( y = w -> ( A D y ) = ( A D w ) )
13 12 cbvmptv 
 |-  ( y e. S |-> ( A D y ) ) = ( w e. S |-> ( A D w ) )
14 11 13 fmptd 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) -> ( y e. S |-> ( A D y ) ) : S --> RR* )
15 14 frnd 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) -> ran ( y e. S |-> ( A D y ) ) C_ RR* )
16 simpr 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) -> R e. RR* )
17 infxrgelb 
 |-  ( ( ran ( y e. S |-> ( A D y ) ) C_ RR* /\ R e. RR* ) -> ( R <_ inf ( ran ( y e. S |-> ( A D y ) ) , RR* , < ) <-> A. z e. ran ( y e. S |-> ( A D y ) ) R <_ z ) )
18 15 16 17 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) -> ( R <_ inf ( ran ( y e. S |-> ( A D y ) ) , RR* , < ) <-> A. z e. ran ( y e. S |-> ( A D y ) ) R <_ z ) )
19 16 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) /\ w e. S ) -> R e. RR* )
20 elbl2 
 |-  ( ( ( D e. ( *Met ` X ) /\ R e. RR* ) /\ ( A e. X /\ w e. X ) ) -> ( w e. ( A ( ball ` D ) R ) <-> ( A D w ) < R ) )
21 6 19 7 9 20 syl22anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) /\ w e. S ) -> ( w e. ( A ( ball ` D ) R ) <-> ( A D w ) < R ) )
22 xrltnle 
 |-  ( ( ( A D w ) e. RR* /\ R e. RR* ) -> ( ( A D w ) < R <-> -. R <_ ( A D w ) ) )
23 11 19 22 syl2anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) /\ w e. S ) -> ( ( A D w ) < R <-> -. R <_ ( A D w ) ) )
24 21 23 bitrd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) /\ w e. S ) -> ( w e. ( A ( ball ` D ) R ) <-> -. R <_ ( A D w ) ) )
25 24 con2bid 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) /\ w e. S ) -> ( R <_ ( A D w ) <-> -. w e. ( A ( ball ` D ) R ) ) )
26 25 ralbidva 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) -> ( A. w e. S R <_ ( A D w ) <-> A. w e. S -. w e. ( A ( ball ` D ) R ) ) )
27 ovex 
 |-  ( A D w ) e. _V
28 27 rgenw 
 |-  A. w e. S ( A D w ) e. _V
29 breq2 
 |-  ( z = ( A D w ) -> ( R <_ z <-> R <_ ( A D w ) ) )
30 13 29 ralrnmptw 
 |-  ( A. w e. S ( A D w ) e. _V -> ( A. z e. ran ( y e. S |-> ( A D y ) ) R <_ z <-> A. w e. S R <_ ( A D w ) ) )
31 28 30 ax-mp 
 |-  ( A. z e. ran ( y e. S |-> ( A D y ) ) R <_ z <-> A. w e. S R <_ ( A D w ) )
32 disj 
 |-  ( ( S i^i ( A ( ball ` D ) R ) ) = (/) <-> A. w e. S -. w e. ( A ( ball ` D ) R ) )
33 26 31 32 3bitr4g 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) -> ( A. z e. ran ( y e. S |-> ( A D y ) ) R <_ z <-> ( S i^i ( A ( ball ` D ) R ) ) = (/) ) )
34 5 18 33 3bitrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) -> ( R <_ ( F ` A ) <-> ( S i^i ( A ( ball ` D ) R ) ) = (/) ) )