Metamath Proof Explorer

Theorem bcthlem4

Description: Lemma for bcth . Given any open ball ( C ( ballD ) R ) as starting point (and in particular, a ball in int ( U. ran M ) ), the limit point x of the centers of the induced sequence of balls g is outside U. ran M . Note that a set A has empty interior iff every nonempty open set U contains points outside A , i.e. ( U \ A ) =/= (/) . (Contributed by Mario Carneiro, 7-Jan-2014)

Ref Expression
Hypotheses bcth.2 
|- J = ( MetOpen ` D )
bcthlem.4 
|- ( ph -> D e. ( CMet ` X ) )
bcthlem.5 
|- F = ( k e. NN , z e. ( X X. RR+ ) |-> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } )
bcthlem.6 
|- ( ph -> M : NN --> ( Clsd ` J ) )
bcthlem.7 
|- ( ph -> R e. RR+ )
bcthlem.8 
|- ( ph -> C e. X )
bcthlem.9 
|- ( ph -> g : NN --> ( X X. RR+ ) )
bcthlem.10 
|- ( ph -> ( g ` 1 ) = <. C , R >. )
bcthlem.11 
|- ( ph -> A. k e. NN ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) )
Assertion bcthlem4 
|- ( ph -> ( ( C ( ball ` D ) R ) \ U. ran M ) =/= (/) )

Proof

Step Hyp Ref Expression
1 bcth.2 
 |-  J = ( MetOpen ` D )
2 bcthlem.4 
 |-  ( ph -> D e. ( CMet ` X ) )
3 bcthlem.5 
 |-  F = ( k e. NN , z e. ( X X. RR+ ) |-> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } )
4 bcthlem.6 
 |-  ( ph -> M : NN --> ( Clsd ` J ) )
5 bcthlem.7 
 |-  ( ph -> R e. RR+ )
6 bcthlem.8 
 |-  ( ph -> C e. X )
7 bcthlem.9 
 |-  ( ph -> g : NN --> ( X X. RR+ ) )
8 bcthlem.10 
 |-  ( ph -> ( g ` 1 ) = <. C , R >. )
9 bcthlem.11 
 |-  ( ph -> A. k e. NN ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) )
10 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
11 2 10 syl 
 |-  ( ph -> D e. ( Met ` X ) )
12 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
13 11 12 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
14 1 2 3 4 5 6 7 8 9 bcthlem2 
 |-  ( ph -> A. n e. NN ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( g ` n ) ) )
15 elrp 
 |-  ( r e. RR+ <-> ( r e. RR /\ 0 < r ) )
16 nnrecl 
 |-  ( ( r e. RR /\ 0 < r ) -> E. m e. NN ( 1 / m ) < r )
17 15 16 sylbi 
 |-  ( r e. RR+ -> E. m e. NN ( 1 / m ) < r )
18 17 adantl 
 |-  ( ( ph /\ r e. RR+ ) -> E. m e. NN ( 1 / m ) < r )
19 peano2nn 
 |-  ( m e. NN -> ( m + 1 ) e. NN )
20 19 adantl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ m e. NN ) -> ( m + 1 ) e. NN )
21 fvoveq1 
 |-  ( k = m -> ( g ` ( k + 1 ) ) = ( g ` ( m + 1 ) ) )
22 id 
 |-  ( k = m -> k = m )
23 fveq2 
 |-  ( k = m -> ( g ` k ) = ( g ` m ) )
24 22 23 oveq12d 
 |-  ( k = m -> ( k F ( g ` k ) ) = ( m F ( g ` m ) ) )
25 21 24 eleq12d 
 |-  ( k = m -> ( ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) <-> ( g ` ( m + 1 ) ) e. ( m F ( g ` m ) ) ) )
26 25 rspccva 
 |-  ( ( A. k e. NN ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) /\ m e. NN ) -> ( g ` ( m + 1 ) ) e. ( m F ( g ` m ) ) )
27 9 26 sylan 
 |-  ( ( ph /\ m e. NN ) -> ( g ` ( m + 1 ) ) e. ( m F ( g ` m ) ) )
28 7 ffvelcdmda 
 |-  ( ( ph /\ m e. NN ) -> ( g ` m ) e. ( X X. RR+ ) )
29 1 2 3 bcthlem1 
 |-  ( ( ph /\ ( m e. NN /\ ( g ` m ) e. ( X X. RR+ ) ) ) -> ( ( g ` ( m + 1 ) ) e. ( m F ( g ` m ) ) <-> ( ( g ` ( m + 1 ) ) e. ( X X. RR+ ) /\ ( 2nd ` ( g ` ( m + 1 ) ) ) < ( 1 / m ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( m + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` m ) ) \ ( M ` m ) ) ) ) )
30 29 expr 
 |-  ( ( ph /\ m e. NN ) -> ( ( g ` m ) e. ( X X. RR+ ) -> ( ( g ` ( m + 1 ) ) e. ( m F ( g ` m ) ) <-> ( ( g ` ( m + 1 ) ) e. ( X X. RR+ ) /\ ( 2nd ` ( g ` ( m + 1 ) ) ) < ( 1 / m ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( m + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` m ) ) \ ( M ` m ) ) ) ) ) )
31 28 30 mpd 
 |-  ( ( ph /\ m e. NN ) -> ( ( g ` ( m + 1 ) ) e. ( m F ( g ` m ) ) <-> ( ( g ` ( m + 1 ) ) e. ( X X. RR+ ) /\ ( 2nd ` ( g ` ( m + 1 ) ) ) < ( 1 / m ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( m + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` m ) ) \ ( M ` m ) ) ) ) )
32 27 31 mpbid 
 |-  ( ( ph /\ m e. NN ) -> ( ( g ` ( m + 1 ) ) e. ( X X. RR+ ) /\ ( 2nd ` ( g ` ( m + 1 ) ) ) < ( 1 / m ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( m + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` m ) ) \ ( M ` m ) ) ) )
33 32 simp2d 
 |-  ( ( ph /\ m e. NN ) -> ( 2nd ` ( g ` ( m + 1 ) ) ) < ( 1 / m ) )
34 33 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ m e. NN ) -> ( 2nd ` ( g ` ( m + 1 ) ) ) < ( 1 / m ) )
35 32 simp1d 
 |-  ( ( ph /\ m e. NN ) -> ( g ` ( m + 1 ) ) e. ( X X. RR+ ) )
36 xp2nd 
 |-  ( ( g ` ( m + 1 ) ) e. ( X X. RR+ ) -> ( 2nd ` ( g ` ( m + 1 ) ) ) e. RR+ )
37 35 36 syl 
 |-  ( ( ph /\ m e. NN ) -> ( 2nd ` ( g ` ( m + 1 ) ) ) e. RR+ )
38 37 rpred 
 |-  ( ( ph /\ m e. NN ) -> ( 2nd ` ( g ` ( m + 1 ) ) ) e. RR )
39 38 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ m e. NN ) -> ( 2nd ` ( g ` ( m + 1 ) ) ) e. RR )
40 nnrecre 
 |-  ( m e. NN -> ( 1 / m ) e. RR )
41 40 adantl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ m e. NN ) -> ( 1 / m ) e. RR )
42 rpre 
 |-  ( r e. RR+ -> r e. RR )
43 42 ad2antlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ m e. NN ) -> r e. RR )
44 lttr 
 |-  ( ( ( 2nd ` ( g ` ( m + 1 ) ) ) e. RR /\ ( 1 / m ) e. RR /\ r e. RR ) -> ( ( ( 2nd ` ( g ` ( m + 1 ) ) ) < ( 1 / m ) /\ ( 1 / m ) < r ) -> ( 2nd ` ( g ` ( m + 1 ) ) ) < r ) )
45 39 41 43 44 syl3anc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ m e. NN ) -> ( ( ( 2nd ` ( g ` ( m + 1 ) ) ) < ( 1 / m ) /\ ( 1 / m ) < r ) -> ( 2nd ` ( g ` ( m + 1 ) ) ) < r ) )
46 34 45 mpand 
 |-  ( ( ( ph /\ r e. RR+ ) /\ m e. NN ) -> ( ( 1 / m ) < r -> ( 2nd ` ( g ` ( m + 1 ) ) ) < r ) )
47 2fveq3 
 |-  ( n = ( m + 1 ) -> ( 2nd ` ( g ` n ) ) = ( 2nd ` ( g ` ( m + 1 ) ) ) )
48 47 breq1d 
 |-  ( n = ( m + 1 ) -> ( ( 2nd ` ( g ` n ) ) < r <-> ( 2nd ` ( g ` ( m + 1 ) ) ) < r ) )
49 48 rspcev 
 |-  ( ( ( m + 1 ) e. NN /\ ( 2nd ` ( g ` ( m + 1 ) ) ) < r ) -> E. n e. NN ( 2nd ` ( g ` n ) ) < r )
50 20 46 49 syl6an 
 |-  ( ( ( ph /\ r e. RR+ ) /\ m e. NN ) -> ( ( 1 / m ) < r -> E. n e. NN ( 2nd ` ( g ` n ) ) < r ) )
51 50 rexlimdva 
 |-  ( ( ph /\ r e. RR+ ) -> ( E. m e. NN ( 1 / m ) < r -> E. n e. NN ( 2nd ` ( g ` n ) ) < r ) )
52 18 51 mpd 
 |-  ( ( ph /\ r e. RR+ ) -> E. n e. NN ( 2nd ` ( g ` n ) ) < r )
53 52 ralrimiva 
 |-  ( ph -> A. r e. RR+ E. n e. NN ( 2nd ` ( g ` n ) ) < r )
54 13 7 14 53 caubl 
 |-  ( ph -> ( 1st o. g ) e. ( Cau ` D ) )
55 1 cmetcau 
 |-  ( ( D e. ( CMet ` X ) /\ ( 1st o. g ) e. ( Cau ` D ) ) -> ( 1st o. g ) e. dom ( ~~>t ` J ) )
56 2 54 55 syl2anc 
 |-  ( ph -> ( 1st o. g ) e. dom ( ~~>t ` J ) )
57 fo1st 
 |-  1st : _V -onto-> _V
58 fofun 
 |-  ( 1st : _V -onto-> _V -> Fun 1st )
59 57 58 ax-mp 
 |-  Fun 1st
60 vex 
 |-  g e. _V
61 cofunexg 
 |-  ( ( Fun 1st /\ g e. _V ) -> ( 1st o. g ) e. _V )
62 59 60 61 mp2an 
 |-  ( 1st o. g ) e. _V
63 62 eldm 
 |-  ( ( 1st o. g ) e. dom ( ~~>t ` J ) <-> E. x ( 1st o. g ) ( ~~>t ` J ) x )
64 56 63 sylib 
 |-  ( ph -> E. x ( 1st o. g ) ( ~~>t ` J ) x )
65 1nn 
 |-  1 e. NN
66 1 2 3 4 5 6 7 8 9 bcthlem3 
 |-  ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x /\ 1 e. NN ) -> x e. ( ( ball ` D ) ` ( g ` 1 ) ) )
67 65 66 mp3an3 
 |-  ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x ) -> x e. ( ( ball ` D ) ` ( g ` 1 ) ) )
68 8 fveq2d 
 |-  ( ph -> ( ( ball ` D ) ` ( g ` 1 ) ) = ( ( ball ` D ) ` <. C , R >. ) )
69 df-ov 
 |-  ( C ( ball ` D ) R ) = ( ( ball ` D ) ` <. C , R >. )
70 68 69 eqtr4di 
 |-  ( ph -> ( ( ball ` D ) ` ( g ` 1 ) ) = ( C ( ball ` D ) R ) )
71 70 adantr 
 |-  ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x ) -> ( ( ball ` D ) ` ( g ` 1 ) ) = ( C ( ball ` D ) R ) )
72 67 71 eleqtrd 
 |-  ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x ) -> x e. ( C ( ball ` D ) R ) )
73 1 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
74 13 73 syl 
 |-  ( ph -> J e. Top )
75 74 adantr 
 |-  ( ( ph /\ m e. NN ) -> J e. Top )
76 13 adantr 
 |-  ( ( ph /\ m e. NN ) -> D e. ( *Met ` X ) )
77 xp1st 
 |-  ( ( g ` ( m + 1 ) ) e. ( X X. RR+ ) -> ( 1st ` ( g ` ( m + 1 ) ) ) e. X )
78 35 77 syl 
 |-  ( ( ph /\ m e. NN ) -> ( 1st ` ( g ` ( m + 1 ) ) ) e. X )
79 37 rpxrd 
 |-  ( ( ph /\ m e. NN ) -> ( 2nd ` ( g ` ( m + 1 ) ) ) e. RR* )
80 blssm 
 |-  ( ( D e. ( *Met ` X ) /\ ( 1st ` ( g ` ( m + 1 ) ) ) e. X /\ ( 2nd ` ( g ` ( m + 1 ) ) ) e. RR* ) -> ( ( 1st ` ( g ` ( m + 1 ) ) ) ( ball ` D ) ( 2nd ` ( g ` ( m + 1 ) ) ) ) C_ X )
81 76 78 79 80 syl3anc 
 |-  ( ( ph /\ m e. NN ) -> ( ( 1st ` ( g ` ( m + 1 ) ) ) ( ball ` D ) ( 2nd ` ( g ` ( m + 1 ) ) ) ) C_ X )
82 df-ov 
 |-  ( ( 1st ` ( g ` ( m + 1 ) ) ) ( ball ` D ) ( 2nd ` ( g ` ( m + 1 ) ) ) ) = ( ( ball ` D ) ` <. ( 1st ` ( g ` ( m + 1 ) ) ) , ( 2nd ` ( g ` ( m + 1 ) ) ) >. )
83 1st2nd2 
 |-  ( ( g ` ( m + 1 ) ) e. ( X X. RR+ ) -> ( g ` ( m + 1 ) ) = <. ( 1st ` ( g ` ( m + 1 ) ) ) , ( 2nd ` ( g ` ( m + 1 ) ) ) >. )
84 35 83 syl 
 |-  ( ( ph /\ m e. NN ) -> ( g ` ( m + 1 ) ) = <. ( 1st ` ( g ` ( m + 1 ) ) ) , ( 2nd ` ( g ` ( m + 1 ) ) ) >. )
85 84 fveq2d 
 |-  ( ( ph /\ m e. NN ) -> ( ( ball ` D ) ` ( g ` ( m + 1 ) ) ) = ( ( ball ` D ) ` <. ( 1st ` ( g ` ( m + 1 ) ) ) , ( 2nd ` ( g ` ( m + 1 ) ) ) >. ) )
86 82 85 eqtr4id 
 |-  ( ( ph /\ m e. NN ) -> ( ( 1st ` ( g ` ( m + 1 ) ) ) ( ball ` D ) ( 2nd ` ( g ` ( m + 1 ) ) ) ) = ( ( ball ` D ) ` ( g ` ( m + 1 ) ) ) )
87 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
88 13 87 syl 
 |-  ( ph -> X = U. J )
89 88 adantr 
 |-  ( ( ph /\ m e. NN ) -> X = U. J )
90 81 86 89 3sstr3d 
 |-  ( ( ph /\ m e. NN ) -> ( ( ball ` D ) ` ( g ` ( m + 1 ) ) ) C_ U. J )
91 eqid 
 |-  U. J = U. J
92 91 sscls 
 |-  ( ( J e. Top /\ ( ( ball ` D ) ` ( g ` ( m + 1 ) ) ) C_ U. J ) -> ( ( ball ` D ) ` ( g ` ( m + 1 ) ) ) C_ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( m + 1 ) ) ) ) )
93 75 90 92 syl2anc 
 |-  ( ( ph /\ m e. NN ) -> ( ( ball ` D ) ` ( g ` ( m + 1 ) ) ) C_ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( m + 1 ) ) ) ) )
94 32 simp3d 
 |-  ( ( ph /\ m e. NN ) -> ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( m + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` m ) ) \ ( M ` m ) ) )
95 93 94 sstrd 
 |-  ( ( ph /\ m e. NN ) -> ( ( ball ` D ) ` ( g ` ( m + 1 ) ) ) C_ ( ( ( ball ` D ) ` ( g ` m ) ) \ ( M ` m ) ) )
96 95 3adant2 
 |-  ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x /\ m e. NN ) -> ( ( ball ` D ) ` ( g ` ( m + 1 ) ) ) C_ ( ( ( ball ` D ) ` ( g ` m ) ) \ ( M ` m ) ) )
97 1 2 3 4 5 6 7 8 9 bcthlem3 
 |-  ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x /\ ( m + 1 ) e. NN ) -> x e. ( ( ball ` D ) ` ( g ` ( m + 1 ) ) ) )
98 19 97 syl3an3 
 |-  ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x /\ m e. NN ) -> x e. ( ( ball ` D ) ` ( g ` ( m + 1 ) ) ) )
99 96 98 sseldd 
 |-  ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x /\ m e. NN ) -> x e. ( ( ( ball ` D ) ` ( g ` m ) ) \ ( M ` m ) ) )
100 99 eldifbd 
 |-  ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x /\ m e. NN ) -> -. x e. ( M ` m ) )
101 100 3expa 
 |-  ( ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x ) /\ m e. NN ) -> -. x e. ( M ` m ) )
102 101 ralrimiva 
 |-  ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x ) -> A. m e. NN -. x e. ( M ` m ) )
103 eluni2 
 |-  ( x e. U. ran M <-> E. y e. ran M x e. y )
104 4 ffnd 
 |-  ( ph -> M Fn NN )
105 eleq2 
 |-  ( y = ( M ` m ) -> ( x e. y <-> x e. ( M ` m ) ) )
106 105 rexrn 
 |-  ( M Fn NN -> ( E. y e. ran M x e. y <-> E. m e. NN x e. ( M ` m ) ) )
107 104 106 syl 
 |-  ( ph -> ( E. y e. ran M x e. y <-> E. m e. NN x e. ( M ` m ) ) )
108 103 107 bitrid 
 |-  ( ph -> ( x e. U. ran M <-> E. m e. NN x e. ( M ` m ) ) )
109 108 notbid 
 |-  ( ph -> ( -. x e. U. ran M <-> -. E. m e. NN x e. ( M ` m ) ) )
110 ralnex 
 |-  ( A. m e. NN -. x e. ( M ` m ) <-> -. E. m e. NN x e. ( M ` m ) )
111 109 110 bitr4di 
 |-  ( ph -> ( -. x e. U. ran M <-> A. m e. NN -. x e. ( M ` m ) ) )
112 111 biimpar 
 |-  ( ( ph /\ A. m e. NN -. x e. ( M ` m ) ) -> -. x e. U. ran M )
113 102 112 syldan 
 |-  ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x ) -> -. x e. U. ran M )
114 72 113 eldifd 
 |-  ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x ) -> x e. ( ( C ( ball ` D ) R ) \ U. ran M ) )
115 114 ne0d 
 |-  ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x ) -> ( ( C ( ball ` D ) R ) \ U. ran M ) =/= (/) )
116 64 115 exlimddv 
 |-  ( ph -> ( ( C ( ball ` D ) R ) \ U. ran M ) =/= (/) )