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 φ D CMet X
bcthlem.5 F = k , z X × + x r | x X r + r < 1 k cls J x ball D r ball D z M k
bcthlem.6 φ M : Clsd J
bcthlem.7 φ R +
bcthlem.8 φ C X
bcthlem.9 φ g : X × +
bcthlem.10 φ g 1 = C R
bcthlem.11 φ k g k + 1 k F g k
Assertion bcthlem3 φ 1 st g t J x A x ball D g A

Proof

Step Hyp Ref Expression
1 bcth.2 J = MetOpen D
2 bcthlem.4 φ D CMet X
3 bcthlem.5 F = k , z X × + x r | x X r + r < 1 k cls J x ball D r ball D z M k
4 bcthlem.6 φ M : Clsd J
5 bcthlem.7 φ R +
6 bcthlem.8 φ C X
7 bcthlem.9 φ g : X × +
8 bcthlem.10 φ g 1 = C R
9 bcthlem.11 φ k g k + 1 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 k F g k g A + 1 A F g A
15 14 rspccva k g k + 1 k F g k A g A + 1 A F g A
16 9 15 sylan φ A g A + 1 A F g A
17 7 ffvelrnda φ A g A X × +
18 1 2 3 bcthlem1 φ A g A X × + g A + 1 A F g A g A + 1 X × + 2 nd g A + 1 < 1 A cls J ball D g A + 1 ball D g A M A
19 18 expr φ A g A X × + g A + 1 A F g A g A + 1 X × + 2 nd g A + 1 < 1 A cls J ball D g A + 1 ball D g A M A
20 17 19 mpd φ A g A + 1 A F g A g A + 1 X × + 2 nd g A + 1 < 1 A cls J ball D g A + 1 ball D g A M A
21 16 20 mpbid φ A g A + 1 X × + 2 nd g A + 1 < 1 A cls J ball D g A + 1 ball D g A M A
22 21 simp3d φ A cls J ball D g A + 1 ball D g A M A
23 22 difss2d φ A cls J ball D g A + 1 ball D g A
24 23 3adant2 φ 1 st g t J x A cls J ball D g A + 1 ball D g A
25 peano2nn A A + 1
26 cmetmet D CMet X D Met X
27 metxmet D Met X D ∞Met X
28 2 26 27 3syl φ D ∞Met X
29 1 2 3 4 5 6 7 8 9 bcthlem2 φ n ball D g n + 1 ball D g n
30 28 7 29 1 caublcls φ 1 st g t J x A + 1 x cls J ball D g A + 1
31 25 30 syl3an3 φ 1 st g t J x A x cls J ball D g A + 1
32 24 31 sseldd φ 1 st g t J x A x ball D g A