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 ffvelcdmd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ* )
13 simprl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝑤 ∈ 𝑋 )
14 10 13 ffvelcdmd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ℝ* )
15 3 xrsdsval ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝑤 ) ∈ ℝ* ) → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) = if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +e -e ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +e -e ( 𝐹 ‘ 𝑤 ) ) ) )
16 12 14 15 syl2anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) = if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +e -e ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +e -e ( 𝐹 ‘ 𝑤 ) ) ) )
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 ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( ( 𝐹 ‘ 𝑤 ) +e -e ( 𝐹 ‘ 𝑧 ) ) < 𝑟 )
25 1 2 3 4 17 18 11 13 19 22 metdscnlem ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( ( 𝐹 ‘ 𝑧 ) +e -e ( 𝐹 ‘ 𝑤 ) ) < 𝑟 )
26 breq1 ⊢ ( ( ( 𝐹 ‘ 𝑤 ) +e -e ( 𝐹 ‘ 𝑧 ) ) = if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +e -e ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +e -e ( 𝐹 ‘ 𝑤 ) ) ) → ( ( ( 𝐹 ‘ 𝑤 ) +e -e ( 𝐹 ‘ 𝑧 ) ) < 𝑟 ↔ if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +e -e ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +e -e ( 𝐹 ‘ 𝑤 ) ) ) < 𝑟 ) )
27 breq1 ⊢ ( ( ( 𝐹 ‘ 𝑧 ) +e -e ( 𝐹 ‘ 𝑤 ) ) = if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +e -e ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +e -e ( 𝐹 ‘ 𝑤 ) ) ) → ( ( ( 𝐹 ‘ 𝑧 ) +e -e ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ↔ if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +e -e ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +e -e ( 𝐹 ‘ 𝑤 ) ) ) < 𝑟 ) )
28 26 27 ifboth ⊢ ( ( ( ( 𝐹 ‘ 𝑤 ) +e -e ( 𝐹 ‘ 𝑧 ) ) < 𝑟 ∧ ( ( 𝐹 ‘ 𝑧 ) +e -e ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) → if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +e -e ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +e -e ( 𝐹 ‘ 𝑤 ) ) ) < 𝑟 )
29 24 25 28 syl2anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +e -e ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +e -e ( 𝐹 ‘ 𝑤 ) ) ) < 𝑟 )
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 𝐾 ) )