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 𝐹 = ( 𝑥𝑋 ↦ inf ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
metdscn.j 𝐽 = ( MetOpen ‘ 𝐷 )
metdscn.c 𝐶 = ( dist ‘ ℝ*𝑠 )
metdscn.k 𝐾 = ( MetOpen ‘ 𝐶 )
Assertion metdscn ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 metdscn.f 𝐹 = ( 𝑥𝑋 ↦ inf ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
2 metdscn.j 𝐽 = ( MetOpen ‘ 𝐷 )
3 metdscn.c 𝐶 = ( dist ‘ ℝ*𝑠 )
4 metdscn.k 𝐾 = ( MetOpen ‘ 𝐶 )
5 1 metdsf ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
6 iccssxr ( 0 [,] +∞ ) ⊆ ℝ*
7 fss ( ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ∧ ( 0 [,] +∞ ) ⊆ ℝ* ) → 𝐹 : 𝑋 ⟶ ℝ* )
8 5 6 7 sylancl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) → 𝐹 : 𝑋 ⟶ ℝ* )
9 simprr ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℝ+ )
10 8 ad2antrr ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝐹 : 𝑋 ⟶ ℝ* )
11 simplrl ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝑧𝑋 )
12 10 11 ffvelrnd ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( 𝐹𝑧 ) ∈ ℝ* )
13 simprl ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝑤𝑋 )
14 10 13 ffvelrnd ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( 𝐹𝑤 ) ∈ ℝ* )
15 3 xrsdsval ( ( ( 𝐹𝑧 ) ∈ ℝ* ∧ ( 𝐹𝑤 ) ∈ ℝ* ) → ( ( 𝐹𝑧 ) 𝐶 ( 𝐹𝑤 ) ) = if ( ( 𝐹𝑧 ) ≤ ( 𝐹𝑤 ) , ( ( 𝐹𝑤 ) +𝑒 -𝑒 ( 𝐹𝑧 ) ) , ( ( 𝐹𝑧 ) +𝑒 -𝑒 ( 𝐹𝑤 ) ) ) )
16 12 14 15 syl2anc ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( ( 𝐹𝑧 ) 𝐶 ( 𝐹𝑤 ) ) = if ( ( 𝐹𝑧 ) ≤ ( 𝐹𝑤 ) , ( ( 𝐹𝑤 ) +𝑒 -𝑒 ( 𝐹𝑧 ) ) , ( ( 𝐹𝑧 ) +𝑒 -𝑒 ( 𝐹𝑤 ) ) ) )
17 simplll ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
18 simpllr ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝑆𝑋 )
19 simplrr ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝑟 ∈ ℝ+ )
20 xmetsym ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑤𝑋𝑧𝑋 ) → ( 𝑤 𝐷 𝑧 ) = ( 𝑧 𝐷 𝑤 ) )
21 17 13 11 20 syl3anc ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( 𝑤 𝐷 𝑧 ) = ( 𝑧 𝐷 𝑤 ) )
22 simprr ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( 𝑧 𝐷 𝑤 ) < 𝑟 )
23 21 22 eqbrtrd ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( 𝑤 𝐷 𝑧 ) < 𝑟 )
24 1 2 3 4 17 18 13 11 19 23 metdscnlem ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( ( 𝐹𝑤 ) +𝑒 -𝑒 ( 𝐹𝑧 ) ) < 𝑟 )
25 1 2 3 4 17 18 11 13 19 22 metdscnlem ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( ( 𝐹𝑧 ) +𝑒 -𝑒 ( 𝐹𝑤 ) ) < 𝑟 )
26 breq1 ( ( ( 𝐹𝑤 ) +𝑒 -𝑒 ( 𝐹𝑧 ) ) = if ( ( 𝐹𝑧 ) ≤ ( 𝐹𝑤 ) , ( ( 𝐹𝑤 ) +𝑒 -𝑒 ( 𝐹𝑧 ) ) , ( ( 𝐹𝑧 ) +𝑒 -𝑒 ( 𝐹𝑤 ) ) ) → ( ( ( 𝐹𝑤 ) +𝑒 -𝑒 ( 𝐹𝑧 ) ) < 𝑟 ↔ if ( ( 𝐹𝑧 ) ≤ ( 𝐹𝑤 ) , ( ( 𝐹𝑤 ) +𝑒 -𝑒 ( 𝐹𝑧 ) ) , ( ( 𝐹𝑧 ) +𝑒 -𝑒 ( 𝐹𝑤 ) ) ) < 𝑟 ) )
27 breq1 ( ( ( 𝐹𝑧 ) +𝑒 -𝑒 ( 𝐹𝑤 ) ) = if ( ( 𝐹𝑧 ) ≤ ( 𝐹𝑤 ) , ( ( 𝐹𝑤 ) +𝑒 -𝑒 ( 𝐹𝑧 ) ) , ( ( 𝐹𝑧 ) +𝑒 -𝑒 ( 𝐹𝑤 ) ) ) → ( ( ( 𝐹𝑧 ) +𝑒 -𝑒 ( 𝐹𝑤 ) ) < 𝑟 ↔ if ( ( 𝐹𝑧 ) ≤ ( 𝐹𝑤 ) , ( ( 𝐹𝑤 ) +𝑒 -𝑒 ( 𝐹𝑧 ) ) , ( ( 𝐹𝑧 ) +𝑒 -𝑒 ( 𝐹𝑤 ) ) ) < 𝑟 ) )
28 26 27 ifboth ( ( ( ( 𝐹𝑤 ) +𝑒 -𝑒 ( 𝐹𝑧 ) ) < 𝑟 ∧ ( ( 𝐹𝑧 ) +𝑒 -𝑒 ( 𝐹𝑤 ) ) < 𝑟 ) → if ( ( 𝐹𝑧 ) ≤ ( 𝐹𝑤 ) , ( ( 𝐹𝑤 ) +𝑒 -𝑒 ( 𝐹𝑧 ) ) , ( ( 𝐹𝑧 ) +𝑒 -𝑒 ( 𝐹𝑤 ) ) ) < 𝑟 )
29 24 25 28 syl2anc ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → if ( ( 𝐹𝑧 ) ≤ ( 𝐹𝑤 ) , ( ( 𝐹𝑤 ) +𝑒 -𝑒 ( 𝐹𝑧 ) ) , ( ( 𝐹𝑧 ) +𝑒 -𝑒 ( 𝐹𝑤 ) ) ) < 𝑟 )
30 16 29 eqbrtrd ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( ( 𝐹𝑧 ) 𝐶 ( 𝐹𝑤 ) ) < 𝑟 )
31 30 expr ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) ∧ 𝑤𝑋 ) → ( ( 𝑧 𝐷 𝑤 ) < 𝑟 → ( ( 𝐹𝑧 ) 𝐶 ( 𝐹𝑤 ) ) < 𝑟 ) )
32 31 ralrimiva ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) → ∀ 𝑤𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑟 → ( ( 𝐹𝑧 ) 𝐶 ( 𝐹𝑤 ) ) < 𝑟 ) )
33 breq2 ( 𝑠 = 𝑟 → ( ( 𝑧 𝐷 𝑤 ) < 𝑠 ↔ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) )
34 33 rspceaimv ( ( 𝑟 ∈ ℝ+ ∧ ∀ 𝑤𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑟 → ( ( 𝐹𝑧 ) 𝐶 ( 𝐹𝑤 ) ) < 𝑟 ) ) → ∃ 𝑠 ∈ ℝ+𝑤𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑠 → ( ( 𝐹𝑧 ) 𝐶 ( 𝐹𝑤 ) ) < 𝑟 ) )
35 9 32 34 syl2anc ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝑧𝑋𝑟 ∈ ℝ+ ) ) → ∃ 𝑠 ∈ ℝ+𝑤𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑠 → ( ( 𝐹𝑧 ) 𝐶 ( 𝐹𝑤 ) ) < 𝑟 ) )
36 35 ralrimivva ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) → ∀ 𝑧𝑋𝑟 ∈ ℝ+𝑠 ∈ ℝ+𝑤𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑠 → ( ( 𝐹𝑧 ) 𝐶 ( 𝐹𝑤 ) ) < 𝑟 ) )
37 simpl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
38 3 xrsxmet 𝐶 ∈ ( ∞Met ‘ ℝ* )
39 2 4 metcn ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐶 ∈ ( ∞Met ‘ ℝ* ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ ℝ* ∧ ∀ 𝑧𝑋𝑟 ∈ ℝ+𝑠 ∈ ℝ+𝑤𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑠 → ( ( 𝐹𝑧 ) 𝐶 ( 𝐹𝑤 ) ) < 𝑟 ) ) ) )
40 37 38 39 sylancl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ ℝ* ∧ ∀ 𝑧𝑋𝑟 ∈ ℝ+𝑠 ∈ ℝ+𝑤𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑠 → ( ( 𝐹𝑧 ) 𝐶 ( 𝐹𝑤 ) ) < 𝑟 ) ) ) )
41 8 36 40 mpbir2and ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )