blcls

Description: The closure of an open ball in a metric space is contained in the corresponding closed ball. (Equality need not hold; for example, with the discrete metric, the closed ball of radius 1 is the whole space, but the open ball of radius 1 is just a point, whose closure is also a point.) (Contributed by Mario Carneiro, 31-Dec-2013)

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

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 2	blcld	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to S \in Clsd (J)$
4		blssm	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to P ball (D) R \subseteq X$
5		elbl	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to (z \in (P ball (D) R) \leftrightarrow (z \in X \land P D z < R))$
6		xmetcl	$⊢ (D \in ∞Met (X) \land P \in X \land z \in X) \to P D z \in ℝ^{*}$
7	6	3expa	$⊢ ((D \in ∞Met (X) \land P \in X) \land z \in X) \to P D z \in ℝ^{*}$
8	7	3adantl3	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{}) \land z \in X) \to P D z \in ℝ^{}$
9		simpl3	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{}) \land z \in X) \to R \in ℝ^{}$
10		xrltle	$⊢ (P D z \in ℝ^{} \land R \in ℝ^{}) \to (P D z < R \to P D z \leq R)$
11	8 9 10	syl2anc	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land z \in X) \to (P D z < R \to P D z \leq R)$
12	11	expimpd	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to ((z \in X \land P D z < R) \to P D z \leq R)$
13	5 12	sylbid	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to (z \in (P ball (D) R) \to P D z \leq R)$
14	13	ralrimiv	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to \forall z \in (P ball (D) R) P D z \leq R$
15		ssrab	$⊢ P ball (D) R \subseteq \{z \in X \| P D z \leq R\} \leftrightarrow (P ball (D) R \subseteq X \land \forall z \in (P ball (D) R) P D z \leq R)$
16	4 14 15	sylanbrc	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to P ball (D) R \subseteq \{z \in X \| P D z \leq R\}$
17	16 2	sseqtrrdi	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to P ball (D) R \subseteq S$
18		eqid	$⊢ ⋃ J = ⋃ J$
19	18	clsss2	$⊢ (S \in Clsd (J) \land P ball (D) R \subseteq S) \to cls (J) (P ball (D) R) \subseteq S$
20	3 17 19	syl2anc	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to cls (J) (P ball (D) R) \subseteq S$

Metamath Proof Explorer

Theorem blcls

Proof