blbnd

Description: A ball is bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 15-Jan-2014)

		Ref	Expression
	Assertion	blbnd	$⊢ (M \in ∞Met (X) \land Y \in X \land R \in ℝ) \to {M ↾}_{((Y ball (M) R) \times (Y ball (M) R))} \in Bnd (Y ball (M) R)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (M \in ∞Met (X) \land Y \in X \land R \in ℝ) \to M \in ∞Met (X)$
2		rexr	$⊢ R \in ℝ \to R \in ℝ^{*}$
3		blssm	$⊢ (M \in ∞Met (X) \land Y \in X \land R \in ℝ^{*}) \to Y ball (M) R \subseteq X$
4	2 3	syl3an3	$⊢ (M \in ∞Met (X) \land Y \in X \land R \in ℝ) \to Y ball (M) R \subseteq X$
5		xmetres2	$⊢ (M \in ∞Met (X) \land Y ball (M) R \subseteq X) \to {M ↾}_{((Y ball (M) R) \times (Y ball (M) R))} \in ∞Met (Y ball (M) R)$
6	1 4 5	syl2anc	$⊢ (M \in ∞Met (X) \land Y \in X \land R \in ℝ) \to {M ↾}_{((Y ball (M) R) \times (Y ball (M) R))} \in ∞Met (Y ball (M) R)$
7	6	adantr	$⊢ ((M \in ∞Met (X) \land Y \in X \land R \in ℝ) \land Y ball (M) R = \emptyset) \to {M ↾}_{((Y ball (M) R) \times (Y ball (M) R))} \in ∞Met (Y ball (M) R)$
8		rzal	$⊢ Y ball (M) R = \emptyset \to \forall x \in (Y ball (M) R) \exists r \in ℝ^{+} Y ball (M) R = x ball ({M ↾}_{((Y ball (M) R) \times (Y ball (M) R))}) r$
9	8	adantl	$⊢ ((M \in ∞Met (X) \land Y \in X \land R \in ℝ) \land Y ball (M) R = \emptyset) \to \forall x \in (Y ball (M) R) \exists r \in ℝ^{+} Y ball (M) R = x ball ({M ↾}_{((Y ball (M) R) \times (Y ball (M) R))}) r$
10		isbndx	$⊢ {M ↾}_{((Y ball (M) R) \times (Y ball (M) R))} \in Bnd (Y ball (M) R) \leftrightarrow ({M ↾}_{((Y ball (M) R) \times (Y ball (M) R))} \in ∞Met (Y ball (M) R) \land \forall x \in (Y ball (M) R) \exists r \in ℝ^{+} Y ball (M) R = x ball ({M ↾}_{((Y ball (M) R) \times (Y ball (M) R))}) r)$
11	7 9 10	sylanbrc	$⊢ ((M \in ∞Met (X) \land Y \in X \land R \in ℝ) \land Y ball (M) R = \emptyset) \to {M ↾}_{((Y ball (M) R) \times (Y ball (M) R))} \in Bnd (Y ball (M) R)$
12	6	adantr	$⊢ ((M \in ∞Met (X) \land Y \in X \land R \in ℝ) \land Y ball (M) R \neq \emptyset) \to {M ↾}_{((Y ball (M) R) \times (Y ball (M) R))} \in ∞Met (Y ball (M) R)$
13	1	adantr	$⊢ ((M \in ∞Met (X) \land Y \in X \land R \in ℝ) \land Y ball (M) R \neq \emptyset) \to M \in ∞Met (X)$
14		simpl2	$⊢ ((M \in ∞Met (X) \land Y \in X \land R \in ℝ) \land Y ball (M) R \neq \emptyset) \to Y \in X$
15		simpl3	$⊢ ((M \in ∞Met (X) \land Y \in X \land R \in ℝ) \land Y ball (M) R \neq \emptyset) \to R \in ℝ$
16		xbln0	$⊢ (M \in ∞Met (X) \land Y \in X \land R \in ℝ^{*}) \to (Y ball (M) R \neq \emptyset \leftrightarrow 0 < R)$
17	2 16	syl3an3	$⊢ (M \in ∞Met (X) \land Y \in X \land R \in ℝ) \to (Y ball (M) R \neq \emptyset \leftrightarrow 0 < R)$
18	17	biimpa	$⊢ ((M \in ∞Met (X) \land Y \in X \land R \in ℝ) \land Y ball (M) R \neq \emptyset) \to 0 < R$
19	15 18	elrpd	$⊢ ((M \in ∞Met (X) \land Y \in X \land R \in ℝ) \land Y ball (M) R \neq \emptyset) \to R \in ℝ^{+}$
20		blcntr	$⊢ (M \in ∞Met (X) \land Y \in X \land R \in ℝ^{+}) \to Y \in (Y ball (M) R)$
21	13 14 19 20	syl3anc	$⊢ ((M \in ∞Met (X) \land Y \in X \land R \in ℝ) \land Y ball (M) R \neq \emptyset) \to Y \in (Y ball (M) R)$
22	14 21	elind	$⊢ ((M \in ∞Met (X) \land Y \in X \land R \in ℝ) \land Y ball (M) R \neq \emptyset) \to Y \in (X \cap (Y ball (M) R))$
23	15	rexrd	$⊢ ((M \in ∞Met (X) \land Y \in X \land R \in ℝ) \land Y ball (M) R \neq \emptyset) \to R \in ℝ^{*}$
24		eqid	$⊢ {M ↾}_{((Y ball (M) R) \times (Y ball (M) R))} = {M ↾}_{((Y ball (M) R) \times (Y ball (M) R))}$
25	24	blres	$⊢ (M \in ∞Met (X) \land Y \in (X \cap (Y ball (M) R)) \land R \in ℝ^{*}) \to Y ball ({M ↾}_{((Y ball (M) R) \times (Y ball (M) R))}) R = (Y ball (M) R) \cap (Y ball (M) R)$
26	13 22 23 25	syl3anc	$⊢ ((M \in ∞Met (X) \land Y \in X \land R \in ℝ) \land Y ball (M) R \neq \emptyset) \to Y ball ({M ↾}_{((Y ball (M) R) \times (Y ball (M) R))}) R = (Y ball (M) R) \cap (Y ball (M) R)$
27		inidm	$⊢ (Y ball (M) R) \cap (Y ball (M) R) = Y ball (M) R$
28	26 27	eqtr2di	$⊢ ((M \in ∞Met (X) \land Y \in X \land R \in ℝ) \land Y ball (M) R \neq \emptyset) \to Y ball (M) R = Y ball ({M ↾}_{((Y ball (M) R) \times (Y ball (M) R))}) R$
29		rspceov	$⊢ (Y \in (Y ball (M) R) \land R \in ℝ^{+} \land Y ball (M) R = Y ball ({M ↾}_{((Y ball (M) R) \times (Y ball (M) R))}) R) \to \exists x \in (Y ball (M) R) \exists r \in ℝ^{+} Y ball (M) R = x ball ({M ↾}_{((Y ball (M) R) \times (Y ball (M) R))}) r$
30	21 19 28 29	syl3anc	$⊢ ((M \in ∞Met (X) \land Y \in X \land R \in ℝ) \land Y ball (M) R \neq \emptyset) \to \exists x \in (Y ball (M) R) \exists r \in ℝ^{+} Y ball (M) R = x ball ({M ↾}_{((Y ball (M) R) \times (Y ball (M) R))}) r$
31		isbnd2	$⊢ ({M ↾}_{((Y ball (M) R) \times (Y ball (M) R))} \in Bnd (Y ball (M) R) \land Y ball (M) R \neq \emptyset) \leftrightarrow ({M ↾}_{((Y ball (M) R) \times (Y ball (M) R))} \in ∞Met (Y ball (M) R) \land \exists x \in (Y ball (M) R) \exists r \in ℝ^{+} Y ball (M) R = x ball ({M ↾}_{((Y ball (M) R) \times (Y ball (M) R))}) r)$
32	12 30 31	sylanbrc	$⊢ ((M \in ∞Met (X) \land Y \in X \land R \in ℝ) \land Y ball (M) R \neq \emptyset) \to ({M ↾}_{((Y ball (M) R) \times (Y ball (M) R))} \in Bnd (Y ball (M) R) \land Y ball (M) R \neq \emptyset)$
33	32	simpld	$⊢ ((M \in ∞Met (X) \land Y \in X \land R \in ℝ) \land Y ball (M) R \neq \emptyset) \to {M ↾}_{((Y ball (M) R) \times (Y ball (M) R))} \in Bnd (Y ball (M) R)$
34	11 33	pm2.61dane	$⊢ (M \in ∞Met (X) \land Y \in X \land R \in ℝ) \to {M ↾}_{((Y ball (M) R) \times (Y ball (M) R))} \in Bnd (Y ball (M) R)$

Metamath Proof Explorer

Theorem blbnd

Proof