metdsge

Description: The distance from the point A to the set S is greater than R iff the R -ball around A misses S . (Contributed by Mario Carneiro, 4-Sep-2015) (Proof shortened by AV, 30-Sep-2020)

		Ref	Expression
	Hypothesis	metdscn.f	$⊢ F = (x \in X ⟼ sup (ran (y \in S ⟼ x D y) ℝ^{*} <))$
	Assertion	metdsge	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{*}) \to (R \leq F (A) \leftrightarrow S \cap (A ball (D) R) = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	$⊢ F = (x \in X ⟼ sup (ran (y \in S ⟼ x D y) ℝ^{*} <))$
2		simpl3	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{*}) \to A \in X$
3	1	metdsval	$⊢ A \in X \to F (A) = sup (ran (y \in S ⟼ A D y) ℝ^{*} <)$
4	2 3	syl	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{}) \to F (A) = sup (ran (y \in S ⟼ A D y) ℝ^{} <)$
5	4	breq2d	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{}) \to (R \leq F (A) \leftrightarrow R \leq sup (ran (y \in S ⟼ A D y) ℝ^{} <))$
6		simpll1	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{*}) \land w \in S) \to D \in ∞Met (X)$
7	2	adantr	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{*}) \land w \in S) \to A \in X$
8		simpl2	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{*}) \to S \subseteq X$
9	8	sselda	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{*}) \land w \in S) \to w \in X$
10		xmetcl	$⊢ (D \in ∞Met (X) \land A \in X \land w \in X) \to A D w \in ℝ^{*}$
11	6 7 9 10	syl3anc	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{}) \land w \in S) \to A D w \in ℝ^{}$
12		oveq2	$⊢ y = w \to A D y = A D w$
13	12	cbvmptv	$⊢ (y \in S ⟼ A D y) = (w \in S ⟼ A D w)$
14	11 13	fmptd	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{}) \to (y \in S ⟼ A D y) : S ⟶ ℝ^{}$
15	14	frnd	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{}) \to ran (y \in S ⟼ A D y) \subseteq ℝ^{}$
16		simpr	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{}) \to R \in ℝ^{}$
17		infxrgelb	$⊢ (ran (y \in S ⟼ A D y) \subseteq ℝ^{} \land R \in ℝ^{}) \to (R \leq sup (ran (y \in S ⟼ A D y) ℝ^{*} <) \leftrightarrow \forall z \in ran (y \in S ⟼ A D y) R \leq z)$
18	15 16 17	syl2anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{}) \to (R \leq sup (ran (y \in S ⟼ A D y) ℝ^{} <) \leftrightarrow \forall z \in ran (y \in S ⟼ A D y) R \leq z)$
19	16	adantr	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{}) \land w \in S) \to R \in ℝ^{}$
20		elbl2	$⊢ ((D \in ∞Met (X) \land R \in ℝ^{*}) \land (A \in X \land w \in X)) \to (w \in (A ball (D) R) \leftrightarrow A D w < R)$
21	6 19 7 9 20	syl22anc	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{*}) \land w \in S) \to (w \in (A ball (D) R) \leftrightarrow A D w < R)$
22		xrltnle	$⊢ (A D w \in ℝ^{} \land R \in ℝ^{}) \to (A D w < R \leftrightarrow \neg R \leq A D w)$
23	11 19 22	syl2anc	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{*}) \land w \in S) \to (A D w < R \leftrightarrow \neg R \leq A D w)$
24	21 23	bitrd	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{*}) \land w \in S) \to (w \in (A ball (D) R) \leftrightarrow \neg R \leq A D w)$
25	24	con2bid	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{*}) \land w \in S) \to (R \leq A D w \leftrightarrow \neg w \in (A ball (D) R))$
26	25	ralbidva	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{*}) \to (\forall w \in S R \leq A D w \leftrightarrow \forall w \in S \neg w \in (A ball (D) R))$
27		ovex	$⊢ A D w \in V$
28	27	rgenw	$⊢ \forall w \in S A D w \in V$
29		breq2	$⊢ z = A D w \to (R \leq z \leftrightarrow R \leq A D w)$
30	13 29	ralrnmptw	$⊢ \forall w \in S A D w \in V \to (\forall z \in ran (y \in S ⟼ A D y) R \leq z \leftrightarrow \forall w \in S R \leq A D w)$
31	28 30	ax-mp	$⊢ \forall z \in ran (y \in S ⟼ A D y) R \leq z \leftrightarrow \forall w \in S R \leq A D w$
32		disj	$⊢ S \cap (A ball (D) R) = \emptyset \leftrightarrow \forall w \in S \neg w \in (A ball (D) R)$
33	26 31 32	3bitr4g	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{*}) \to (\forall z \in ran (y \in S ⟼ A D y) R \leq z \leftrightarrow S \cap (A ball (D) R) = \emptyset)$
34	5 18 33	3bitrd	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land R \in ℝ^{*}) \to (R \leq F (A) \leftrightarrow S \cap (A ball (D) R) = \emptyset)$

Metamath Proof Explorer

Theorem metdsge

Proof