Metamath Proof Explorer


Theorem bcthlem5

Description: Lemma for bcth . The proof makes essential use of the Axiom of Dependent Choice axdc4uz , which in the form used here accepts a "selection" function F from each element of K to a nonempty subset of K , and the result function g maps g ( n + 1 ) to an element of F ( n , g ( n ) ) . The trick here is thus in the choice of F and K : we let K be the set of all tagged nonempty open sets (tagged here meaning that we have a point and an open set, in an ordered pair), and F ( k , <. x , z >. ) gives the set of all balls of size less than 1 / k , tagged by their centers, whose closures fit within the given open set z and miss M ( k ) .

Since M ( k ) is closed, z \ M ( k ) is open and also nonempty, since z is nonempty and M ( k ) has empty interior. Then there is some ball contained in it, and hence our function F is valid (it never maps to the empty set). Now starting at a point in the interior of U. ran M , DC gives us the function g all whose elements are constrained by F acting on the previous value. (This is all proven in this lemma.) Now g is a sequence of tagged open balls, forming an inclusion chain (see bcthlem2 ) and whose sizes tend to zero, since they are bounded above by 1 / k . Thus, the centers of these balls form a Cauchy sequence, and converge to a point x (see bcthlem4 ). Since the inclusion chain also ensures the closure of each ball is in the previous ball, the point x must be in all these balls (see bcthlem3 ) and hence misses each M ( k ) , contradicting the fact that x is in the interior of U. ran M (which was the starting point). (Contributed by Mario Carneiro, 6-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
bcthlem5.7 φkintJMk=
Assertion bcthlem5 φintJranM=

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 bcthlem5.7 φkintJMk=
6 cmetmet DCMetXDMetX
7 metxmet DMetXD∞MetX
8 2 6 7 3syl φD∞MetX
9 1 mopntop D∞MetXJTop
10 8 9 syl φJTop
11 4 frnd φranMClsdJ
12 eqid J=J
13 12 cldss2 ClsdJ𝒫J
14 11 13 sstrdi φranM𝒫J
15 sspwuni ranM𝒫JranMJ
16 14 15 sylib φranMJ
17 12 ntropn JTopranMJintJranMJ
18 10 16 17 syl2anc φintJranMJ
19 8 18 jca φD∞MetXintJranMJ
20 1 mopni2 D∞MetXintJranMJnintJranMm+nballDmintJranM
21 20 3expa D∞MetXintJranMJnintJranMm+nballDmintJranM
22 19 21 sylan φnintJranMm+nballDmintJranM
23 1 mopnuni D∞MetXX=J
24 8 23 syl φX=J
25 12 topopn JTopJJ
26 10 25 syl φJJ
27 24 26 eqeltrd φXJ
28 reex V
29 rpssre +
30 28 29 ssexi +V
31 xpexg XJ+VX×+V
32 27 30 31 sylancl φX×+V
33 32 3ad2ant1 φnintJranMm+X×+V
34 12 ntrss3 JTopranMJintJranMJ
35 10 16 34 syl2anc φintJranMJ
36 35 24 sseqtrrd φintJranMX
37 36 3ad2ant1 φnintJranMm+intJranMX
38 simp2 φnintJranMm+nintJranM
39 37 38 sseldd φnintJranMm+nX
40 simp3 φnintJranMm+m+
41 39 40 opelxpd φnintJranMm+nmX×+
42 opabssxp xr|xXr+r<1kclsJxballDrballDzMkX×+
43 elpw2g X×+Vxr|xXr+r<1kclsJxballDrballDzMk𝒫X×+xr|xXr+r<1kclsJxballDrballDzMkX×+
44 32 43 syl φxr|xXr+r<1kclsJxballDrballDzMk𝒫X×+xr|xXr+r<1kclsJxballDrballDzMkX×+
45 44 adantr φkzX×+xr|xXr+r<1kclsJxballDrballDzMk𝒫X×+xr|xXr+r<1kclsJxballDrballDzMkX×+
46 42 45 mpbiri φkzX×+xr|xXr+r<1kclsJxballDrballDzMk𝒫X×+
47 simpl kzX×+k
48 rspa kintJMk=kintJMk=
49 5 47 48 syl2an φkzX×+intJMk=
50 ssdif0 ballDzMkballDzMk=
51 1st2nd2 zX×+z=1stz2ndz
52 51 ad2antll φkzX×+z=1stz2ndz
53 52 fveq2d φkzX×+ballDz=ballD1stz2ndz
54 df-ov 1stzballD2ndz=ballD1stz2ndz
55 53 54 eqtr4di φkzX×+ballDz=1stzballD2ndz
56 8 adantr φkzX×+D∞MetX
57 xp1st zX×+1stzX
58 57 ad2antll φkzX×+1stzX
59 xp2nd zX×+2ndz+
60 59 ad2antll φkzX×+2ndz+
61 bln0 D∞MetX1stzX2ndz+1stzballD2ndz
62 56 58 60 61 syl3anc φkzX×+1stzballD2ndz
63 55 62 eqnetrd φkzX×+ballDz
64 10 adantr φkzX×+JTop
65 ffvelcdm M:ClsdJkMkClsdJ
66 4 47 65 syl2an φkzX×+MkClsdJ
67 12 cldss MkClsdJMkJ
68 66 67 syl φkzX×+MkJ
69 60 rpxrd φkzX×+2ndz*
70 1 blopn D∞MetX1stzX2ndz*1stzballD2ndzJ
71 56 58 69 70 syl3anc φkzX×+1stzballD2ndzJ
72 55 71 eqeltrd φkzX×+ballDzJ
73 12 ssntr JTopMkJballDzJballDzMkballDzintJMk
74 73 expr JTopMkJballDzJballDzMkballDzintJMk
75 64 68 72 74 syl21anc φkzX×+ballDzMkballDzintJMk
76 ssn0 ballDzintJMkballDzintJMk
77 76 expcom ballDzballDzintJMkintJMk
78 63 75 77 sylsyld φkzX×+ballDzMkintJMk
79 50 78 biimtrrid φkzX×+ballDzMk=intJMk
80 79 necon2d φkzX×+intJMk=ballDzMk
81 49 80 mpd φkzX×+ballDzMk
82 n0 ballDzMkxxballDzMk
83 8 3ad2ant1 φkzX×+xballDzMkD∞MetX
84 12 difopn ballDzJMkClsdJballDzMkJ
85 72 66 84 syl2anc φkzX×+ballDzMkJ
86 85 3adant3 φkzX×+xballDzMkballDzMkJ
87 simp3 φkzX×+xballDzMkxballDzMk
88 simp2l φkzX×+xballDzMkk
89 nnrp kk+
90 89 rpreccld k1k+
91 88 90 syl φkzX×+xballDzMk1k+
92 1 mopni3 D∞MetXballDzMkJxballDzMk1k+n+n<1kxballDnballDzMk
93 83 86 87 91 92 syl31anc φkzX×+xballDzMkn+n<1kxballDnballDzMk
94 simp1 φkzX×+xballDzMkφ
95 elssuni ballDzJballDzJ
96 72 95 syl φkzX×+ballDzJ
97 24 adantr φkzX×+X=J
98 96 97 sseqtrrd φkzX×+ballDzX
99 98 ssdifssd φkzX×+ballDzMkX
100 99 sseld φkzX×+xballDzMkxX
101 100 3impia φkzX×+xballDzMkxX
102 simp2 φkzX×+xballDzMkkzX×+
103 rphalfcl n+n2+
104 rphalflt n+n2<n
105 breq1 r=n2r<nn2<n
106 105 rspcev n2+n2<nr+r<n
107 103 104 106 syl2anc n+r+r<n
108 107 ad2antlr φxXkzX×+n+n<1kxballDnballDzMkr+r<n
109 df-rex r+r<nrr+r<n
110 simpr3 φxXkzX×+n+r<nr+r+
111 110 rpred φxXkzX×+n+r<nr+r
112 simpr1 φxXkzX×+n+r<nr+n+
113 112 rpred φxXkzX×+n+r<nr+n
114 simplrl φxXkzX×+n+r<nr+k
115 114 nnrecred φxXkzX×+n+r<nr+1k
116 simpr2 φxXkzX×+n+r<nr+r<n
117 lttr rn1kr<nn<1kr<1k
118 117 expdimp rn1kr<nn<1kr<1k
119 111 113 115 116 118 syl31anc φxXkzX×+n+r<nr+n<1kr<1k
120 8 anim1i φxXD∞MetXxX
121 120 adantr φxXkzX×+D∞MetXxX
122 rpxr r+r*
123 rpxr n+n*
124 id r<nr<n
125 122 123 124 3anim123i r+n+r<nr*n*r<n
126 125 3coml n+r<nr+r*n*r<n
127 1 blsscls D∞MetXxXr*n*r<nclsJxballDrxballDn
128 121 126 127 syl2an φxXkzX×+n+r<nr+clsJxballDrxballDn
129 sstr2 clsJxballDrxballDnxballDnballDzMkclsJxballDrballDzMk
130 128 129 syl φxXkzX×+n+r<nr+xballDnballDzMkclsJxballDrballDzMk
131 119 130 anim12d φxXkzX×+n+r<nr+n<1kxballDnballDzMkr<1kclsJxballDrballDzMk
132 simpllr φxXkzX×+n+r<nr+xX
133 132 110 jca φxXkzX×+n+r<nr+xXr+
134 131 133 jctild φxXkzX×+n+r<nr+n<1kxballDnballDzMkxXr+r<1kclsJxballDrballDzMk
135 134 3exp2 φxXkzX×+n+r<nr+n<1kxballDnballDzMkxXr+r<1kclsJxballDrballDzMk
136 135 com35 φxXkzX×+n+n<1kxballDnballDzMkr+r<nxXr+r<1kclsJxballDrballDzMk
137 136 imp5d φxXkzX×+n+n<1kxballDnballDzMkr+r<nxXr+r<1kclsJxballDrballDzMk
138 137 eximdv φxXkzX×+n+n<1kxballDnballDzMkrr+r<nrxXr+r<1kclsJxballDrballDzMk
139 109 138 biimtrid φxXkzX×+n+n<1kxballDnballDzMkr+r<nrxXr+r<1kclsJxballDrballDzMk
140 108 139 mpd φxXkzX×+n+n<1kxballDnballDzMkrxXr+r<1kclsJxballDrballDzMk
141 140 rexlimdva2 φxXkzX×+n+n<1kxballDnballDzMkrxXr+r<1kclsJxballDrballDzMk
142 94 101 102 141 syl21anc φkzX×+xballDzMkn+n<1kxballDnballDzMkrxXr+r<1kclsJxballDrballDzMk
143 93 142 mpd φkzX×+xballDzMkrxXr+r<1kclsJxballDrballDzMk
144 143 3expia φkzX×+xballDzMkrxXr+r<1kclsJxballDrballDzMk
145 144 eximdv φkzX×+xxballDzMkxrxXr+r<1kclsJxballDrballDzMk
146 82 145 biimtrid φkzX×+ballDzMkxrxXr+r<1kclsJxballDrballDzMk
147 81 146 mpd φkzX×+xrxXr+r<1kclsJxballDrballDzMk
148 opabn0 xr|xXr+r<1kclsJxballDrballDzMkxrxXr+r<1kclsJxballDrballDzMk
149 147 148 sylibr φkzX×+xr|xXr+r<1kclsJxballDrballDzMk
150 eldifsn xr|xXr+r<1kclsJxballDrballDzMk𝒫X×+xr|xXr+r<1kclsJxballDrballDzMk𝒫X×+xr|xXr+r<1kclsJxballDrballDzMk
151 46 149 150 sylanbrc φkzX×+xr|xXr+r<1kclsJxballDrballDzMk𝒫X×+
152 151 ralrimivva φkzX×+xr|xXr+r<1kclsJxballDrballDzMk𝒫X×+
153 3 fmpo kzX×+xr|xXr+r<1kclsJxballDrballDzMk𝒫X×+F:×X×+𝒫X×+
154 152 153 sylib φF:×X×+𝒫X×+
155 154 3ad2ant1 φnintJranMm+F:×X×+𝒫X×+
156 1z 1
157 nnuz =1
158 156 157 axdc4uz X×+VnmX×+F:×X×+𝒫X×+gg:X×+g1=nmngn+1nFgn
159 33 41 155 158 syl3anc φnintJranMm+gg:X×+g1=nmngn+1nFgn
160 simpl1 φnintJranMm+g:X×+g1=nmngn+1nFgnφ
161 160 2 syl φnintJranMm+g:X×+g1=nmngn+1nFgnDCMetX
162 160 4 syl φnintJranMm+g:X×+g1=nmngn+1nFgnM:ClsdJ
163 simpl3 φnintJranMm+g:X×+g1=nmngn+1nFgnm+
164 39 adantr φnintJranMm+g:X×+g1=nmngn+1nFgnnX
165 simpr1 φnintJranMm+g:X×+g1=nmngn+1nFgng:X×+
166 simpr2 φnintJranMm+g:X×+g1=nmngn+1nFgng1=nm
167 simpr3 φnintJranMm+g:X×+g1=nmngn+1nFgnngn+1nFgn
168 fvoveq1 n=kgn+1=gk+1
169 id n=kn=k
170 fveq2 n=kgn=gk
171 169 170 oveq12d n=knFgn=kFgk
172 168 171 eleq12d n=kgn+1nFgngk+1kFgk
173 172 cbvralvw ngn+1nFgnkgk+1kFgk
174 167 173 sylib φnintJranMm+g:X×+g1=nmngn+1nFgnkgk+1kFgk
175 1 161 3 162 163 164 165 166 174 bcthlem4 φnintJranMm+g:X×+g1=nmngn+1nFgnnballDmranM
176 159 175 exlimddv φnintJranMm+nballDmranM
177 12 ntrss2 JTopranMJintJranMranM
178 10 16 177 syl2anc φintJranMranM
179 sstr2 nballDmintJranMintJranMranMnballDmranM
180 178 179 syl5com φnballDmintJranMnballDmranM
181 ssdif0 nballDmranMnballDmranM=
182 180 181 imbitrdi φnballDmintJranMnballDmranM=
183 182 necon3ad φnballDmranM¬nballDmintJranM
184 183 3ad2ant1 φnintJranMm+nballDmranM¬nballDmintJranM
185 176 184 mpd φnintJranMm+¬nballDmintJranM
186 185 3expa φnintJranMm+¬nballDmintJranM
187 186 nrexdv φnintJranM¬m+nballDmintJranM
188 22 187 pm2.65da φ¬nintJranM
189 188 eq0rdv φintJranM=