Metamath Proof Explorer


Theorem metdsval

Description: Value of the "distance to a set" function. (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by Mario Carneiro, 4-Sep-2015) (Revised by AV, 30-Sep-2020)

Ref Expression
Hypothesis metdscn.f 𝐹 = ( 𝑥𝑋 ↦ inf ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
Assertion metdsval ( 𝐴𝑋 → ( 𝐹𝐴 ) = inf ( ran ( 𝑦𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 metdscn.f 𝐹 = ( 𝑥𝑋 ↦ inf ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
2 oveq1 ( 𝑥 = 𝐴 → ( 𝑥 𝐷 𝑦 ) = ( 𝐴 𝐷 𝑦 ) )
3 2 mpteq2dv ( 𝑥 = 𝐴 → ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) = ( 𝑦𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) )
4 3 rneqd ( 𝑥 = 𝐴 → ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) = ran ( 𝑦𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) )
5 4 infeq1d ( 𝑥 = 𝐴 → inf ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) = inf ( ran ( 𝑦𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) , ℝ* , < ) )
6 xrltso < Or ℝ*
7 6 infex inf ( ran ( 𝑦𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) , ℝ* , < ) ∈ V
8 5 1 7 fvmpt ( 𝐴𝑋 → ( 𝐹𝐴 ) = inf ( ran ( 𝑦𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) , ℝ* , < ) )