blcld

Description: A "closed ball" in a metric space is actually closed. (Contributed by Mario Carneiro, 31-Dec-2013) (Revised by Mario Carneiro, 24-Aug-2015)

	Ref	Expression
Hypotheses	mopni.1	$⊢ J = MetOpen (D)$
	blcld.3	$⊢ S = \{z \in X \| P D z \leq R\}$
Assertion	blcld	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to S \in Clsd (J)$

Proof

Step	Hyp	Ref	Expression
1		mopni.1	$⊢ J = MetOpen (D)$
2		blcld.3	$⊢ S = \{z \in X \| P D z \leq R\}$
3	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
4	3	3ad2ant1	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to X = ⋃ J$
5	4	difeq1d	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to X ∖ S = ⋃ J ∖ S$
6		difssd	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to X ∖ S \subseteq X$
7		simpl3	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{}) \land y \in (X ∖ S)) \to R \in ℝ^{}$
8		simpl1	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \to D \in ∞Met (X)$
9		simpl2	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \to P \in X$
10		eldifi	$⊢ y \in (X ∖ S) \to y \in X$
11	10	adantl	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \to y \in X$
12		xmetcl	$⊢ (D \in ∞Met (X) \land P \in X \land y \in X) \to P D y \in ℝ^{*}$
13	8 9 11 12	syl3anc	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{}) \land y \in (X ∖ S)) \to P D y \in ℝ^{}$
14		eldif	$⊢ y \in (X ∖ S) \leftrightarrow (y \in X \land \neg y \in S)$
15		oveq2	$⊢ z = y \to P D z = P D y$
16	15	breq1d	$⊢ z = y \to (P D z \leq R \leftrightarrow P D y \leq R)$
17	16 2	elrab2	$⊢ y \in S \leftrightarrow (y \in X \land P D y \leq R)$
18	17	simplbi2	$⊢ y \in X \to (P D y \leq R \to y \in S)$
19	18	con3dimp	$⊢ (y \in X \land \neg y \in S) \to \neg P D y \leq R$
20	14 19	sylbi	$⊢ y \in (X ∖ S) \to \neg P D y \leq R$
21	20	adantl	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \to \neg P D y \leq R$
22		xrltnle	$⊢ (R \in ℝ^{} \land P D y \in ℝ^{}) \to (R < P D y \leftrightarrow \neg P D y \leq R)$
23	7 13 22	syl2anc	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \to (R < P D y \leftrightarrow \neg P D y \leq R)$
24	21 23	mpbird	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \to R < P D y$
25		qbtwnxr	$⊢ (R \in ℝ^{} \land P D y \in ℝ^{} \land R < P D y) \to \exists x \in ℚ (R < x \land x < P D y)$
26	7 13 24 25	syl3anc	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \to \exists x \in ℚ (R < x \land x < P D y)$
27		qre	$⊢ x \in ℚ \to x \in ℝ$
28	8	adantr	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to D \in ∞Met (X)$
29	11	adantr	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to y \in X$
30	13	adantr	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to P D y \in ℝ^{}$
31		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
32	31	ad2antrl	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to x \in ℝ^{}$
33	32	xnegcld	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to - x \in ℝ^{}$
34	30 33	xaddcld	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to (P D y) +_{𝑒} (- x) \in ℝ^{}$
35		blelrn	$⊢ (D \in ∞Met (X) \land y \in X \land (P D y) +_{𝑒} (- x) \in ℝ^{*}) \to y ball (D) ((P D y) +_{𝑒} (- x)) \in ran ball (D)$
36	28 29 34 35	syl3anc	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to y ball (D) ((P D y) +_{𝑒} (- x)) \in ran ball (D)$
37		simprrr	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to x < P D y$
38		xposdif	$⊢ (x \in ℝ^{} \land P D y \in ℝ^{}) \to (x < P D y \leftrightarrow 0 < (P D y) +_{𝑒} (- x))$
39	32 30 38	syl2anc	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to (x < P D y \leftrightarrow 0 < (P D y) +_{𝑒} (- x))$
40	37 39	mpbid	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to 0 < (P D y) +_{𝑒} (- x)$
41		xblcntr	$⊢ (D \in ∞Met (X) \land y \in X \land ((P D y) +_{𝑒} (- x) \in ℝ^{*} \land 0 < (P D y) +_{𝑒} (- x))) \to y \in (y ball (D) ((P D y) +_{𝑒} (- x)))$
42	28 29 34 40 41	syl112anc	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to y \in (y ball (D) ((P D y) +_{𝑒} (- x)))$
43		incom	$⊢ (y ball (D) ((P D y) +_{𝑒} (- x))) \cap (P ball (D) x) = (P ball (D) x) \cap (y ball (D) ((P D y) +_{𝑒} (- x)))$
44	9	adantr	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to P \in X$
45		xaddcom	$⊢ (x \in ℝ^{} \land (P D y) +_{𝑒} (- x) \in ℝ^{}) \to x +_{𝑒} ((P D y) +_{𝑒} (- x)) = ((P D y) +_{𝑒} (- x)) +_{𝑒} x$
46	32 34 45	syl2anc	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to x +_{𝑒} ((P D y) +_{𝑒} (- x)) = ((P D y) +_{𝑒} (- x)) +_{𝑒} x$
47		simprl	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to x \in ℝ$
48		xnpcan	$⊢ (P D y \in ℝ^{*} \land x \in ℝ) \to ((P D y) +_{𝑒} (- x)) +_{𝑒} x = P D y$
49	30 47 48	syl2anc	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to ((P D y) +_{𝑒} (- x)) +_{𝑒} x = P D y$
50	46 49	eqtrd	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to x +_{𝑒} ((P D y) +_{𝑒} (- x)) = P D y$
51	30	xrleidd	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to P D y \leq P D y$
52	50 51	eqbrtrd	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to x +_{𝑒} ((P D y) +_{𝑒} (- x)) \leq P D y$
53		bldisj	$⊢ ((D \in ∞Met (X) \land P \in X \land y \in X) \land (x \in ℝ^{} \land (P D y) +_{𝑒} (- x) \in ℝ^{} \land x +_{𝑒} ((P D y) +_{𝑒} (- x)) \leq P D y)) \to (P ball (D) x) \cap (y ball (D) ((P D y) +_{𝑒} (- x))) = \emptyset$
54	28 44 29 32 34 52 53	syl33anc	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to (P ball (D) x) \cap (y ball (D) ((P D y) +_{𝑒} (- x))) = \emptyset$
55	43 54	eqtrid	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to (y ball (D) ((P D y) +_{𝑒} (- x))) \cap (P ball (D) x) = \emptyset$
56		blssm	$⊢ (D \in ∞Met (X) \land y \in X \land (P D y) +_{𝑒} (- x) \in ℝ^{*}) \to y ball (D) ((P D y) +_{𝑒} (- x)) \subseteq X$
57	28 29 34 56	syl3anc	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to y ball (D) ((P D y) +_{𝑒} (- x)) \subseteq X$
58		reldisj	$⊢ y ball (D) ((P D y) +_{𝑒} (- x)) \subseteq X \to ((y ball (D) ((P D y) +_{𝑒} (- x))) \cap (P ball (D) x) = \emptyset \leftrightarrow y ball (D) ((P D y) +_{𝑒} (- x)) \subseteq X ∖ (P ball (D) x))$
59	57 58	syl	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to ((y ball (D) ((P D y) +_{𝑒} (- x))) \cap (P ball (D) x) = \emptyset \leftrightarrow y ball (D) ((P D y) +_{𝑒} (- x)) \subseteq X ∖ (P ball (D) x))$
60	55 59	mpbid	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to y ball (D) ((P D y) +_{𝑒} (- x)) \subseteq X ∖ (P ball (D) x)$
61	7	adantr	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to R \in ℝ^{}$
62		simprrl	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to R < x$
63	1 2	blsscls2	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land x \in ℝ^{} \land R < x)) \to S \subseteq P ball (D) x$
64	28 44 61 32 62 63	syl23anc	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to S \subseteq P ball (D) x$
65	64	sscond	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to X ∖ (P ball (D) x) \subseteq X ∖ S$
66	60 65	sstrd	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to y ball (D) ((P D y) +_{𝑒} (- x)) \subseteq X ∖ S$
67		eleq2	$⊢ w = y ball (D) ((P D y) +_{𝑒} (- x)) \to (y \in w \leftrightarrow y \in (y ball (D) ((P D y) +_{𝑒} (- x))))$
68		sseq1	$⊢ w = y ball (D) ((P D y) +_{𝑒} (- x)) \to (w \subseteq X ∖ S \leftrightarrow y ball (D) ((P D y) +_{𝑒} (- x)) \subseteq X ∖ S)$
69	67 68	anbi12d	$⊢ w = y ball (D) ((P D y) +_{𝑒} (- x)) \to ((y \in w \land w \subseteq X ∖ S) \leftrightarrow (y \in (y ball (D) ((P D y) +_{𝑒} (- x))) \land y ball (D) ((P D y) +_{𝑒} (- x)) \subseteq X ∖ S))$
70	69	rspcev	$⊢ (y ball (D) ((P D y) +_{𝑒} (- x)) \in ran ball (D) \land (y \in (y ball (D) ((P D y) +_{𝑒} (- x))) \land y ball (D) ((P D y) +_{𝑒} (- x)) \subseteq X ∖ S)) \to \exists w \in ran ball (D) (y \in w \land w \subseteq X ∖ S)$
71	36 42 66 70	syl12anc	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land (x \in ℝ \land (R < x \land x < P D y))) \to \exists w \in ran ball (D) (y \in w \land w \subseteq X ∖ S)$
72	71	expr	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land x \in ℝ) \to ((R < x \land x < P D y) \to \exists w \in ran ball (D) (y \in w \land w \subseteq X ∖ S))$
73	27 72	sylan2	$⊢ (((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \land x \in ℚ) \to ((R < x \land x < P D y) \to \exists w \in ran ball (D) (y \in w \land w \subseteq X ∖ S))$
74	73	rexlimdva	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \to (\exists x \in ℚ (R < x \land x < P D y) \to \exists w \in ran ball (D) (y \in w \land w \subseteq X ∖ S))$
75	26 74	mpd	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land y \in (X ∖ S)) \to \exists w \in ran ball (D) (y \in w \land w \subseteq X ∖ S)$
76	75	ralrimiva	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to \forall y \in (X ∖ S) \exists w \in ran ball (D) (y \in w \land w \subseteq X ∖ S)$
77	1	elmopn	$⊢ D \in ∞Met (X) \to (X ∖ S \in J \leftrightarrow (X ∖ S \subseteq X \land \forall y \in (X ∖ S) \exists w \in ran ball (D) (y \in w \land w \subseteq X ∖ S)))$
78	77	3ad2ant1	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to (X ∖ S \in J \leftrightarrow (X ∖ S \subseteq X \land \forall y \in (X ∖ S) \exists w \in ran ball (D) (y \in w \land w \subseteq X ∖ S)))$
79	6 76 78	mpbir2and	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to X ∖ S \in J$
80	5 79	eqeltrrd	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to ⋃ J ∖ S \in J$
81	1	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
82	81	3ad2ant1	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to J \in Top$
83	2	ssrab3	$⊢ S \subseteq X$
84	83 4	sseqtrid	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to S \subseteq ⋃ J$
85		eqid	$⊢ ⋃ J = ⋃ J$
86	85	iscld2	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (S \in Clsd (J) \leftrightarrow ⋃ J ∖ S \in J)$
87	82 84 86	syl2anc	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to (S \in Clsd (J) \leftrightarrow ⋃ J ∖ S \in J)$
88	80 87	mpbird	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to S \in Clsd (J)$

Metamath Proof Explorer

Theorem blcld

Proof