Metamath Proof Explorer


Theorem metdsf

Description: The distance from a point to a set is a nonnegative extended real number. (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by Mario Carneiro, 4-Sep-2015) (Proof shortened by AV, 30-Sep-2020)

Ref Expression
Hypothesis metdscn.f 𝐹 = ( 𝑥𝑋 ↦ inf ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
Assertion metdsf ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )

Proof

Step Hyp Ref Expression
1 metdscn.f 𝐹 = ( 𝑥𝑋 ↦ inf ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
2 simplll ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ 𝑥𝑋 ) ∧ 𝑦𝑆 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3 simplr ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ 𝑥𝑋 ) ∧ 𝑦𝑆 ) → 𝑥𝑋 )
4 simplr ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ 𝑥𝑋 ) → 𝑆𝑋 )
5 4 sselda ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ 𝑥𝑋 ) ∧ 𝑦𝑆 ) → 𝑦𝑋 )
6 xmetcl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥𝑋𝑦𝑋 ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ* )
7 2 3 5 6 syl3anc ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ 𝑥𝑋 ) ∧ 𝑦𝑆 ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ* )
8 eqid ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) = ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) )
9 7 8 fmptd ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ 𝑥𝑋 ) → ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) : 𝑆 ⟶ ℝ* )
10 9 frnd ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ 𝑥𝑋 ) → ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) ⊆ ℝ* )
11 infxrcl ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) ⊆ ℝ* → inf ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ∈ ℝ* )
12 10 11 syl ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ 𝑥𝑋 ) → inf ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ∈ ℝ* )
13 xmetge0 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥𝑋𝑦𝑋 ) → 0 ≤ ( 𝑥 𝐷 𝑦 ) )
14 2 3 5 13 syl3anc ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ 𝑥𝑋 ) ∧ 𝑦𝑆 ) → 0 ≤ ( 𝑥 𝐷 𝑦 ) )
15 14 ralrimiva ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ 𝑥𝑋 ) → ∀ 𝑦𝑆 0 ≤ ( 𝑥 𝐷 𝑦 ) )
16 ovex ( 𝑥 𝐷 𝑦 ) ∈ V
17 16 rgenw 𝑦𝑆 ( 𝑥 𝐷 𝑦 ) ∈ V
18 breq2 ( 𝑧 = ( 𝑥 𝐷 𝑦 ) → ( 0 ≤ 𝑧 ↔ 0 ≤ ( 𝑥 𝐷 𝑦 ) ) )
19 8 18 ralrnmptw ( ∀ 𝑦𝑆 ( 𝑥 𝐷 𝑦 ) ∈ V → ( ∀ 𝑧 ∈ ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) 0 ≤ 𝑧 ↔ ∀ 𝑦𝑆 0 ≤ ( 𝑥 𝐷 𝑦 ) ) )
20 17 19 ax-mp ( ∀ 𝑧 ∈ ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) 0 ≤ 𝑧 ↔ ∀ 𝑦𝑆 0 ≤ ( 𝑥 𝐷 𝑦 ) )
21 15 20 sylibr ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ 𝑥𝑋 ) → ∀ 𝑧 ∈ ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) 0 ≤ 𝑧 )
22 0xr 0 ∈ ℝ*
23 infxrgelb ( ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) ⊆ ℝ* ∧ 0 ∈ ℝ* ) → ( 0 ≤ inf ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ↔ ∀ 𝑧 ∈ ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) 0 ≤ 𝑧 ) )
24 10 22 23 sylancl ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ 𝑥𝑋 ) → ( 0 ≤ inf ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ↔ ∀ 𝑧 ∈ ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) 0 ≤ 𝑧 ) )
25 21 24 mpbird ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ 𝑥𝑋 ) → 0 ≤ inf ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
26 elxrge0 ( inf ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ∈ ( 0 [,] +∞ ) ↔ ( inf ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ∈ ℝ* ∧ 0 ≤ inf ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ) )
27 12 25 26 sylanbrc ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ 𝑥𝑋 ) → inf ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
28 27 1 fmptd ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )