Metamath Proof Explorer


Theorem heiborlem8

Description: Lemma for heibor . The previous lemmas establish that the sequence M is Cauchy, so using completeness we now consider the convergent point Y . By assumption, U is an open cover, so Y is an element of some Z e. U , and some ball centered at Y is contained in Z . But the sequence contains arbitrarily small balls close to Y , so some element ball ( Mn ) of the sequence is contained in Z . And finally we arrive at a contradiction, because { Z } is a finite subcover of U that covers ball ( Mn ) , yet ball ( Mn ) e. K . For convenience, we write this contradiction as ph -> ps where ph is all the accumulated hypotheses and ps is anything at all. (Contributed by Jeff Madsen, 22-Jan-2014)

Ref Expression
Hypotheses heibor.1 J = MetOpen D
heibor.3 K = u | ¬ v 𝒫 U Fin u v
heibor.4 G = y n | n 0 y F n y B n K
heibor.5 B = z X , m 0 z ball D 1 2 m
heibor.6 φ D CMet X
heibor.7 φ F : 0 𝒫 X Fin
heibor.8 φ n 0 X = y F n y B n
heibor.9 φ x G T x G 2 nd x + 1 B x T x B 2 nd x + 1 K
heibor.10 φ C G 0
heibor.11 S = seq 0 T m 0 if m = 0 C m 1
heibor.12 M = n S n 3 2 n
heibor.13 φ U J
heibor.14 Y V
heibor.15 φ Y Z
heibor.16 φ Z U
heibor.17 φ 1 st M t J Y
Assertion heiborlem8 φ ψ

Proof

Step Hyp Ref Expression
1 heibor.1 J = MetOpen D
2 heibor.3 K = u | ¬ v 𝒫 U Fin u v
3 heibor.4 G = y n | n 0 y F n y B n K
4 heibor.5 B = z X , m 0 z ball D 1 2 m
5 heibor.6 φ D CMet X
6 heibor.7 φ F : 0 𝒫 X Fin
7 heibor.8 φ n 0 X = y F n y B n
8 heibor.9 φ x G T x G 2 nd x + 1 B x T x B 2 nd x + 1 K
9 heibor.10 φ C G 0
10 heibor.11 S = seq 0 T m 0 if m = 0 C m 1
11 heibor.12 M = n S n 3 2 n
12 heibor.13 φ U J
13 heibor.14 Y V
14 heibor.15 φ Y Z
15 heibor.16 φ Z U
16 heibor.17 φ 1 st M t J Y
17 cmetmet D CMet X D Met X
18 metxmet D Met X D ∞Met X
19 5 17 18 3syl φ D ∞Met X
20 12 15 sseldd φ Z J
21 1 mopni2 D ∞Met X Z J Y Z x + Y ball D x Z
22 19 20 14 21 syl3anc φ x + Y ball D x Z
23 rphalfcl x + x 2 +
24 breq2 r = x 2 2 nd M k < r 2 nd M k < x 2
25 24 rexbidv r = x 2 k 2 nd M k < r k 2 nd M k < x 2
26 1 2 3 4 5 6 7 8 9 10 11 heiborlem7 r + k 2 nd M k < r
27 25 26 vtoclri x 2 + k 2 nd M k < x 2
28 23 27 syl x + k 2 nd M k < x 2
29 28 adantl φ x + k 2 nd M k < x 2
30 nnnn0 k k 0
31 1 2 3 4 5 6 7 8 9 10 heiborlem4 φ k 0 S k G k
32 fvex S k V
33 vex k V
34 1 2 3 32 33 heiborlem2 S k G k k 0 S k F k S k B k K
35 34 simp3bi S k G k S k B k K
36 31 35 syl φ k 0 S k B k K
37 30 36 sylan2 φ k S k B k K
38 37 ad2ant2r φ x + k 2 nd M k < x 2 S k B k K
39 19 ad2antrr φ x + k 2 nd M k < x 2 D ∞Met X
40 1 2 3 4 5 6 7 8 9 10 11 heiborlem5 φ M : X × +
41 40 ffvelrnda φ k M k X × +
42 41 ad2ant2r φ x + k 2 nd M k < x 2 M k X × +
43 xp1st M k X × + 1 st M k X
44 42 43 syl φ x + k 2 nd M k < x 2 1 st M k X
45 2nn 2
46 nnexpcl 2 k 0 2 k
47 45 30 46 sylancr k 2 k
48 47 nnrpd k 2 k +
49 48 rpreccld k 1 2 k +
50 49 ad2antrl φ x + k 2 nd M k < x 2 1 2 k +
51 50 rpxrd φ x + k 2 nd M k < x 2 1 2 k *
52 xp2nd M k X × + 2 nd M k +
53 42 52 syl φ x + k 2 nd M k < x 2 2 nd M k +
54 53 rpxrd φ x + k 2 nd M k < x 2 2 nd M k *
55 1le3 1 3
56 elrp 2 k + 2 k 0 < 2 k
57 1re 1
58 3re 3
59 lediv1 1 3 2 k 0 < 2 k 1 3 1 2 k 3 2 k
60 57 58 59 mp3an12 2 k 0 < 2 k 1 3 1 2 k 3 2 k
61 56 60 sylbi 2 k + 1 3 1 2 k 3 2 k
62 55 61 mpbii 2 k + 1 2 k 3 2 k
63 48 62 syl k 1 2 k 3 2 k
64 63 ad2antrl φ x + k 2 nd M k < x 2 1 2 k 3 2 k
65 fveq2 n = k S n = S k
66 oveq2 n = k 2 n = 2 k
67 66 oveq2d n = k 3 2 n = 3 2 k
68 65 67 opeq12d n = k S n 3 2 n = S k 3 2 k
69 opex S k 3 2 k V
70 68 11 69 fvmpt k M k = S k 3 2 k
71 70 fveq2d k 2 nd M k = 2 nd S k 3 2 k
72 ovex 3 2 k V
73 32 72 op2nd 2 nd S k 3 2 k = 3 2 k
74 71 73 eqtrdi k 2 nd M k = 3 2 k
75 74 ad2antrl φ x + k 2 nd M k < x 2 2 nd M k = 3 2 k
76 64 75 breqtrrd φ x + k 2 nd M k < x 2 1 2 k 2 nd M k
77 ssbl D ∞Met X 1 st M k X 1 2 k * 2 nd M k * 1 2 k 2 nd M k 1 st M k ball D 1 2 k 1 st M k ball D 2 nd M k
78 39 44 51 54 76 77 syl221anc φ x + k 2 nd M k < x 2 1 st M k ball D 1 2 k 1 st M k ball D 2 nd M k
79 30 ad2antrl φ x + k 2 nd M k < x 2 k 0
80 oveq1 z = 1 st M k z ball D 1 2 m = 1 st M k ball D 1 2 m
81 oveq2 m = k 2 m = 2 k
82 81 oveq2d m = k 1 2 m = 1 2 k
83 82 oveq2d m = k 1 st M k ball D 1 2 m = 1 st M k ball D 1 2 k
84 ovex 1 st M k ball D 1 2 k V
85 80 83 4 84 ovmpo 1 st M k X k 0 1 st M k B k = 1 st M k ball D 1 2 k
86 44 79 85 syl2anc φ x + k 2 nd M k < x 2 1 st M k B k = 1 st M k ball D 1 2 k
87 70 fveq2d k 1 st M k = 1 st S k 3 2 k
88 32 72 op1st 1 st S k 3 2 k = S k
89 87 88 eqtrdi k 1 st M k = S k
90 89 ad2antrl φ x + k 2 nd M k < x 2 1 st M k = S k
91 90 oveq1d φ x + k 2 nd M k < x 2 1 st M k B k = S k B k
92 86 91 eqtr3d φ x + k 2 nd M k < x 2 1 st M k ball D 1 2 k = S k B k
93 df-ov 1 st M k ball D 2 nd M k = ball D 1 st M k 2 nd M k
94 1st2nd2 M k X × + M k = 1 st M k 2 nd M k
95 42 94 syl φ x + k 2 nd M k < x 2 M k = 1 st M k 2 nd M k
96 95 fveq2d φ x + k 2 nd M k < x 2 ball D M k = ball D 1 st M k 2 nd M k
97 93 96 eqtr4id φ x + k 2 nd M k < x 2 1 st M k ball D 2 nd M k = ball D M k
98 78 92 97 3sstr3d φ x + k 2 nd M k < x 2 S k B k ball D M k
99 1 mopntop D ∞Met X J Top
100 39 99 syl φ x + k 2 nd M k < x 2 J Top
101 blssm D ∞Met X 1 st M k X 2 nd M k * 1 st M k ball D 2 nd M k X
102 39 44 54 101 syl3anc φ x + k 2 nd M k < x 2 1 st M k ball D 2 nd M k X
103 1 mopnuni D ∞Met X X = J
104 39 103 syl φ x + k 2 nd M k < x 2 X = J
105 102 97 104 3sstr3d φ x + k 2 nd M k < x 2 ball D M k J
106 eqid J = J
107 106 sscls J Top ball D M k J ball D M k cls J ball D M k
108 100 105 107 syl2anc φ x + k 2 nd M k < x 2 ball D M k cls J ball D M k
109 97 fveq2d φ x + k 2 nd M k < x 2 cls J 1 st M k ball D 2 nd M k = cls J ball D M k
110 23 ad2antlr φ x + k 2 nd M k < x 2 x 2 +
111 110 rpxrd φ x + k 2 nd M k < x 2 x 2 *
112 simprr φ x + k 2 nd M k < x 2 2 nd M k < x 2
113 1 blsscls D ∞Met X 1 st M k X 2 nd M k * x 2 * 2 nd M k < x 2 cls J 1 st M k ball D 2 nd M k 1 st M k ball D x 2
114 39 44 54 111 112 113 syl23anc φ x + k 2 nd M k < x 2 cls J 1 st M k ball D 2 nd M k 1 st M k ball D x 2
115 109 114 eqsstrrd φ x + k 2 nd M k < x 2 cls J ball D M k 1 st M k ball D x 2
116 rpre x + x
117 116 ad2antlr φ x + k 2 nd M k < x 2 x
118 1 2 3 4 5 6 7 8 9 10 11 heiborlem6 φ t ball D M t + 1 ball D M t
119 19 40 118 1 caublcls φ 1 st M t J Y k Y cls J ball D M k
120 119 3expia φ 1 st M t J Y k Y cls J ball D M k
121 16 120 mpdan φ k Y cls J ball D M k
122 121 imp φ k Y cls J ball D M k
123 122 ad2ant2r φ x + k 2 nd M k < x 2 Y cls J ball D M k
124 115 123 sseldd φ x + k 2 nd M k < x 2 Y 1 st M k ball D x 2
125 blhalf D ∞Met X 1 st M k X x Y 1 st M k ball D x 2 1 st M k ball D x 2 Y ball D x
126 39 44 117 124 125 syl22anc φ x + k 2 nd M k < x 2 1 st M k ball D x 2 Y ball D x
127 115 126 sstrd φ x + k 2 nd M k < x 2 cls J ball D M k Y ball D x
128 108 127 sstrd φ x + k 2 nd M k < x 2 ball D M k Y ball D x
129 98 128 sstrd φ x + k 2 nd M k < x 2 S k B k Y ball D x
130 sstr2 S k B k Y ball D x Y ball D x Z S k B k Z
131 129 130 syl φ x + k 2 nd M k < x 2 Y ball D x Z S k B k Z
132 unisng Z U Z = Z
133 15 132 syl φ Z = Z
134 133 sseq2d φ S k B k Z S k B k Z
135 134 biimpar φ S k B k Z S k B k Z
136 15 snssd φ Z U
137 snex Z V
138 137 elpw Z 𝒫 U Z U
139 136 138 sylibr φ Z 𝒫 U
140 snfi Z Fin
141 140 a1i φ Z Fin
142 139 141 elind φ Z 𝒫 U Fin
143 unieq v = Z v = Z
144 143 sseq2d v = Z S k B k v S k B k Z
145 144 rspcev Z 𝒫 U Fin S k B k Z v 𝒫 U Fin S k B k v
146 142 145 sylan φ S k B k Z v 𝒫 U Fin S k B k v
147 135 146 syldan φ S k B k Z v 𝒫 U Fin S k B k v
148 ovex S k B k V
149 sseq1 u = S k B k u v S k B k v
150 149 rexbidv u = S k B k v 𝒫 U Fin u v v 𝒫 U Fin S k B k v
151 150 notbid u = S k B k ¬ v 𝒫 U Fin u v ¬ v 𝒫 U Fin S k B k v
152 148 151 2 elab2 S k B k K ¬ v 𝒫 U Fin S k B k v
153 152 con2bii v 𝒫 U Fin S k B k v ¬ S k B k K
154 147 153 sylib φ S k B k Z ¬ S k B k K
155 154 ex φ S k B k Z ¬ S k B k K
156 155 ad2antrr φ x + k 2 nd M k < x 2 S k B k Z ¬ S k B k K
157 131 156 syld φ x + k 2 nd M k < x 2 Y ball D x Z ¬ S k B k K
158 38 157 mt2d φ x + k 2 nd M k < x 2 ¬ Y ball D x Z
159 29 158 rexlimddv φ x + ¬ Y ball D x Z
160 159 nrexdv φ ¬ x + Y ball D x Z
161 22 160 pm2.21dd φ ψ