Metamath Proof Explorer

Theorem bcthlem3

Description: Lemma for bcth . The limit point of the centers in the sequence is in the intersection of every ball in the sequence. (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 bcthlem3 
|- ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x /\ A e. NN ) -> x e. ( ( ball ` D ) ` ( g ` A ) ) )

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 fvoveq1 
 |-  ( k = A -> ( g ` ( k + 1 ) ) = ( g ` ( A + 1 ) ) )
11 id 
 |-  ( k = A -> k = A )
12 fveq2 
 |-  ( k = A -> ( g ` k ) = ( g ` A ) )
13 11 12 oveq12d 
 |-  ( k = A -> ( k F ( g ` k ) ) = ( A F ( g ` A ) ) )
14 10 13 eleq12d 
 |-  ( k = A -> ( ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) <-> ( g ` ( A + 1 ) ) e. ( A F ( g ` A ) ) ) )
15 14 rspccva 
 |-  ( ( A. k e. NN ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) /\ A e. NN ) -> ( g ` ( A + 1 ) ) e. ( A F ( g ` A ) ) )
16 9 15 sylan 
 |-  ( ( ph /\ A e. NN ) -> ( g ` ( A + 1 ) ) e. ( A F ( g ` A ) ) )
17 7 ffvelrnda 
 |-  ( ( ph /\ A e. NN ) -> ( g ` A ) e. ( X X. RR+ ) )
18 1 2 3 bcthlem1 
 |-  ( ( ph /\ ( A e. NN /\ ( g ` A ) e. ( X X. RR+ ) ) ) -> ( ( g ` ( A + 1 ) ) e. ( A F ( g ` A ) ) <-> ( ( g ` ( A + 1 ) ) e. ( X X. RR+ ) /\ ( 2nd ` ( g ` ( A + 1 ) ) ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( A + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` A ) ) \ ( M ` A ) ) ) ) )
19 18 expr 
 |-  ( ( ph /\ A e. NN ) -> ( ( g ` A ) e. ( X X. RR+ ) -> ( ( g ` ( A + 1 ) ) e. ( A F ( g ` A ) ) <-> ( ( g ` ( A + 1 ) ) e. ( X X. RR+ ) /\ ( 2nd ` ( g ` ( A + 1 ) ) ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( A + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` A ) ) \ ( M ` A ) ) ) ) ) )
20 17 19 mpd 
 |-  ( ( ph /\ A e. NN ) -> ( ( g ` ( A + 1 ) ) e. ( A F ( g ` A ) ) <-> ( ( g ` ( A + 1 ) ) e. ( X X. RR+ ) /\ ( 2nd ` ( g ` ( A + 1 ) ) ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( A + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` A ) ) \ ( M ` A ) ) ) ) )
21 16 20 mpbid 
 |-  ( ( ph /\ A e. NN ) -> ( ( g ` ( A + 1 ) ) e. ( X X. RR+ ) /\ ( 2nd ` ( g ` ( A + 1 ) ) ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( A + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` A ) ) \ ( M ` A ) ) ) )
22 21 simp3d 
 |-  ( ( ph /\ A e. NN ) -> ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( A + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` A ) ) \ ( M ` A ) ) )
23 22 difss2d 
 |-  ( ( ph /\ A e. NN ) -> ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( A + 1 ) ) ) ) C_ ( ( ball ` D ) ` ( g ` A ) ) )
24 23 3adant2 
 |-  ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x /\ A e. NN ) -> ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( A + 1 ) ) ) ) C_ ( ( ball ` D ) ` ( g ` A ) ) )
25 peano2nn 
 |-  ( A e. NN -> ( A + 1 ) e. NN )
26 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
27 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
28 2 26 27 3syl 
 |-  ( ph -> D e. ( *Met ` X ) )
29 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 ) ) )
30 28 7 29 1 caublcls 
 |-  ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x /\ ( A + 1 ) e. NN ) -> x e. ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( A + 1 ) ) ) ) )
31 25 30 syl3an3 
 |-  ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x /\ A e. NN ) -> x e. ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( A + 1 ) ) ) ) )
32 24 31 sseldd 
 |-  ( ( ph /\ ( 1st o. g ) ( ~~>t ` J ) x /\ A e. NN ) -> x e. ( ( ball ` D ) ` ( g ` A ) ) )