Metamath Proof Explorer


Theorem heicant

Description: Heine-Cantor theorem: a continuous mapping between metric spaces whose domain is compact is uniformly continuous. Theorem on Rosenlicht p. 80. (Contributed by Brendan Leahy, 13-Aug-2018) (Proof shortened by AV, 27-Sep-2020)

Ref Expression
Hypotheses heicant.c φ C ∞Met X
heicant.d φ D ∞Met Y
heicant.j φ MetOpen C Comp
heicant.x φ X
heicant.y φ Y
Assertion heicant φ metUnif C uCn metUnif D = MetOpen C Cn MetOpen D

Proof

Step Hyp Ref Expression
1 heicant.c φ C ∞Met X
2 heicant.d φ D ∞Met Y
3 heicant.j φ MetOpen C Comp
4 heicant.x φ X
5 heicant.y φ Y
6 breq2 d = y f x D f w < d f x D f w < y
7 6 imbi2d d = y x C w < z f x D f w < d x C w < z f x D f w < y
8 7 2ralbidv d = y x X w X x C w < z f x D f w < d x X w X x C w < z f x D f w < y
9 8 rexbidv d = y z + x X w X x C w < z f x D f w < d z + x X w X x C w < z f x D f w < y
10 9 cbvralvw d + z + x X w X x C w < z f x D f w < d y + z + x X w X x C w < z f x D f w < y
11 r19.12 z + x X w X x C w < z f x D f w < y x X z + w X x C w < z f x D f w < y
12 11 ralimi y + z + x X w X x C w < z f x D f w < y y + x X z + w X x C w < z f x D f w < y
13 10 12 sylbi d + z + x X w X x C w < z f x D f w < d y + x X z + w X x C w < z f x D f w < y
14 rphalfcl d + d 2 +
15 breq2 y = d 2 f x D f w < y f x D f w < d 2
16 15 imbi2d y = d 2 x C w < z f x D f w < y x C w < z f x D f w < d 2
17 16 ralbidv y = d 2 w X x C w < z f x D f w < y w X x C w < z f x D f w < d 2
18 17 rexbidv y = d 2 z + w X x C w < z f x D f w < y z + w X x C w < z f x D f w < d 2
19 18 ralbidv y = d 2 x X z + w X x C w < z f x D f w < y x X z + w X x C w < z f x D f w < d 2
20 19 rspcva d 2 + y + x X z + w X x C w < z f x D f w < y x X z + w X x C w < z f x D f w < d 2
21 3 ad3antrrr φ f : X Y d + x X z + w X x C w < z f x D f w < d 2 MetOpen C Comp
22 1 ad2antrr φ f : X Y d + C ∞Met X
23 22 anim1i φ f : X Y d + x X C ∞Met X x X
24 rphalfcl z + z 2 +
25 24 rpxrd z + z 2 *
26 eqid MetOpen C = MetOpen C
27 26 blopn C ∞Met X x X z 2 * x ball C z 2 MetOpen C
28 27 3expa C ∞Met X x X z 2 * x ball C z 2 MetOpen C
29 23 25 28 syl2an φ f : X Y d + x X z + x ball C z 2 MetOpen C
30 29 adantr φ f : X Y d + x X z + w X x C w < z f x D f w < d 2 x ball C z 2 MetOpen C
31 24 rpgt0d z + 0 < z 2
32 25 31 jca z + z 2 * 0 < z 2
33 xblcntr C ∞Met X x X z 2 * 0 < z 2 x x ball C z 2
34 33 3expa C ∞Met X x X z 2 * 0 < z 2 x x ball C z 2
35 23 32 34 syl2an φ f : X Y d + x X z + x x ball C z 2
36 35 adantr φ f : X Y d + x X z + w X x C w < z f x D f w < d 2 x x ball C z 2
37 opelxpi x X z 2 + x z 2 X × +
38 24 37 sylan2 x X z + x z 2 X × +
39 38 ad4ant23 φ f : X Y d + x X z + w X x C w < z f x D f w < d 2 x z 2 X × +
40 rpcn z + z
41 40 2halvesd z + z 2 + z 2 = z
42 41 breq2d z + x C c < z 2 + z 2 x C c < z
43 42 imbi1d z + x C c < z 2 + z 2 f x D f c < d 2 x C c < z f x D f c < d 2
44 43 ralbidv z + c X x C c < z 2 + z 2 f x D f c < d 2 c X x C c < z f x D f c < d 2
45 oveq2 c = w x C c = x C w
46 45 breq1d c = w x C c < z x C w < z
47 fveq2 c = w f c = f w
48 47 oveq2d c = w f x D f c = f x D f w
49 48 breq1d c = w f x D f c < d 2 f x D f w < d 2
50 46 49 imbi12d c = w x C c < z f x D f c < d 2 x C w < z f x D f w < d 2
51 50 cbvralvw c X x C c < z f x D f c < d 2 w X x C w < z f x D f w < d 2
52 44 51 bitrdi z + c X x C c < z 2 + z 2 f x D f c < d 2 w X x C w < z f x D f w < d 2
53 52 biimpar z + w X x C w < z f x D f w < d 2 c X x C c < z 2 + z 2 f x D f c < d 2
54 53 adantll φ f : X Y d + x X z + w X x C w < z f x D f w < d 2 c X x C c < z 2 + z 2 f x D f c < d 2
55 vex x V
56 ovex z 2 V
57 55 56 op1std p = x z 2 1 st p = x
58 55 56 op2ndd p = x z 2 2 nd p = z 2
59 57 58 oveq12d p = x z 2 1 st p ball C 2 nd p = x ball C z 2
60 59 eqcomd p = x z 2 x ball C z 2 = 1 st p ball C 2 nd p
61 60 biantrurd p = x z 2 c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2 x ball C z 2 = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2
62 57 oveq1d p = x z 2 1 st p C c = x C c
63 58 58 oveq12d p = x z 2 2 nd p + 2 nd p = z 2 + z 2
64 62 63 breq12d p = x z 2 1 st p C c < 2 nd p + 2 nd p x C c < z 2 + z 2
65 57 fveq2d p = x z 2 f 1 st p = f x
66 65 oveq1d p = x z 2 f 1 st p D f c = f x D f c
67 66 breq1d p = x z 2 f 1 st p D f c < d 2 f x D f c < d 2
68 64 67 imbi12d p = x z 2 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2 x C c < z 2 + z 2 f x D f c < d 2
69 68 ralbidv p = x z 2 c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2 c X x C c < z 2 + z 2 f x D f c < d 2
70 61 69 bitr3d p = x z 2 x ball C z 2 = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2 c X x C c < z 2 + z 2 f x D f c < d 2
71 70 rspcev x z 2 X × + c X x C c < z 2 + z 2 f x D f c < d 2 p X × + x ball C z 2 = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2
72 39 54 71 syl2anc φ f : X Y d + x X z + w X x C w < z f x D f w < d 2 p X × + x ball C z 2 = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2
73 eleq2 b = x ball C z 2 x b x x ball C z 2
74 eqeq1 b = x ball C z 2 b = 1 st p ball C 2 nd p x ball C z 2 = 1 st p ball C 2 nd p
75 74 anbi1d b = x ball C z 2 b = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2 x ball C z 2 = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2
76 75 rexbidv b = x ball C z 2 p X × + b = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2 p X × + x ball C z 2 = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2
77 73 76 anbi12d b = x ball C z 2 x b p X × + b = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2 x x ball C z 2 p X × + x ball C z 2 = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2
78 77 rspcev x ball C z 2 MetOpen C x x ball C z 2 p X × + x ball C z 2 = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2 b MetOpen C x b p X × + b = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2
79 30 36 72 78 syl12anc φ f : X Y d + x X z + w X x C w < z f x D f w < d 2 b MetOpen C x b p X × + b = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2
80 79 rexlimdva2 φ f : X Y d + x X z + w X x C w < z f x D f w < d 2 b MetOpen C x b p X × + b = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2
81 80 ralimdva φ f : X Y d + x X z + w X x C w < z f x D f w < d 2 x X b MetOpen C x b p X × + b = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2
82 81 imp φ f : X Y d + x X z + w X x C w < z f x D f w < d 2 x X b MetOpen C x b p X × + b = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2
83 26 mopnuni C ∞Met X X = MetOpen C
84 1 83 syl φ X = MetOpen C
85 84 raleqdv φ x X b MetOpen C x b p X × + b = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2 x MetOpen C b MetOpen C x b p X × + b = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2
86 85 ad3antrrr φ f : X Y d + x X z + w X x C w < z f x D f w < d 2 x X b MetOpen C x b p X × + b = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2 x MetOpen C b MetOpen C x b p X × + b = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2
87 82 86 mpbid φ f : X Y d + x X z + w X x C w < z f x D f w < d 2 x MetOpen C b MetOpen C x b p X × + b = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2
88 eqid MetOpen C = MetOpen C
89 fveq2 p = g b 1 st p = 1 st g b
90 fveq2 p = g b 2 nd p = 2 nd g b
91 89 90 oveq12d p = g b 1 st p ball C 2 nd p = 1 st g b ball C 2 nd g b
92 91 eqeq2d p = g b b = 1 st p ball C 2 nd p b = 1 st g b ball C 2 nd g b
93 89 oveq1d p = g b 1 st p C c = 1 st g b C c
94 90 90 oveq12d p = g b 2 nd p + 2 nd p = 2 nd g b + 2 nd g b
95 93 94 breq12d p = g b 1 st p C c < 2 nd p + 2 nd p 1 st g b C c < 2 nd g b + 2 nd g b
96 89 fveq2d p = g b f 1 st p = f 1 st g b
97 96 oveq1d p = g b f 1 st p D f c = f 1 st g b D f c
98 97 breq1d p = g b f 1 st p D f c < d 2 f 1 st g b D f c < d 2
99 95 98 imbi12d p = g b 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2
100 99 ralbidv p = g b c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2 c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2
101 92 100 anbi12d p = g b b = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2 b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2
102 88 101 cmpcovf MetOpen C Comp x MetOpen C b MetOpen C x b p X × + b = 1 st p ball C 2 nd p c X 1 st p C c < 2 nd p + 2 nd p f 1 st p D f c < d 2 s 𝒫 MetOpen C Fin MetOpen C = s g g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2
103 21 87 102 syl2anc φ f : X Y d + x X z + w X x C w < z f x D f w < d 2 s 𝒫 MetOpen C Fin MetOpen C = s g g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2
104 103 ex φ f : X Y d + x X z + w X x C w < z f x D f w < d 2 s 𝒫 MetOpen C Fin MetOpen C = s g g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2
105 elinel2 s 𝒫 MetOpen C Fin s Fin
106 simpll φ f : X Y d + φ
107 106 anim1i φ f : X Y d + s Fin φ s Fin
108 frn g : s X × + ran g X × +
109 rnss ran g X × + ran ran g ran X × +
110 108 109 syl g : s X × + ran ran g ran X × +
111 rnxpss ran X × + +
112 110 111 sstrdi g : s X × + ran ran g +
113 112 adantl φ s Fin MetOpen C = s g : s X × + ran ran g +
114 simplr φ s Fin MetOpen C = s s Fin
115 ffun g : s X × + Fun g
116 vex g V
117 116 fundmen Fun g dom g g
118 117 ensymd Fun g g dom g
119 115 118 syl g : s X × + g dom g
120 fdm g : s X × + dom g = s
121 119 120 breqtrd g : s X × + g s
122 enfii s Fin g s g Fin
123 121 122 sylan2 s Fin g : s X × + g Fin
124 rnfi g Fin ran g Fin
125 rnfi ran g Fin ran ran g Fin
126 123 124 125 3syl s Fin g : s X × + ran ran g Fin
127 114 126 sylan φ s Fin MetOpen C = s g : s X × + ran ran g Fin
128 120 adantl φ MetOpen C = s g : s X × + dom g = s
129 eqtr X = MetOpen C MetOpen C = s X = s
130 84 129 sylan φ MetOpen C = s X = s
131 4 adantr φ MetOpen C = s X
132 130 131 eqnetrrd φ MetOpen C = s s
133 unieq s = s =
134 uni0 =
135 133 134 eqtrdi s = s =
136 135 necon3i s s
137 132 136 syl φ MetOpen C = s s
138 137 adantr φ MetOpen C = s g : s X × + s
139 128 138 eqnetrd φ MetOpen C = s g : s X × + dom g
140 dm0rn0 dom g = ran g =
141 140 necon3bii dom g ran g
142 139 141 sylib φ MetOpen C = s g : s X × + ran g
143 relxp Rel X × +
144 relss ran g X × + Rel X × + Rel ran g
145 108 143 144 mpisyl g : s X × + Rel ran g
146 relrn0 Rel ran g ran g = ran ran g =
147 146 necon3bid Rel ran g ran g ran ran g
148 145 147 syl g : s X × + ran g ran ran g
149 148 adantl φ MetOpen C = s g : s X × + ran g ran ran g
150 142 149 mpbid φ MetOpen C = s g : s X × + ran ran g
151 150 adantllr φ s Fin MetOpen C = s g : s X × + ran ran g
152 rpssre +
153 113 152 sstrdi φ s Fin MetOpen C = s g : s X × + ran ran g
154 ltso < Or
155 fiinfcl < Or ran ran g Fin ran ran g ran ran g sup ran ran g < ran ran g
156 154 155 mpan ran ran g Fin ran ran g ran ran g sup ran ran g < ran ran g
157 127 151 153 156 syl3anc φ s Fin MetOpen C = s g : s X × + sup ran ran g < ran ran g
158 113 157 sseldd φ s Fin MetOpen C = s g : s X × + sup ran ran g < +
159 107 158 sylanl1 φ f : X Y d + s Fin MetOpen C = s g : s X × + sup ran ran g < +
160 159 adantr φ f : X Y d + s Fin MetOpen C = s g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 sup ran ran g < +
161 84 ad3antrrr φ f : X Y d + s Fin X = MetOpen C
162 161 anim1i φ f : X Y d + s Fin MetOpen C = s X = MetOpen C MetOpen C = s
163 162 ad2antrr φ f : X Y d + s Fin MetOpen C = s g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 X = MetOpen C MetOpen C = s
164 simpl x X w X x X
165 129 eleq2d X = MetOpen C MetOpen C = s x X x s
166 eluni2 x s b s x b
167 165 166 bitrdi X = MetOpen C MetOpen C = s x X b s x b
168 167 biimpa X = MetOpen C MetOpen C = s x X b s x b
169 163 164 168 syl2an φ f : X Y d + s Fin MetOpen C = s g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 x X w X b s x b
170 nfv b φ f : X Y d + s Fin MetOpen C = s g : s X × +
171 nfra1 b b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2
172 170 171 nfan b φ f : X Y d + s Fin MetOpen C = s g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2
173 nfv b x X w X
174 172 173 nfan b φ f : X Y d + s Fin MetOpen C = s g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 x X w X
175 nfv b x C w < sup ran ran g < f x D f w < d
176 rspa b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2
177 oveq2 c = x 1 st g b C c = 1 st g b C x
178 177 breq1d c = x 1 st g b C c < 2 nd g b + 2 nd g b 1 st g b C x < 2 nd g b + 2 nd g b
179 fveq2 c = x f c = f x
180 179 oveq2d c = x f 1 st g b D f c = f 1 st g b D f x
181 180 breq1d c = x f 1 st g b D f c < d 2 f 1 st g b D f x < d 2
182 178 181 imbi12d c = x 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 1 st g b C x < 2 nd g b + 2 nd g b f 1 st g b D f x < d 2
183 182 rspcva x X c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 1 st g b C x < 2 nd g b + 2 nd g b f 1 st g b D f x < d 2
184 oveq2 c = w 1 st g b C c = 1 st g b C w
185 184 breq1d c = w 1 st g b C c < 2 nd g b + 2 nd g b 1 st g b C w < 2 nd g b + 2 nd g b
186 47 oveq2d c = w f 1 st g b D f c = f 1 st g b D f w
187 186 breq1d c = w f 1 st g b D f c < d 2 f 1 st g b D f w < d 2
188 185 187 imbi12d c = w 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 1 st g b C w < 2 nd g b + 2 nd g b f 1 st g b D f w < d 2
189 188 rspcva w X c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 1 st g b C w < 2 nd g b + 2 nd g b f 1 st g b D f w < d 2
190 183 189 anim12i x X c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 w X c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 1 st g b C x < 2 nd g b + 2 nd g b f 1 st g b D f x < d 2 1 st g b C w < 2 nd g b + 2 nd g b f 1 st g b D f w < d 2
191 190 anandirs x X w X c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 1 st g b C x < 2 nd g b + 2 nd g b f 1 st g b D f x < d 2 1 st g b C w < 2 nd g b + 2 nd g b f 1 st g b D f w < d 2
192 anim12 1 st g b C x < 2 nd g b + 2 nd g b f 1 st g b D f x < d 2 1 st g b C w < 2 nd g b + 2 nd g b f 1 st g b D f w < d 2 1 st g b C x < 2 nd g b + 2 nd g b 1 st g b C w < 2 nd g b + 2 nd g b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2
193 191 192 syl x X w X c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 1 st g b C x < 2 nd g b + 2 nd g b 1 st g b C w < 2 nd g b + 2 nd g b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2
194 193 adantrl x X w X b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 1 st g b C x < 2 nd g b + 2 nd g b 1 st g b C w < 2 nd g b + 2 nd g b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2
195 194 ad4ant23 φ f : X Y d + s Fin MetOpen C = s g : s X × + x X w X b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 b s x b 1 st g b C x < 2 nd g b + 2 nd g b 1 st g b C w < 2 nd g b + 2 nd g b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2
196 simpll φ f : X Y d + s Fin MetOpen C = s φ f : X Y d +
197 196 anim1i φ f : X Y d + s Fin MetOpen C = s g : s X × + φ f : X Y d + g : s X × +
198 197 anim1i φ f : X Y d + s Fin MetOpen C = s g : s X × + x X w X φ f : X Y d + g : s X × + x X w X
199 112 152 sstrdi g : s X × + ran ran g
200 199 adantr g : s X × + b s ran ran g
201 0re 0
202 rpge0 y + 0 y
203 202 rgen y + 0 y
204 ssralv ran ran g + y + 0 y y ran ran g 0 y
205 112 203 204 mpisyl g : s X × + y ran ran g 0 y
206 breq1 x = 0 x y 0 y
207 206 ralbidv x = 0 y ran ran g x y y ran ran g 0 y
208 207 rspcev 0 y ran ran g 0 y x y ran ran g x y
209 201 205 208 sylancr g : s X × + x y ran ran g x y
210 209 adantr g : s X × + b s x y ran ran g x y
211 145 adantr g : s X × + b s Rel ran g
212 ffn g : s X × + g Fn s
213 fnfvelrn g Fn s b s g b ran g
214 212 213 sylan g : s X × + b s g b ran g
215 2ndrn Rel ran g g b ran g 2 nd g b ran ran g
216 211 214 215 syl2anc g : s X × + b s 2 nd g b ran ran g
217 infrelb ran ran g x y ran ran g x y 2 nd g b ran ran g sup ran ran g < 2 nd g b
218 200 210 216 217 syl3anc g : s X × + b s sup ran ran g < 2 nd g b
219 218 adantll φ f : X Y d + g : s X × + b s sup ran ran g < 2 nd g b
220 219 ad2ant2r φ f : X Y d + g : s X × + x X w X b s x b sup ran ran g < 2 nd g b
221 1 ad3antrrr φ f : X Y d + g : s X × + C ∞Met X
222 xmetcl C ∞Met X x X w X x C w *
223 222 3expb C ∞Met X x X w X x C w *
224 221 223 sylan φ f : X Y d + g : s X × + x X w X x C w *
225 224 adantr φ f : X Y d + g : s X × + x X w X b s x b x C w *
226 simplr φ f : X Y d + g : s X × + x X w X g : s X × +
227 simpl b s x b b s
228 216 ne0d g : s X × + b s ran ran g
229 infrecl ran ran g ran ran g x y ran ran g x y sup ran ran g <
230 200 228 210 229 syl3anc g : s X × + b s sup ran ran g <
231 230 rexrd g : s X × + b s sup ran ran g < *
232 226 227 231 syl2an φ f : X Y d + g : s X × + x X w X b s x b sup ran ran g < *
233 simpr φ f : X Y d + g : s X × + g : s X × +
234 233 ffvelrnda φ f : X Y d + g : s X × + b s g b X × +
235 xp2nd g b X × + 2 nd g b +
236 234 235 syl φ f : X Y d + g : s X × + b s 2 nd g b +
237 236 rpxrd φ f : X Y d + g : s X × + b s 2 nd g b *
238 237 ad2ant2r φ f : X Y d + g : s X × + x X w X b s x b 2 nd g b *
239 xrltletr x C w * sup ran ran g < * 2 nd g b * x C w < sup ran ran g < sup ran ran g < 2 nd g b x C w < 2 nd g b
240 225 232 238 239 syl3anc φ f : X Y d + g : s X × + x X w X b s x b x C w < sup ran ran g < sup ran ran g < 2 nd g b x C w < 2 nd g b
241 220 240 mpan2d φ f : X Y d + g : s X × + x X w X b s x b x C w < sup ran ran g < x C w < 2 nd g b
242 241 adantlr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < sup ran ran g < x C w < 2 nd g b
243 1 ad6antr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b C ∞Met X
244 simpllr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b g : s X × +
245 ffvelrn g : s X × + b s g b X × +
246 xp1st g b X × + 1 st g b X
247 245 246 syl g : s X × + b s 1 st g b X
248 244 227 247 syl2an φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b 1 st g b X
249 simpr x X w X w X
250 249 ad3antlr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b w X
251 xmetcl C ∞Met X 1 st g b X w X 1 st g b C w *
252 243 248 250 251 syl3anc φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b 1 st g b C w *
253 252 adantr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < 2 nd g b 1 st g b C w *
254 245 235 syl g : s X × + b s 2 nd g b +
255 226 254 sylan φ f : X Y d + g : s X × + x X w X b s 2 nd g b +
256 255 ad2ant2r φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b 2 nd g b +
257 256 rpred φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b 2 nd g b
258 164 ad3antlr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x X
259 xmetcl C ∞Met X 1 st g b X x X 1 st g b C x *
260 243 248 258 259 syl3anc φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b 1 st g b C x *
261 254 rpxrd g : s X × + b s 2 nd g b *
262 244 227 261 syl2an φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b 2 nd g b *
263 eleq2 b = 1 st g b ball C 2 nd g b x b x 1 st g b ball C 2 nd g b
264 1 ad5antr φ f : X Y d + g : s X × + x X w X b s C ∞Met X
265 226 247 sylan φ f : X Y d + g : s X × + x X w X b s 1 st g b X
266 255 rpxrd φ f : X Y d + g : s X × + x X w X b s 2 nd g b *
267 elbl C ∞Met X 1 st g b X 2 nd g b * x 1 st g b ball C 2 nd g b x X 1 st g b C x < 2 nd g b
268 264 265 266 267 syl3anc φ f : X Y d + g : s X × + x X w X b s x 1 st g b ball C 2 nd g b x X 1 st g b C x < 2 nd g b
269 263 268 sylan9bbr φ f : X Y d + g : s X × + x X w X b s b = 1 st g b ball C 2 nd g b x b x X 1 st g b C x < 2 nd g b
270 269 biimpd φ f : X Y d + g : s X × + x X w X b s b = 1 st g b ball C 2 nd g b x b x X 1 st g b C x < 2 nd g b
271 270 an32s φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x X 1 st g b C x < 2 nd g b
272 271 impr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x X 1 st g b C x < 2 nd g b
273 272 simprd φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b 1 st g b C x < 2 nd g b
274 260 262 273 xrltled φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b 1 st g b C x 2 nd g b
275 226 ffvelrnda φ f : X Y d + g : s X × + x X w X b s g b X × +
276 275 246 syl φ f : X Y d + g : s X × + x X w X b s 1 st g b X
277 simplrl φ f : X Y d + g : s X × + x X w X b s x X
278 264 276 277 259 syl3anc φ f : X Y d + g : s X × + x X w X b s 1 st g b C x *
279 xmetge0 C ∞Met X 1 st g b X x X 0 1 st g b C x
280 264 276 277 279 syl3anc φ f : X Y d + g : s X × + x X w X b s 0 1 st g b C x
281 xrrege0 1 st g b C x * 2 nd g b 0 1 st g b C x 1 st g b C x 2 nd g b 1 st g b C x
282 281 an4s 1 st g b C x * 0 1 st g b C x 2 nd g b 1 st g b C x 2 nd g b 1 st g b C x
283 282 ex 1 st g b C x * 0 1 st g b C x 2 nd g b 1 st g b C x 2 nd g b 1 st g b C x
284 278 280 283 syl2anc φ f : X Y d + g : s X × + x X w X b s 2 nd g b 1 st g b C x 2 nd g b 1 st g b C x
285 284 ad2ant2r φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b 2 nd g b 1 st g b C x 2 nd g b 1 st g b C x
286 257 274 285 mp2and φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b 1 st g b C x
287 286 adantr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < 2 nd g b 1 st g b C x
288 xrltle x C w * 2 nd g b * x C w < 2 nd g b x C w 2 nd g b
289 225 238 288 syl2anc φ f : X Y d + g : s X × + x X w X b s x b x C w < 2 nd g b x C w 2 nd g b
290 xmetge0 C ∞Met X x X w X 0 x C w
291 290 3expb C ∞Met X x X w X 0 x C w
292 221 291 sylan φ f : X Y d + g : s X × + x X w X 0 x C w
293 292 adantr φ f : X Y d + g : s X × + x X w X b s x b 0 x C w
294 236 rpred φ f : X Y d + g : s X × + b s 2 nd g b
295 294 ad2ant2r φ f : X Y d + g : s X × + x X w X b s x b 2 nd g b
296 xrrege0 x C w * 2 nd g b 0 x C w x C w 2 nd g b x C w
297 296 ex x C w * 2 nd g b 0 x C w x C w 2 nd g b x C w
298 225 295 297 syl2anc φ f : X Y d + g : s X × + x X w X b s x b 0 x C w x C w 2 nd g b x C w
299 293 298 mpand φ f : X Y d + g : s X × + x X w X b s x b x C w 2 nd g b x C w
300 289 299 syld φ f : X Y d + g : s X × + x X w X b s x b x C w < 2 nd g b x C w
301 300 adantlr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < 2 nd g b x C w
302 301 imp φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < 2 nd g b x C w
303 287 302 readdcld φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < 2 nd g b 1 st g b C x + x C w
304 303 rexrd φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < 2 nd g b 1 st g b C x + x C w *
305 256 256 rpaddcld φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b 2 nd g b + 2 nd g b +
306 305 rpxrd φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b 2 nd g b + 2 nd g b *
307 306 adantr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < 2 nd g b 2 nd g b + 2 nd g b *
308 xmettri C ∞Met X 1 st g b X w X x X 1 st g b C w 1 st g b C x + 𝑒 x C w
309 243 248 250 258 308 syl13anc φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b 1 st g b C w 1 st g b C x + 𝑒 x C w
310 309 adantr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < 2 nd g b 1 st g b C w 1 st g b C x + 𝑒 x C w
311 rexadd 1 st g b C x x C w 1 st g b C x + 𝑒 x C w = 1 st g b C x + x C w
312 287 302 311 syl2anc φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < 2 nd g b 1 st g b C x + 𝑒 x C w = 1 st g b C x + x C w
313 310 312 breqtrd φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < 2 nd g b 1 st g b C w 1 st g b C x + x C w
314 257 adantr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < 2 nd g b 2 nd g b
315 273 adantr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < 2 nd g b 1 st g b C x < 2 nd g b
316 simpr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < 2 nd g b x C w < 2 nd g b
317 287 302 314 314 315 316 lt2addd φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < 2 nd g b 1 st g b C x + x C w < 2 nd g b + 2 nd g b
318 253 304 307 313 317 xrlelttrd φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < 2 nd g b 1 st g b C w < 2 nd g b + 2 nd g b
319 318 ex φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < 2 nd g b 1 st g b C w < 2 nd g b + 2 nd g b
320 254 rpred g : s X × + b s 2 nd g b
321 320 254 ltaddrpd g : s X × + b s 2 nd g b < 2 nd g b + 2 nd g b
322 244 227 321 syl2an φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b 2 nd g b < 2 nd g b + 2 nd g b
323 260 262 306 273 322 xrlttrd φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b 1 st g b C x < 2 nd g b + 2 nd g b
324 319 323 jctild φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < 2 nd g b 1 st g b C x < 2 nd g b + 2 nd g b 1 st g b C w < 2 nd g b + 2 nd g b
325 242 324 syld φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b x C w < sup ran ran g < 1 st g b C x < 2 nd g b + 2 nd g b 1 st g b C w < 2 nd g b + 2 nd g b
326 simpll φ f : X Y d + g : s X × + φ f : X Y
327 ffvelrn f : X Y x X f x Y
328 ffvelrn f : X Y w X f w Y
329 327 328 anim12dan f : X Y x X w X f x Y f w Y
330 xmetcl D ∞Met Y f x Y f w Y f x D f w *
331 330 3expb D ∞Met Y f x Y f w Y f x D f w *
332 2 329 331 syl2an φ f : X Y x X w X f x D f w *
333 332 anassrs φ f : X Y x X w X f x D f w *
334 326 333 sylan φ f : X Y d + g : s X × + x X w X f x D f w *
335 334 ad3antrrr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f x D f w *
336 2 ad5antr φ f : X Y d + g : s X × + x X w X b s D ∞Met Y
337 simp-5r φ f : X Y d + g : s X × + x X w X b s f : X Y
338 337 276 ffvelrnd φ f : X Y d + g : s X × + x X w X b s f 1 st g b Y
339 simpllr φ f : X Y d + g : s X × + f : X Y
340 339 ffvelrnda φ f : X Y d + g : s X × + x X f x Y
341 340 adantrr φ f : X Y d + g : s X × + x X w X f x Y
342 341 adantr φ f : X Y d + g : s X × + x X w X b s f x Y
343 xmetcl D ∞Met Y f 1 st g b Y f x Y f 1 st g b D f x *
344 336 338 342 343 syl3anc φ f : X Y d + g : s X × + x X w X b s f 1 st g b D f x *
345 14 rpxrd d + d 2 *
346 345 ad4antlr φ f : X Y d + g : s X × + x X w X b s d 2 *
347 xrltle f 1 st g b D f x * d 2 * f 1 st g b D f x < d 2 f 1 st g b D f x d 2
348 344 346 347 syl2anc φ f : X Y d + g : s X × + x X w X b s f 1 st g b D f x < d 2 f 1 st g b D f x d 2
349 xmetge0 D ∞Met Y f 1 st g b Y f x Y 0 f 1 st g b D f x
350 336 338 342 349 syl3anc φ f : X Y d + g : s X × + x X w X b s 0 f 1 st g b D f x
351 14 rpred d + d 2
352 351 ad4antlr φ f : X Y d + g : s X × + x X w X b s d 2
353 xrrege0 f 1 st g b D f x * d 2 0 f 1 st g b D f x f 1 st g b D f x d 2 f 1 st g b D f x
354 353 ex f 1 st g b D f x * d 2 0 f 1 st g b D f x f 1 st g b D f x d 2 f 1 st g b D f x
355 344 352 354 syl2anc φ f : X Y d + g : s X × + x X w X b s 0 f 1 st g b D f x f 1 st g b D f x d 2 f 1 st g b D f x
356 350 355 mpand φ f : X Y d + g : s X × + x X w X b s f 1 st g b D f x d 2 f 1 st g b D f x
357 348 356 syld φ f : X Y d + g : s X × + x X w X b s f 1 st g b D f x < d 2 f 1 st g b D f x
358 357 ad2ant2r φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f x
359 358 imp φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f x
360 339 ffvelrnda φ f : X Y d + g : s X × + w X f w Y
361 360 adantrl φ f : X Y d + g : s X × + x X w X f w Y
362 361 adantr φ f : X Y d + g : s X × + x X w X b s f w Y
363 xmetcl D ∞Met Y f 1 st g b Y f w Y f 1 st g b D f w *
364 336 338 362 363 syl3anc φ f : X Y d + g : s X × + x X w X b s f 1 st g b D f w *
365 xrltle f 1 st g b D f w * d 2 * f 1 st g b D f w < d 2 f 1 st g b D f w d 2
366 364 346 365 syl2anc φ f : X Y d + g : s X × + x X w X b s f 1 st g b D f w < d 2 f 1 st g b D f w d 2
367 xmetge0 D ∞Met Y f 1 st g b Y f w Y 0 f 1 st g b D f w
368 336 338 362 367 syl3anc φ f : X Y d + g : s X × + x X w X b s 0 f 1 st g b D f w
369 xrrege0 f 1 st g b D f w * d 2 0 f 1 st g b D f w f 1 st g b D f w d 2 f 1 st g b D f w
370 369 ex f 1 st g b D f w * d 2 0 f 1 st g b D f w f 1 st g b D f w d 2 f 1 st g b D f w
371 364 352 370 syl2anc φ f : X Y d + g : s X × + x X w X b s 0 f 1 st g b D f w f 1 st g b D f w d 2 f 1 st g b D f w
372 368 371 mpand φ f : X Y d + g : s X × + x X w X b s f 1 st g b D f w d 2 f 1 st g b D f w
373 366 372 syld φ f : X Y d + g : s X × + x X w X b s f 1 st g b D f w < d 2 f 1 st g b D f w
374 373 ad2ant2r φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f w < d 2 f 1 st g b D f w
375 374 imp φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f w < d 2 f 1 st g b D f w
376 readdcl f 1 st g b D f x f 1 st g b D f w f 1 st g b D f x + f 1 st g b D f w
377 359 375 376 syl2an φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f w < d 2 f 1 st g b D f x + f 1 st g b D f w
378 377 anandis φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f 1 st g b D f x + f 1 st g b D f w
379 378 rexrd φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f 1 st g b D f x + f 1 st g b D f w *
380 rpxr d + d *
381 380 ad6antlr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 d *
382 xmettri D ∞Met Y f x Y f w Y f 1 st g b Y f x D f w f x D f 1 st g b + 𝑒 f 1 st g b D f w
383 336 342 362 338 382 syl13anc φ f : X Y d + g : s X × + x X w X b s f x D f w f x D f 1 st g b + 𝑒 f 1 st g b D f w
384 383 ad2ant2r φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f x D f w f x D f 1 st g b + 𝑒 f 1 st g b D f w
385 384 adantr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f x D f w f x D f 1 st g b + 𝑒 f 1 st g b D f w
386 xmetsym D ∞Met Y f x Y f 1 st g b Y f x D f 1 st g b = f 1 st g b D f x
387 336 342 338 386 syl3anc φ f : X Y d + g : s X × + x X w X b s f x D f 1 st g b = f 1 st g b D f x
388 387 ad2ant2r φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f x D f 1 st g b = f 1 st g b D f x
389 388 adantr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f x D f 1 st g b = f 1 st g b D f x
390 389 oveq1d φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f x D f 1 st g b + 𝑒 f 1 st g b D f w = f 1 st g b D f x + 𝑒 f 1 st g b D f w
391 rexadd f 1 st g b D f x f 1 st g b D f w f 1 st g b D f x + 𝑒 f 1 st g b D f w = f 1 st g b D f x + f 1 st g b D f w
392 359 375 391 syl2an φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f w < d 2 f 1 st g b D f x + 𝑒 f 1 st g b D f w = f 1 st g b D f x + f 1 st g b D f w
393 392 anandis φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f 1 st g b D f x + 𝑒 f 1 st g b D f w = f 1 st g b D f x + f 1 st g b D f w
394 390 393 eqtrd φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f x D f 1 st g b + 𝑒 f 1 st g b D f w = f 1 st g b D f x + f 1 st g b D f w
395 385 394 breqtrd φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f x D f w f 1 st g b D f x + f 1 st g b D f w
396 lt2add f 1 st g b D f x f 1 st g b D f w d 2 d 2 f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f 1 st g b D f x + f 1 st g b D f w < d 2 + d 2
397 396 expcom d 2 d 2 f 1 st g b D f x f 1 st g b D f w f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f 1 st g b D f x + f 1 st g b D f w < d 2 + d 2
398 352 352 397 syl2anc φ f : X Y d + g : s X × + x X w X b s f 1 st g b D f x f 1 st g b D f w f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f 1 st g b D f x + f 1 st g b D f w < d 2 + d 2
399 357 373 398 syl2and φ f : X Y d + g : s X × + x X w X b s f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f 1 st g b D f x + f 1 st g b D f w < d 2 + d 2
400 399 pm2.43d φ f : X Y d + g : s X × + x X w X b s f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f 1 st g b D f x + f 1 st g b D f w < d 2 + d 2
401 400 ad2ant2r φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f 1 st g b D f x + f 1 st g b D f w < d 2 + d 2
402 401 imp φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f 1 st g b D f x + f 1 st g b D f w < d 2 + d 2
403 rpcn d + d
404 403 2halvesd d + d 2 + d 2 = d
405 404 ad6antlr φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 d 2 + d 2 = d
406 402 405 breqtrd φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f 1 st g b D f x + f 1 st g b D f w < d
407 335 379 381 395 406 xrlelttrd φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f x D f w < d
408 407 ex φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 f x D f w < d
409 325 408 imim12d φ f : X Y d + g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b 1 st g b C x < 2 nd g b + 2 nd g b 1 st g b C w < 2 nd g b + 2 nd g b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 x C w < sup ran ran g < f x D f w < d
410 198 409 sylanl1 φ f : X Y d + s Fin MetOpen C = s g : s X × + x X w X b = 1 st g b ball C 2 nd g b b s x b 1 st g b C x < 2 nd g b + 2 nd g b 1 st g b C w < 2 nd g b + 2 nd g b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 x C w < sup ran ran g < f x D f w < d
411 410 adantlrr φ f : X Y d + s Fin MetOpen C = s g : s X × + x X w X b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 b s x b 1 st g b C x < 2 nd g b + 2 nd g b 1 st g b C w < 2 nd g b + 2 nd g b f 1 st g b D f x < d 2 f 1 st g b D f w < d 2 x C w < sup ran ran g < f x D f w < d
412 195 411 mpd φ f : X Y d + s Fin MetOpen C = s g : s X × + x X w X b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 b s x b x C w < sup ran ran g < f x D f w < d
413 412 exp32 φ f : X Y d + s Fin MetOpen C = s g : s X × + x X w X b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 b s x b x C w < sup ran ran g < f x D f w < d
414 176 413 sylan2 φ f : X Y d + s Fin MetOpen C = s g : s X × + x X w X b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 b s b s x b x C w < sup ran ran g < f x D f w < d
415 414 expr φ f : X Y d + s Fin MetOpen C = s g : s X × + x X w X b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 b s b s x b x C w < sup ran ran g < f x D f w < d
416 415 pm2.43d φ f : X Y d + s Fin MetOpen C = s g : s X × + x X w X b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 b s x b x C w < sup ran ran g < f x D f w < d
417 416 an32s φ f : X Y d + s Fin MetOpen C = s g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 x X w X b s x b x C w < sup ran ran g < f x D f w < d
418 174 175 417 rexlimd φ f : X Y d + s Fin MetOpen C = s g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 x X w X b s x b x C w < sup ran ran g < f x D f w < d
419 169 418 mpd φ f : X Y d + s Fin MetOpen C = s g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 x X w X x C w < sup ran ran g < f x D f w < d
420 419 ralrimivva φ f : X Y d + s Fin MetOpen C = s g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 x X w X x C w < sup ran ran g < f x D f w < d
421 breq2 z = sup ran ran g < x C w < z x C w < sup ran ran g <
422 421 imbi1d z = sup ran ran g < x C w < z f x D f w < d x C w < sup ran ran g < f x D f w < d
423 422 2ralbidv z = sup ran ran g < x X w X x C w < z f x D f w < d x X w X x C w < sup ran ran g < f x D f w < d
424 423 rspcev sup ran ran g < + x X w X x C w < sup ran ran g < f x D f w < d z + x X w X x C w < z f x D f w < d
425 160 420 424 syl2anc φ f : X Y d + s Fin MetOpen C = s g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 z + x X w X x C w < z f x D f w < d
426 425 expl φ f : X Y d + s Fin MetOpen C = s g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 z + x X w X x C w < z f x D f w < d
427 426 exlimdv φ f : X Y d + s Fin MetOpen C = s g g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 z + x X w X x C w < z f x D f w < d
428 427 expimpd φ f : X Y d + s Fin MetOpen C = s g g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 z + x X w X x C w < z f x D f w < d
429 105 428 sylan2 φ f : X Y d + s 𝒫 MetOpen C Fin MetOpen C = s g g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 z + x X w X x C w < z f x D f w < d
430 429 rexlimdva φ f : X Y d + s 𝒫 MetOpen C Fin MetOpen C = s g g : s X × + b s b = 1 st g b ball C 2 nd g b c X 1 st g b C c < 2 nd g b + 2 nd g b f 1 st g b D f c < d 2 z + x X w X x C w < z f x D f w < d
431 104 430 syld φ f : X Y d + x X z + w X x C w < z f x D f w < d 2 z + x X w X x C w < z f x D f w < d
432 20 431 syl5 φ f : X Y d + d 2 + y + x X z + w X x C w < z f x D f w < y z + x X w X x C w < z f x D f w < d
433 432 exp4b φ f : X Y d + d 2 + y + x X z + w X x C w < z f x D f w < y z + x X w X x C w < z f x D f w < d
434 14 433 mpdi φ f : X Y d + y + x X z + w X x C w < z f x D f w < y z + x X w X x C w < z f x D f w < d
435 434 ralrimiv φ f : X Y d + y + x X z + w X x C w < z f x D f w < y z + x X w X x C w < z f x D f w < d
436 r19.21v d + y + x X z + w X x C w < z f x D f w < y z + x X w X x C w < z f x D f w < d y + x X z + w X x C w < z f x D f w < y d + z + x X w X x C w < z f x D f w < d
437 435 436 sylib φ f : X Y y + x X z + w X x C w < z f x D f w < y d + z + x X w X x C w < z f x D f w < d
438 13 437 impbid2 φ f : X Y d + z + x X w X x C w < z f x D f w < d y + x X z + w X x C w < z f x D f w < y
439 ralcom y + x X z + w X x C w < z f x D f w < y x X y + z + w X x C w < z f x D f w < y
440 438 439 bitrdi φ f : X Y d + z + x X w X x C w < z f x D f w < d x X y + z + w X x C w < z f x D f w < y
441 440 pm5.32da φ f : X Y d + z + x X w X x C w < z f x D f w < d f : X Y x X y + z + w X x C w < z f x D f w < y
442 eqid metUnif C = metUnif C
443 eqid metUnif D = metUnif D
444 xmetpsmet C ∞Met X C PsMet X
445 1 444 syl φ C PsMet X
446 xmetpsmet D ∞Met Y D PsMet Y
447 2 446 syl φ D PsMet Y
448 442 443 4 5 445 447 metucn φ f metUnif C uCn metUnif D f : X Y d + z + x X w X x C w < z f x D f w < d
449 eqid MetOpen D = MetOpen D
450 26 449 metcn C ∞Met X D ∞Met Y f MetOpen C Cn MetOpen D f : X Y x X y + z + w X x C w < z f x D f w < y
451 1 2 450 syl2anc φ f MetOpen C Cn MetOpen D f : X Y x X y + z + w X x C w < z f x D f w < y
452 441 448 451 3bitr4d φ f metUnif C uCn metUnif D f MetOpen C Cn MetOpen D
453 452 eqrdv φ metUnif C uCn metUnif D = MetOpen C Cn MetOpen D