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=MetOpenD
bcthlem.4 φDCMetX
bcthlem.5 F=k,zX×+xr|xXr+r<1kclsJxballDrballDzMk
bcthlem.6 φM:ClsdJ
bcthlem.7 φR+
bcthlem.8 φCX
bcthlem.9 φg:X×+
bcthlem.10 φg1=CR
bcthlem.11 φkgk+1kFgk
Assertion bcthlem3 φ1stgtJxAxballDgA

Proof

Step Hyp Ref Expression
1 bcth.2 J=MetOpenD
2 bcthlem.4 φDCMetX
3 bcthlem.5 F=k,zX×+xr|xXr+r<1kclsJxballDrballDzMk
4 bcthlem.6 φM:ClsdJ
5 bcthlem.7 φR+
6 bcthlem.8 φCX
7 bcthlem.9 φg:X×+
8 bcthlem.10 φg1=CR
9 bcthlem.11 φkgk+1kFgk
10 fvoveq1 k=Agk+1=gA+1
11 id k=Ak=A
12 fveq2 k=Agk=gA
13 11 12 oveq12d k=AkFgk=AFgA
14 10 13 eleq12d k=Agk+1kFgkgA+1AFgA
15 14 rspccva kgk+1kFgkAgA+1AFgA
16 9 15 sylan φAgA+1AFgA
17 7 ffvelcdmda φAgAX×+
18 1 2 3 bcthlem1 φAgAX×+gA+1AFgAgA+1X×+2ndgA+1<1AclsJballDgA+1ballDgAMA
19 18 expr φAgAX×+gA+1AFgAgA+1X×+2ndgA+1<1AclsJballDgA+1ballDgAMA
20 17 19 mpd φAgA+1AFgAgA+1X×+2ndgA+1<1AclsJballDgA+1ballDgAMA
21 16 20 mpbid φAgA+1X×+2ndgA+1<1AclsJballDgA+1ballDgAMA
22 21 simp3d φAclsJballDgA+1ballDgAMA
23 22 difss2d φAclsJballDgA+1ballDgA
24 23 3adant2 φ1stgtJxAclsJballDgA+1ballDgA
25 peano2nn AA+1
26 cmetmet DCMetXDMetX
27 metxmet DMetXD∞MetX
28 2 26 27 3syl φD∞MetX
29 1 2 3 4 5 6 7 8 9 bcthlem2 φnballDgn+1ballDgn
30 28 7 29 1 caublcls φ1stgtJxA+1xclsJballDgA+1
31 25 30 syl3an3 φ1stgtJxAxclsJballDgA+1
32 24 31 sseldd φ1stgtJxAxballDgA