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 ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) , ℝ* , < ) )