Metamath Proof Explorer


Theorem metdscn

Description: The function F which gives the distance from a point to a set is a continuous function into the metric topology of the extended reals. (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypotheses metdscn.f F = x X sup ran y S x D y * <
metdscn.j J = MetOpen D
metdscn.c C = dist 𝑠 *
metdscn.k K = MetOpen C
Assertion metdscn D ∞Met X S X F J Cn K

Proof

Step Hyp Ref Expression
1 metdscn.f F = x X sup ran y S x D y * <
2 metdscn.j J = MetOpen D
3 metdscn.c C = dist 𝑠 *
4 metdscn.k K = MetOpen C
5 1 metdsf D ∞Met X S X F : X 0 +∞
6 iccssxr 0 +∞ *
7 fss F : X 0 +∞ 0 +∞ * F : X *
8 5 6 7 sylancl D ∞Met X S X F : X *
9 simprr D ∞Met X S X z X r + r +
10 8 ad2antrr D ∞Met X S X z X r + w X z D w < r F : X *
11 simplrl D ∞Met X S X z X r + w X z D w < r z X
12 10 11 ffvelrnd D ∞Met X S X z X r + w X z D w < r F z *
13 simprl D ∞Met X S X z X r + w X z D w < r w X
14 10 13 ffvelrnd D ∞Met X S X z X r + w X z D w < r F w *
15 3 xrsdsval F z * F w * F z C F w = if F z F w F w + 𝑒 F z F z + 𝑒 F w
16 12 14 15 syl2anc D ∞Met X S X z X r + w X z D w < r F z C F w = if F z F w F w + 𝑒 F z F z + 𝑒 F w
17 simplll D ∞Met X S X z X r + w X z D w < r D ∞Met X
18 simpllr D ∞Met X S X z X r + w X z D w < r S X
19 simplrr D ∞Met X S X z X r + w X z D w < r r +
20 xmetsym D ∞Met X w X z X w D z = z D w
21 17 13 11 20 syl3anc D ∞Met X S X z X r + w X z D w < r w D z = z D w
22 simprr D ∞Met X S X z X r + w X z D w < r z D w < r
23 21 22 eqbrtrd D ∞Met X S X z X r + w X z D w < r w D z < r
24 1 2 3 4 17 18 13 11 19 23 metdscnlem D ∞Met X S X z X r + w X z D w < r F w + 𝑒 F z < r
25 1 2 3 4 17 18 11 13 19 22 metdscnlem D ∞Met X S X z X r + w X z D w < r F z + 𝑒 F w < r
26 breq1 F w + 𝑒 F z = if F z F w F w + 𝑒 F z F z + 𝑒 F w F w + 𝑒 F z < r if F z F w F w + 𝑒 F z F z + 𝑒 F w < r
27 breq1 F z + 𝑒 F w = if F z F w F w + 𝑒 F z F z + 𝑒 F w F z + 𝑒 F w < r if F z F w F w + 𝑒 F z F z + 𝑒 F w < r
28 26 27 ifboth F w + 𝑒 F z < r F z + 𝑒 F w < r if F z F w F w + 𝑒 F z F z + 𝑒 F w < r
29 24 25 28 syl2anc D ∞Met X S X z X r + w X z D w < r if F z F w F w + 𝑒 F z F z + 𝑒 F w < r
30 16 29 eqbrtrd D ∞Met X S X z X r + w X z D w < r F z C F w < r
31 30 expr D ∞Met X S X z X r + w X z D w < r F z C F w < r
32 31 ralrimiva D ∞Met X S X z X r + w X z D w < r F z C F w < r
33 breq2 s = r z D w < s z D w < r
34 33 rspceaimv r + w X z D w < r F z C F w < r s + w X z D w < s F z C F w < r
35 9 32 34 syl2anc D ∞Met X S X z X r + s + w X z D w < s F z C F w < r
36 35 ralrimivva D ∞Met X S X z X r + s + w X z D w < s F z C F w < r
37 simpl D ∞Met X S X D ∞Met X
38 3 xrsxmet C ∞Met *
39 2 4 metcn D ∞Met X C ∞Met * F J Cn K F : X * z X r + s + w X z D w < s F z C F w < r
40 37 38 39 sylancl D ∞Met X S X F J Cn K F : X * z X r + s + w X z D w < s F z C F w < r
41 8 36 40 mpbir2and D ∞Met X S X F J Cn K