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 | |
|
bcthlem.4 | |
||
bcthlem.5 | |
||
bcthlem.6 | |
||
bcthlem.7 | |
||
bcthlem.8 | |
||
bcthlem.9 | |
||
bcthlem.10 | |
||
bcthlem.11 | |
||
Assertion | bcthlem3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bcth.2 | |
|
2 | bcthlem.4 | |
|
3 | bcthlem.5 | |
|
4 | bcthlem.6 | |
|
5 | bcthlem.7 | |
|
6 | bcthlem.8 | |
|
7 | bcthlem.9 | |
|
8 | bcthlem.10 | |
|
9 | bcthlem.11 | |
|
10 | fvoveq1 | |
|
11 | id | |
|
12 | fveq2 | |
|
13 | 11 12 | oveq12d | |
14 | 10 13 | eleq12d | |
15 | 14 | rspccva | |
16 | 9 15 | sylan | |
17 | 7 | ffvelcdmda | |
18 | 1 2 3 | bcthlem1 | |
19 | 18 | expr | |
20 | 17 19 | mpd | |
21 | 16 20 | mpbid | |
22 | 21 | simp3d | |
23 | 22 | difss2d | |
24 | 23 | 3adant2 | |
25 | peano2nn | |
|
26 | cmetmet | |
|
27 | metxmet | |
|
28 | 2 26 27 | 3syl | |
29 | 1 2 3 4 5 6 7 8 9 | bcthlem2 | |
30 | 28 7 29 1 | caublcls | |
31 | 25 30 | syl3an3 | |
32 | 24 31 | sseldd | |