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	$⊢ F = (x \in X ⟼ inf (ran (y \in S ⟼ x D y) ℝ^{*} <))$
	Assertion	metdsf	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to F : X ⟶ [0, +∞]$

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	$⊢ F = (x \in X ⟼ inf (ran (y \in S ⟼ x D y) ℝ^{*} <))$
2		simplll	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land x \in X) \land y \in S) \to D \in ∞Met (X)$
3		simplr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land x \in X) \land y \in S) \to x \in X$
4		simplr	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land x \in X) \to S \subseteq X$
5	4	sselda	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land x \in X) \land y \in S) \to y \in X$
6		xmetcl	$⊢ (D \in ∞Met (X) \land x \in X \land y \in X) \to x D y \in ℝ^{*}$
7	2 3 5 6	syl3anc	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land x \in X) \land y \in S) \to x D y \in ℝ^{*}$
8		eqid	$⊢ (y \in S ⟼ x D y) = (y \in S ⟼ x D y)$
9	7 8	fmptd	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land x \in X) \to (y \in S ⟼ x D y) : S ⟶ ℝ^{*}$
10	9	frnd	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land x \in X) \to ran (y \in S ⟼ x D y) \subseteq ℝ^{*}$
11		infxrcl	$⊢ ran (y \in S ⟼ x D y) \subseteq ℝ^{} \to inf (ran (y \in S ⟼ x D y) ℝ^{} <) \in ℝ^{*}$
12	10 11	syl	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land x \in X) \to inf (ran (y \in S ⟼ x D y) ℝ^{} <) \in ℝ^{}$
13		xmetge0	$⊢ (D \in ∞Met (X) \land x \in X \land y \in X) \to 0 \leq x D y$
14	2 3 5 13	syl3anc	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land x \in X) \land y \in S) \to 0 \leq x D y$
15	14	ralrimiva	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land x \in X) \to \forall y \in S 0 \leq x D y$
16		ovex	$⊢ x D y \in V$
17	16	rgenw	$⊢ \forall y \in S x D y \in V$
18		breq2	$⊢ z = x D y \to (0 \leq z \leftrightarrow 0 \leq x D y)$
19	8 18	ralrnmptw	$⊢ \forall y \in S x D y \in V \to (\forall z \in ran (y \in S ⟼ x D y) 0 \leq z \leftrightarrow \forall y \in S 0 \leq x D y)$
20	17 19	ax-mp	$⊢ \forall z \in ran (y \in S ⟼ x D y) 0 \leq z \leftrightarrow \forall y \in S 0 \leq x D y$
21	15 20	sylibr	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land x \in X) \to \forall z \in ran (y \in S ⟼ x D y) 0 \leq z$
22		0xr	$⊢ 0 \in ℝ^{*}$
23		infxrgelb	$⊢ (ran (y \in S ⟼ x D y) \subseteq ℝ^{} \land 0 \in ℝ^{}) \to (0 \leq inf (ran (y \in S ⟼ x D y) ℝ^{*} <) \leftrightarrow \forall z \in ran (y \in S ⟼ x D y) 0 \leq z)$
24	10 22 23	sylancl	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land x \in X) \to (0 \leq inf (ran (y \in S ⟼ x D y) ℝ^{*} <) \leftrightarrow \forall z \in ran (y \in S ⟼ x D y) 0 \leq z)$
25	21 24	mpbird	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land x \in X) \to 0 \leq inf (ran (y \in S ⟼ x D y) ℝ^{*} <)$
26		elxrge0	$⊢ inf (ran (y \in S ⟼ x D y) ℝ^{} <) \in [0, +∞] \leftrightarrow (inf (ran (y \in S ⟼ x D y) ℝ^{} <) \in ℝ^{} \land 0 \leq inf (ran (y \in S ⟼ x D y) ℝ^{} <))$
27	12 25 26	sylanbrc	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land x \in X) \to inf (ran (y \in S ⟼ x D y) ℝ^{*} <) \in [0, +∞]$
28	27 1	fmptd	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to F : X ⟶ [0, +∞]$

Metamath Proof Explorer

Theorem metdsf

Proof