This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 [,] +∞ ) )