Metamath Proof Explorer

Theorem blcld

Description: A "closed ball" in a metric space is actually closed. (Contributed by Mario Carneiro, 31-Dec-2013) (Revised by Mario Carneiro, 24-Aug-2015)

Ref Expression
Hypotheses mopni.1 
|- J = ( MetOpen ` D )
blcld.3 
|- S = { z e. X | ( P D z ) <_ R }
Assertion blcld 
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> S e. ( Clsd ` J ) )

Proof

Step Hyp Ref Expression
1 mopni.1 
 |-  J = ( MetOpen ` D )
2 blcld.3 
 |-  S = { z e. X | ( P D z ) <_ R }
3 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
4 3 3ad2ant1 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> X = U. J )
5 4 difeq1d 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( X \ S ) = ( U. J \ S ) )
6 difssd 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( X \ S ) C_ X )
7 simpl3 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) -> R e. RR* )
8 simpl1 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) -> D e. ( *Met ` X ) )
9 simpl2 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) -> P e. X )
10 eldifi 
 |-  ( y e. ( X \ S ) -> y e. X )
11 10 adantl 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) -> y e. X )
12 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ y e. X ) -> ( P D y ) e. RR* )
13 8 9 11 12 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) -> ( P D y ) e. RR* )
14 eldif 
 |-  ( y e. ( X \ S ) <-> ( y e. X /\ -. y e. S ) )
15 oveq2 
 |-  ( z = y -> ( P D z ) = ( P D y ) )
16 15 breq1d 
 |-  ( z = y -> ( ( P D z ) <_ R <-> ( P D y ) <_ R ) )
17 16 2 elrab2 
 |-  ( y e. S <-> ( y e. X /\ ( P D y ) <_ R ) )
18 17 simplbi2 
 |-  ( y e. X -> ( ( P D y ) <_ R -> y e. S ) )
19 18 con3dimp 
 |-  ( ( y e. X /\ -. y e. S ) -> -. ( P D y ) <_ R )
20 14 19 sylbi 
 |-  ( y e. ( X \ S ) -> -. ( P D y ) <_ R )
21 20 adantl 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) -> -. ( P D y ) <_ R )
22 xrltnle 
 |-  ( ( R e. RR* /\ ( P D y ) e. RR* ) -> ( R < ( P D y ) <-> -. ( P D y ) <_ R ) )
23 7 13 22 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) -> ( R < ( P D y ) <-> -. ( P D y ) <_ R ) )
24 21 23 mpbird 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) -> R < ( P D y ) )
25 qbtwnxr 
 |-  ( ( R e. RR* /\ ( P D y ) e. RR* /\ R < ( P D y ) ) -> E. x e. QQ ( R < x /\ x < ( P D y ) ) )
26 7 13 24 25 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) -> E. x e. QQ ( R < x /\ x < ( P D y ) ) )
27 qre 
 |-  ( x e. QQ -> x e. RR )
28 8 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> D e. ( *Met ` X ) )
29 11 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> y e. X )
30 13 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> ( P D y ) e. RR* )
31 rexr 
 |-  ( x e. RR -> x e. RR* )
32 31 ad2antrl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> x e. RR* )
33 32 xnegcld 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> -e x e. RR* )
34 30 33 xaddcld 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> ( ( P D y ) +e -e x ) e. RR* )
35 blelrn 
 |-  ( ( D e. ( *Met ` X ) /\ y e. X /\ ( ( P D y ) +e -e x ) e. RR* ) -> ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) e. ran ( ball ` D ) )
36 28 29 34 35 syl3anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) e. ran ( ball ` D ) )
37 simprrr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> x < ( P D y ) )
38 xposdif 
 |-  ( ( x e. RR* /\ ( P D y ) e. RR* ) -> ( x < ( P D y ) <-> 0 < ( ( P D y ) +e -e x ) ) )
39 32 30 38 syl2anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> ( x < ( P D y ) <-> 0 < ( ( P D y ) +e -e x ) ) )
40 37 39 mpbid 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> 0 < ( ( P D y ) +e -e x ) )
41 xblcntr 
 |-  ( ( D e. ( *Met ` X ) /\ y e. X /\ ( ( ( P D y ) +e -e x ) e. RR* /\ 0 < ( ( P D y ) +e -e x ) ) ) -> y e. ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) )
42 28 29 34 40 41 syl112anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> y e. ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) )
43 incom 
 |-  ( ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) i^i ( P ( ball ` D ) x ) ) = ( ( P ( ball ` D ) x ) i^i ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) )
44 9 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> P e. X )
45 xaddcom 
 |-  ( ( x e. RR* /\ ( ( P D y ) +e -e x ) e. RR* ) -> ( x +e ( ( P D y ) +e -e x ) ) = ( ( ( P D y ) +e -e x ) +e x ) )
46 32 34 45 syl2anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> ( x +e ( ( P D y ) +e -e x ) ) = ( ( ( P D y ) +e -e x ) +e x ) )
47 simprl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> x e. RR )
48 xnpcan 
 |-  ( ( ( P D y ) e. RR* /\ x e. RR ) -> ( ( ( P D y ) +e -e x ) +e x ) = ( P D y ) )
49 30 47 48 syl2anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> ( ( ( P D y ) +e -e x ) +e x ) = ( P D y ) )
50 46 49 eqtrd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> ( x +e ( ( P D y ) +e -e x ) ) = ( P D y ) )
51 30 xrleidd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> ( P D y ) <_ ( P D y ) )
52 50 51 eqbrtrd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> ( x +e ( ( P D y ) +e -e x ) ) <_ ( P D y ) )
53 bldisj 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ y e. X ) /\ ( x e. RR* /\ ( ( P D y ) +e -e x ) e. RR* /\ ( x +e ( ( P D y ) +e -e x ) ) <_ ( P D y ) ) ) -> ( ( P ( ball ` D ) x ) i^i ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) ) = (/) )
54 28 44 29 32 34 52 53 syl33anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> ( ( P ( ball ` D ) x ) i^i ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) ) = (/) )
55 43 54 eqtrid 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> ( ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) i^i ( P ( ball ` D ) x ) ) = (/) )
56 blssm 
 |-  ( ( D e. ( *Met ` X ) /\ y e. X /\ ( ( P D y ) +e -e x ) e. RR* ) -> ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) C_ X )
57 28 29 34 56 syl3anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) C_ X )
58 reldisj 
 |-  ( ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) C_ X -> ( ( ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) i^i ( P ( ball ` D ) x ) ) = (/) <-> ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) C_ ( X \ ( P ( ball ` D ) x ) ) ) )
59 57 58 syl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> ( ( ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) i^i ( P ( ball ` D ) x ) ) = (/) <-> ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) C_ ( X \ ( P ( ball ` D ) x ) ) ) )
60 55 59 mpbid 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) C_ ( X \ ( P ( ball ` D ) x ) ) )
61 7 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> R e. RR* )
62 simprrl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> R < x )
63 1 2 blsscls2 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ x e. RR* /\ R < x ) ) -> S C_ ( P ( ball ` D ) x ) )
64 28 44 61 32 62 63 syl23anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> S C_ ( P ( ball ` D ) x ) )
65 64 sscond 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> ( X \ ( P ( ball ` D ) x ) ) C_ ( X \ S ) )
66 60 65 sstrd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) C_ ( X \ S ) )
67 eleq2 
 |-  ( w = ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) -> ( y e. w <-> y e. ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) ) )
68 sseq1 
 |-  ( w = ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) -> ( w C_ ( X \ S ) <-> ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) C_ ( X \ S ) ) )
69 67 68 anbi12d 
 |-  ( w = ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) -> ( ( y e. w /\ w C_ ( X \ S ) ) <-> ( y e. ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) /\ ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) C_ ( X \ S ) ) ) )
70 69 rspcev 
 |-  ( ( ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) e. ran ( ball ` D ) /\ ( y e. ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) /\ ( y ( ball ` D ) ( ( P D y ) +e -e x ) ) C_ ( X \ S ) ) ) -> E. w e. ran ( ball ` D ) ( y e. w /\ w C_ ( X \ S ) ) )
71 36 42 66 70 syl12anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ ( x e. RR /\ ( R < x /\ x < ( P D y ) ) ) ) -> E. w e. ran ( ball ` D ) ( y e. w /\ w C_ ( X \ S ) ) )
72 71 expr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ x e. RR ) -> ( ( R < x /\ x < ( P D y ) ) -> E. w e. ran ( ball ` D ) ( y e. w /\ w C_ ( X \ S ) ) ) )
73 27 72 sylan2 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) /\ x e. QQ ) -> ( ( R < x /\ x < ( P D y ) ) -> E. w e. ran ( ball ` D ) ( y e. w /\ w C_ ( X \ S ) ) ) )
74 73 rexlimdva 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) -> ( E. x e. QQ ( R < x /\ x < ( P D y ) ) -> E. w e. ran ( ball ` D ) ( y e. w /\ w C_ ( X \ S ) ) ) )
75 26 74 mpd 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ y e. ( X \ S ) ) -> E. w e. ran ( ball ` D ) ( y e. w /\ w C_ ( X \ S ) ) )
76 75 ralrimiva 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> A. y e. ( X \ S ) E. w e. ran ( ball ` D ) ( y e. w /\ w C_ ( X \ S ) ) )
77 1 elmopn 
 |-  ( D e. ( *Met ` X ) -> ( ( X \ S ) e. J <-> ( ( X \ S ) C_ X /\ A. y e. ( X \ S ) E. w e. ran ( ball ` D ) ( y e. w /\ w C_ ( X \ S ) ) ) ) )
78 77 3ad2ant1 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( ( X \ S ) e. J <-> ( ( X \ S ) C_ X /\ A. y e. ( X \ S ) E. w e. ran ( ball ` D ) ( y e. w /\ w C_ ( X \ S ) ) ) ) )
79 6 76 78 mpbir2and 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( X \ S ) e. J )
80 5 79 eqeltrrd 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( U. J \ S ) e. J )
81 1 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
82 81 3ad2ant1 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> J e. Top )
83 2 ssrab3 
 |-  S C_ X
84 83 4 sseqtrid 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> S C_ U. J )
85 eqid 
 |-  U. J = U. J
86 85 iscld2 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( S e. ( Clsd ` J ) <-> ( U. J \ S ) e. J ) )
87 82 84 86 syl2anc 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( S e. ( Clsd ` J ) <-> ( U. J \ S ) e. J ) )
88 80 87 mpbird 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> S e. ( Clsd ` J ) )