metdseq0

Description: The distance from a point to a set is zero iff the point is in the closure set. (Contributed by Mario Carneiro, 14-Feb-2015)

	Ref	Expression
Hypotheses	metdscn.f	$⊢ F = (x \in X ⟼ sup (ran (y \in S ⟼ x D y) ℝ^{*} <))$
	metdscn.j	$⊢ J = MetOpen (D)$
Assertion	metdseq0	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in X) \to (F (A) = 0 \leftrightarrow A \in cls (J) (S))$

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	$⊢ F = (x \in X ⟼ sup (ran (y \in S ⟼ x D y) ℝ^{*} <))$
2		metdscn.j	$⊢ J = MetOpen (D)$
3		simpll1	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \to D \in ∞Met (X)$
4		simprl	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \to z \in J$
5		simprr	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \to A \in z$
6	2	mopni2	$⊢ (D \in ∞Met (X) \land z \in J \land A \in z) \to \exists r \in ℝ^{+} A ball (D) r \subseteq z$
7	3 4 5 6	syl3anc	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \to \exists r \in ℝ^{+} A ball (D) r \subseteq z$
8		simprr	$⊢ ((((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \land (r \in ℝ^{+} \land A ball (D) r \subseteq z)) \to A ball (D) r \subseteq z$
9	8	ssrind	$⊢ ((((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \land (r \in ℝ^{+} \land A ball (D) r \subseteq z)) \to (A ball (D) r) \cap S \subseteq z \cap S$
10		rpgt0	$⊢ r \in ℝ^{+} \to 0 < r$
11		0re	$⊢ 0 \in ℝ$
12		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
13		ltnle	$⊢ (0 \in ℝ \land r \in ℝ) \to (0 < r \leftrightarrow \neg r \leq 0)$
14	11 12 13	sylancr	$⊢ r \in ℝ^{+} \to (0 < r \leftrightarrow \neg r \leq 0)$
15	10 14	mpbid	$⊢ r \in ℝ^{+} \to \neg r \leq 0$
16	15	ad2antrl	$⊢ ((((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \land (r \in ℝ^{+} \land A ball (D) r \subseteq z)) \to \neg r \leq 0$
17		simpllr	$⊢ ((((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \land (r \in ℝ^{+} \land A ball (D) r \subseteq z)) \to F (A) = 0$
18	17	breq2d	$⊢ ((((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \land (r \in ℝ^{+} \land A ball (D) r \subseteq z)) \to (r \leq F (A) \leftrightarrow r \leq 0)$
19	3	adantr	$⊢ ((((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \land (r \in ℝ^{+} \land A ball (D) r \subseteq z)) \to D \in ∞Met (X)$
20		simpl2	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \to S \subseteq X$
21	20	ad2antrr	$⊢ ((((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \land (r \in ℝ^{+} \land A ball (D) r \subseteq z)) \to S \subseteq X$
22		simpl3	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \to A \in X$
23	22	ad2antrr	$⊢ ((((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \land (r \in ℝ^{+} \land A ball (D) r \subseteq z)) \to A \in X$
24		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
25	24	ad2antrl	$⊢ ((((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \land (r \in ℝ^{+} \land A ball (D) r \subseteq z)) \to r \in ℝ^{*}$
26	1	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)$
27	19 21 23 25 26	syl31anc	$⊢ ((((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \land (r \in ℝ^{+} \land A ball (D) r \subseteq z)) \to (r \leq F (A) \leftrightarrow S \cap (A ball (D) r) = \emptyset)$
28	18 27	bitr3d	$⊢ ((((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \land (r \in ℝ^{+} \land A ball (D) r \subseteq z)) \to (r \leq 0 \leftrightarrow S \cap (A ball (D) r) = \emptyset)$
29		incom	$⊢ S \cap (A ball (D) r) = (A ball (D) r) \cap S$
30	29	eqeq1i	$⊢ S \cap (A ball (D) r) = \emptyset \leftrightarrow (A ball (D) r) \cap S = \emptyset$
31	28 30	bitrdi	$⊢ ((((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \land (r \in ℝ^{+} \land A ball (D) r \subseteq z)) \to (r \leq 0 \leftrightarrow (A ball (D) r) \cap S = \emptyset)$
32	31	necon3bbid	$⊢ ((((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \land (r \in ℝ^{+} \land A ball (D) r \subseteq z)) \to (\neg r \leq 0 \leftrightarrow (A ball (D) r) \cap S \neq \emptyset)$
33	16 32	mpbid	$⊢ ((((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \land (r \in ℝ^{+} \land A ball (D) r \subseteq z)) \to (A ball (D) r) \cap S \neq \emptyset$
34		ssn0	$⊢ ((A ball (D) r) \cap S \subseteq z \cap S \land (A ball (D) r) \cap S \neq \emptyset) \to z \cap S \neq \emptyset$
35	9 33 34	syl2anc	$⊢ ((((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \land (r \in ℝ^{+} \land A ball (D) r \subseteq z)) \to z \cap S \neq \emptyset$
36	7 35	rexlimddv	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land (z \in J \land A \in z)) \to z \cap S \neq \emptyset$
37	36	expr	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \land z \in J) \to (A \in z \to z \cap S \neq \emptyset)$
38	37	ralrimiva	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \to \forall z \in J (A \in z \to z \cap S \neq \emptyset)$
39	2	mopntopon	$⊢ D \in ∞Met (X) \to J \in TopOn (X)$
40	39	3ad2ant1	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in X) \to J \in TopOn (X)$
41	40	adantr	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \to J \in TopOn (X)$
42		topontop	$⊢ J \in TopOn (X) \to J \in Top$
43	41 42	syl	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \to J \in Top$
44		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
45	41 44	syl	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \to X = ⋃ J$
46	20 45	sseqtrd	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \to S \subseteq ⋃ J$
47	22 45	eleqtrd	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \to A \in ⋃ J$
48		eqid	$⊢ ⋃ J = ⋃ J$
49	48	elcls	$⊢ (J \in Top \land S \subseteq ⋃ J \land A \in ⋃ J) \to (A \in cls (J) (S) \leftrightarrow \forall z \in J (A \in z \to z \cap S \neq \emptyset))$
50	43 46 47 49	syl3anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \to (A \in cls (J) (S) \leftrightarrow \forall z \in J (A \in z \to z \cap S \neq \emptyset))$
51	38 50	mpbird	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) = 0) \to A \in cls (J) (S)$
52		incom	$⊢ (A ball (D) F (A)) \cap S = S \cap (A ball (D) F (A))$
53	1	metdsf	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to F : X ⟶ [0, +∞]$
54	53	ffvelrnda	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land A \in X) \to F (A) \in [0, +∞]$
55	54	3impa	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in X) \to F (A) \in [0, +∞]$
56		eliccxr	$⊢ F (A) \in [0, +∞] \to F (A) \in ℝ^{*}$
57	55 56	syl	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in X) \to F (A) \in ℝ^{*}$
58	57	xrleidd	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in X) \to F (A) \leq F (A)$
59	1	metdsge	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) \in ℝ^{*}) \to (F (A) \leq F (A) \leftrightarrow S \cap (A ball (D) F (A)) = \emptyset)$
60	57 59	mpdan	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in X) \to (F (A) \leq F (A) \leftrightarrow S \cap (A ball (D) F (A)) = \emptyset)$
61	58 60	mpbid	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in X) \to S \cap (A ball (D) F (A)) = \emptyset$
62	52 61	syl5eq	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in X) \to (A ball (D) F (A)) \cap S = \emptyset$
63	62	adantr	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \to (A ball (D) F (A)) \cap S = \emptyset$
64	40	ad2antrr	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \land 0 < F (A)) \to J \in TopOn (X)$
65	64 42	syl	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \land 0 < F (A)) \to J \in Top$
66		simpll2	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \land 0 < F (A)) \to S \subseteq X$
67	64 44	syl	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \land 0 < F (A)) \to X = ⋃ J$
68	66 67	sseqtrd	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \land 0 < F (A)) \to S \subseteq ⋃ J$
69		simplr	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \land 0 < F (A)) \to A \in cls (J) (S)$
70		simpll1	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \land 0 < F (A)) \to D \in ∞Met (X)$
71		simpll3	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \land 0 < F (A)) \to A \in X$
72	57	ad2antrr	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \land 0 < F (A)) \to F (A) \in ℝ^{*}$
73	2	blopn	$⊢ (D \in ∞Met (X) \land A \in X \land F (A) \in ℝ^{*}) \to A ball (D) F (A) \in J$
74	70 71 72 73	syl3anc	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \land 0 < F (A)) \to A ball (D) F (A) \in J$
75		simpr	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \land 0 < F (A)) \to 0 < F (A)$
76		xblcntr	$⊢ (D \in ∞Met (X) \land A \in X \land (F (A) \in ℝ^{*} \land 0 < F (A))) \to A \in (A ball (D) F (A))$
77	70 71 72 75 76	syl112anc	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \land 0 < F (A)) \to A \in (A ball (D) F (A))$
78	48	clsndisj	$⊢ ((J \in Top \land S \subseteq ⋃ J \land A \in cls (J) (S)) \land (A ball (D) F (A) \in J \land A \in (A ball (D) F (A)))) \to (A ball (D) F (A)) \cap S \neq \emptyset$
79	65 68 69 74 77 78	syl32anc	$⊢ (((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \land 0 < F (A)) \to (A ball (D) F (A)) \cap S \neq \emptyset$
80	79	ex	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \to (0 < F (A) \to (A ball (D) F (A)) \cap S \neq \emptyset)$
81	80	necon2bd	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \to ((A ball (D) F (A)) \cap S = \emptyset \to \neg 0 < F (A))$
82	63 81	mpd	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \to \neg 0 < F (A)$
83		elxrge0	$⊢ F (A) \in [0, +∞] \leftrightarrow (F (A) \in ℝ^{*} \land 0 \leq F (A))$
84	83	simprbi	$⊢ F (A) \in [0, +∞] \to 0 \leq F (A)$
85	55 84	syl	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in X) \to 0 \leq F (A)$
86		0xr	$⊢ 0 \in ℝ^{*}$
87		xrleloe	$⊢ (0 \in ℝ^{} \land F (A) \in ℝ^{}) \to (0 \leq F (A) \leftrightarrow (0 < F (A) \lor 0 = F (A)))$
88	86 57 87	sylancr	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in X) \to (0 \leq F (A) \leftrightarrow (0 < F (A) \lor 0 = F (A)))$
89	85 88	mpbid	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in X) \to (0 < F (A) \lor 0 = F (A))$
90	89	adantr	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \to (0 < F (A) \lor 0 = F (A))$
91	90	ord	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \to (\neg 0 < F (A) \to 0 = F (A))$
92	82 91	mpd	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \to 0 = F (A)$
93	92	eqcomd	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land A \in cls (J) (S)) \to F (A) = 0$
94	51 93	impbida	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in X) \to (F (A) = 0 \leftrightarrow A \in cls (J) (S))$

Metamath Proof Explorer

Theorem metdseq0

Proof