blsscls2

Description: A smaller closed ball is contained in a larger open ball. (Contributed by Mario Carneiro, 10-Jan-2014)

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

Proof

Step	Hyp	Ref	Expression
1		mopni.1	$⊢ J = MetOpen (D)$
2		blcld.3	$⊢ S = \{z \in X \| P D z \leq R\}$
3		simplr3	$⊢ (((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land T \in ℝ^{} \land R < T)) \land z \in X) \to R < T$
4		xmetcl	$⊢ (D \in ∞Met (X) \land P \in X \land z \in X) \to P D z \in ℝ^{*}$
5	4	ad4ant124	$⊢ (((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land T \in ℝ^{} \land R < T)) \land z \in X) \to P D z \in ℝ^{*}$
6		simplr1	$⊢ (((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land T \in ℝ^{} \land R < T)) \land z \in X) \to R \in ℝ^{*}$
7		simplr2	$⊢ (((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land T \in ℝ^{} \land R < T)) \land z \in X) \to T \in ℝ^{*}$
8		xrlelttr	$⊢ (P D z \in ℝ^{} \land R \in ℝ^{} \land T \in ℝ^{*}) \to ((P D z \leq R \land R < T) \to P D z < T)$
9	8	expcomd	$⊢ (P D z \in ℝ^{} \land R \in ℝ^{} \land T \in ℝ^{*}) \to (R < T \to (P D z \leq R \to P D z < T))$
10	5 6 7 9	syl3anc	$⊢ (((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land T \in ℝ^{} \land R < T)) \land z \in X) \to (R < T \to (P D z \leq R \to P D z < T))$
11	3 10	mpd	$⊢ (((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land T \in ℝ^{} \land R < T)) \land z \in X) \to (P D z \leq R \to P D z < T)$
12		simp2	$⊢ (R \in ℝ^{} \land T \in ℝ^{} \land R < T) \to T \in ℝ^{*}$
13		elbl2	$⊢ ((D \in ∞Met (X) \land T \in ℝ^{*}) \land (P \in X \land z \in X)) \to (z \in (P ball (D) T) \leftrightarrow P D z < T)$
14	13	an4s	$⊢ ((D \in ∞Met (X) \land P \in X) \land (T \in ℝ^{*} \land z \in X)) \to (z \in (P ball (D) T) \leftrightarrow P D z < T)$
15	12 14	sylanr1	$⊢ ((D \in ∞Met (X) \land P \in X) \land ((R \in ℝ^{} \land T \in ℝ^{} \land R < T) \land z \in X)) \to (z \in (P ball (D) T) \leftrightarrow P D z < T)$
16	15	anassrs	$⊢ (((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land T \in ℝ^{} \land R < T)) \land z \in X) \to (z \in (P ball (D) T) \leftrightarrow P D z < T)$
17	11 16	sylibrd	$⊢ (((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land T \in ℝ^{} \land R < T)) \land z \in X) \to (P D z \leq R \to z \in (P ball (D) T))$
18	17	ralrimiva	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land T \in ℝ^{} \land R < T)) \to \forall z \in X (P D z \leq R \to z \in (P ball (D) T))$
19		rabss	$⊢ \{z \in X \| P D z \leq R\} \subseteq P ball (D) T \leftrightarrow \forall z \in X (P D z \leq R \to z \in (P ball (D) T))$
20	18 19	sylibr	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land T \in ℝ^{} \land R < T)) \to \{z \in X \| P D z \leq R\} \subseteq P ball (D) T$
21	2 20	eqsstrid	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land T \in ℝ^{} \land R < T)) \to S \subseteq P ball (D) T$

Metamath Proof Explorer

Theorem blsscls2

Proof