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

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	$⊢ F = (x \in X ⟼ inf (ran (y \in S ⟼ x D y) ℝ^{*} <))$
	Assertion	metdsval	$⊢ A \in X \to F (A) = inf (ran (y \in S ⟼ A D y) ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	$⊢ F = (x \in X ⟼ inf (ran (y \in S ⟼ x D y) ℝ^{*} <))$
2		oveq1	$⊢ x = A \to x D y = A D y$
3	2	mpteq2dv	$⊢ x = A \to (y \in S ⟼ x D y) = (y \in S ⟼ A D y)$
4	3	rneqd	$⊢ x = A \to ran (y \in S ⟼ x D y) = ran (y \in S ⟼ A D y)$
5	4	infeq1d	$⊢ x = A \to inf (ran (y \in S ⟼ x D y) ℝ^{} <) = inf (ran (y \in S ⟼ A D y) ℝ^{} <)$
6		xrltso	$⊢ < Or ℝ^{*}$
7	6	infex	$⊢ inf (ran (y \in S ⟼ A D y) ℝ^{*} <) \in V$
8	5 1 7	fvmpt	$⊢ A \in X \to F (A) = inf (ran (y \in S ⟼ A D y) ℝ^{*} <)$