metdsle

Description: The distance from a point to a set is bounded by the distance to any member of the set. (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	metdsle	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in S \land B \in X)) \to F (B) \leq A D B$

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	$⊢ F = (x \in X ⟼ sup (ran (y \in S ⟼ x D y) ℝ^{*} <))$
2		simprr	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in S \land B \in X)) \to B \in X$
3		simpr	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to S \subseteq X$
4	3	sselda	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land A \in S) \to A \in X$
5	4	adantrr	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in S \land B \in X)) \to A \in X$
6	2 5	jca	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in S \land B \in X)) \to (B \in X \land A \in X)$
7	1	metdstri	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (B \in X \land A \in X)) \to F (B) \leq (B D A) +_{𝑒} F (A)$
8	6 7	syldan	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in S \land B \in X)) \to F (B) \leq (B D A) +_{𝑒} F (A)$
9		simpll	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in S \land B \in X)) \to D \in ∞Met (X)$
10		xmetsym	$⊢ (D \in ∞Met (X) \land B \in X \land A \in X) \to B D A = A D B$
11	9 2 5 10	syl3anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in S \land B \in X)) \to B D A = A D B$
12	1	metds0	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to F (A) = 0$
13	12	3expa	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land A \in S) \to F (A) = 0$
14	13	adantrr	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in S \land B \in X)) \to F (A) = 0$
15	11 14	oveq12d	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in S \land B \in X)) \to (B D A) +_{𝑒} F (A) = (A D B) +_{𝑒} 0$
16		xmetcl	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to A D B \in ℝ^{*}$
17	9 5 2 16	syl3anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in S \land B \in X)) \to A D B \in ℝ^{*}$
18	17	xaddid1d	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in S \land B \in X)) \to (A D B) +_{𝑒} 0 = A D B$
19	15 18	eqtrd	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in S \land B \in X)) \to (B D A) +_{𝑒} F (A) = A D B$
20	8 19	breqtrd	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in S \land B \in X)) \to F (B) \leq A D B$

Metamath Proof Explorer

Theorem metdsle

Proof