metdsre

Description: The distance from a point to a nonempty set in a proper metric space is a real number. (Contributed by Mario Carneiro, 5-Sep-2015)

		Ref	Expression
	Hypothesis	metdscn.f	$⊢ F = (x \in X ⟼ sup (ran (y \in S ⟼ x D y) ℝ^{*} <))$
	Assertion	metdsre	$⊢ (D \in Met (X) \land S \subseteq X \land S \neq \emptyset) \to F : X ⟶ ℝ$

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	$⊢ F = (x \in X ⟼ sup (ran (y \in S ⟼ x D y) ℝ^{*} <))$
2		n0	$⊢ S \neq \emptyset \leftrightarrow \exists z z \in S$
3		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
4	1	metdsf	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to F : X ⟶ [0, +∞]$
5	3 4	sylan	$⊢ (D \in Met (X) \land S \subseteq X) \to F : X ⟶ [0, +∞]$
6	5	adantr	$⊢ ((D \in Met (X) \land S \subseteq X) \land z \in S) \to F : X ⟶ [0, +∞]$
7	6	ffnd	$⊢ ((D \in Met (X) \land S \subseteq X) \land z \in S) \to F Fn X$
8	5	adantr	$⊢ ((D \in Met (X) \land S \subseteq X) \land (z \in S \land w \in X)) \to F : X ⟶ [0, +∞]$
9		simprr	$⊢ ((D \in Met (X) \land S \subseteq X) \land (z \in S \land w \in X)) \to w \in X$
10	8 9	ffvelrnd	$⊢ ((D \in Met (X) \land S \subseteq X) \land (z \in S \land w \in X)) \to F (w) \in [0, +∞]$
11		eliccxr	$⊢ F (w) \in [0, +∞] \to F (w) \in ℝ^{*}$
12	10 11	syl	$⊢ ((D \in Met (X) \land S \subseteq X) \land (z \in S \land w \in X)) \to F (w) \in ℝ^{*}$
13		simpll	$⊢ ((D \in Met (X) \land S \subseteq X) \land (z \in S \land w \in X)) \to D \in Met (X)$
14		simpr	$⊢ (D \in Met (X) \land S \subseteq X) \to S \subseteq X$
15	14	sselda	$⊢ ((D \in Met (X) \land S \subseteq X) \land z \in S) \to z \in X$
16	15	adantrr	$⊢ ((D \in Met (X) \land S \subseteq X) \land (z \in S \land w \in X)) \to z \in X$
17		metcl	$⊢ (D \in Met (X) \land z \in X \land w \in X) \to z D w \in ℝ$
18	13 16 9 17	syl3anc	$⊢ ((D \in Met (X) \land S \subseteq X) \land (z \in S \land w \in X)) \to z D w \in ℝ$
19		elxrge0	$⊢ F (w) \in [0, +∞] \leftrightarrow (F (w) \in ℝ^{*} \land 0 \leq F (w))$
20	19	simprbi	$⊢ F (w) \in [0, +∞] \to 0 \leq F (w)$
21	10 20	syl	$⊢ ((D \in Met (X) \land S \subseteq X) \land (z \in S \land w \in X)) \to 0 \leq F (w)$
22	1	metdsle	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (z \in S \land w \in X)) \to F (w) \leq z D w$
23	3 22	sylanl1	$⊢ ((D \in Met (X) \land S \subseteq X) \land (z \in S \land w \in X)) \to F (w) \leq z D w$
24		xrrege0	$⊢ ((F (w) \in ℝ^{*} \land z D w \in ℝ) \land (0 \leq F (w) \land F (w) \leq z D w)) \to F (w) \in ℝ$
25	12 18 21 23 24	syl22anc	$⊢ ((D \in Met (X) \land S \subseteq X) \land (z \in S \land w \in X)) \to F (w) \in ℝ$
26	25	anassrs	$⊢ (((D \in Met (X) \land S \subseteq X) \land z \in S) \land w \in X) \to F (w) \in ℝ$
27	26	ralrimiva	$⊢ ((D \in Met (X) \land S \subseteq X) \land z \in S) \to \forall w \in X F (w) \in ℝ$
28		ffnfv	$⊢ F : X ⟶ ℝ \leftrightarrow (F Fn X \land \forall w \in X F (w) \in ℝ)$
29	7 27 28	sylanbrc	$⊢ ((D \in Met (X) \land S \subseteq X) \land z \in S) \to F : X ⟶ ℝ$
30	29	ex	$⊢ (D \in Met (X) \land S \subseteq X) \to (z \in S \to F : X ⟶ ℝ)$
31	30	exlimdv	$⊢ (D \in Met (X) \land S \subseteq X) \to (\exists z z \in S \to F : X ⟶ ℝ)$
32	2 31	syl5bi	$⊢ (D \in Met (X) \land S \subseteq X) \to (S \neq \emptyset \to F : X ⟶ ℝ)$
33	32	3impia	$⊢ (D \in Met (X) \land S \subseteq X \land S \neq \emptyset) \to F : X ⟶ ℝ$

Metamath Proof Explorer

Theorem metdsre

Proof