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 φ 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 bcthlem4 φ C ball D R ran M

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