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 ( ( 𝐹 β€˜ 𝑧 ) ≀ ( 𝐹 β€˜ 𝑀 ) , ( ( 𝐹 β€˜ 𝑀 ) +𝑒 -𝑒 ( 𝐹 β€˜ 𝑧 ) ) , ( ( 𝐹 β€˜ 𝑧 ) +𝑒 -𝑒 ( 𝐹 β€˜ 𝑀 ) ) ) )
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 𝐾 ) )