blin2

Description: Given any two balls and a point in their intersection, there is a ball contained in the intersection with the given center point. (Contributed by Mario Carneiro, 12-Nov-2013)

		Ref	Expression
	Assertion	blin2	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to \exists x \in ℝ^{+} P ball (D) x \subseteq B \cap C$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to D \in ∞Met (X)$
2		simprl	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to B \in ran ball (D)$
3		simplr	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to P \in (B \cap C)$
4	3	elin1d	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to P \in B$
5		blss	$⊢ (D \in ∞Met (X) \land B \in ran ball (D) \land P \in B) \to \exists y \in ℝ^{+} P ball (D) y \subseteq B$
6	1 2 4 5	syl3anc	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to \exists y \in ℝ^{+} P ball (D) y \subseteq B$
7		simprr	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to C \in ran ball (D)$
8	3	elin2d	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to P \in C$
9		blss	$⊢ (D \in ∞Met (X) \land C \in ran ball (D) \land P \in C) \to \exists z \in ℝ^{+} P ball (D) z \subseteq C$
10	1 7 8 9	syl3anc	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to \exists z \in ℝ^{+} P ball (D) z \subseteq C$
11		reeanv	$⊢ \exists y \in ℝ^{+} \exists z \in ℝ^{+} (P ball (D) y \subseteq B \land P ball (D) z \subseteq C) \leftrightarrow (\exists y \in ℝ^{+} P ball (D) y \subseteq B \land \exists z \in ℝ^{+} P ball (D) z \subseteq C)$
12		ss2in	$⊢ (P ball (D) y \subseteq B \land P ball (D) z \subseteq C) \to (P ball (D) y) \cap (P ball (D) z) \subseteq B \cap C$
13		inss1	$⊢ B \cap C \subseteq B$
14		blf	$⊢ D \in ∞Met (X) \to ball (D) : X \times ℝ^{*} ⟶ 𝒫 X$
15		frn	$⊢ ball (D) : X \times ℝ^{*} ⟶ 𝒫 X \to ran ball (D) \subseteq 𝒫 X$
16	1 14 15	3syl	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to ran ball (D) \subseteq 𝒫 X$
17	16 2	sseldd	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to B \in 𝒫 X$
18	17	elpwid	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to B \subseteq X$
19	13 18	sstrid	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to B \cap C \subseteq X$
20	19 3	sseldd	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to P \in X$
21	1 20	jca	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to (D \in ∞Met (X) \land P \in X)$
22		rpxr	$⊢ y \in ℝ^{+} \to y \in ℝ^{*}$
23		rpxr	$⊢ z \in ℝ^{+} \to z \in ℝ^{*}$
24	22 23	anim12i	$⊢ (y \in ℝ^{+} \land z \in ℝ^{+}) \to (y \in ℝ^{} \land z \in ℝ^{})$
25		blin	$⊢ ((D \in ∞Met (X) \land P \in X) \land (y \in ℝ^{} \land z \in ℝ^{})) \to (P ball (D) y) \cap (P ball (D) z) = P ball (D) if (y \leq z, y, z)$
26	21 24 25	syl2an	$⊢ (((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to (P ball (D) y) \cap (P ball (D) z) = P ball (D) if (y \leq z, y, z)$
27	26	sseq1d	$⊢ (((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to ((P ball (D) y) \cap (P ball (D) z) \subseteq B \cap C \leftrightarrow P ball (D) if (y \leq z, y, z) \subseteq B \cap C)$
28		ifcl	$⊢ (y \in ℝ^{+} \land z \in ℝ^{+}) \to if (y \leq z, y, z) \in ℝ^{+}$
29		oveq2	$⊢ x = if (y \leq z, y, z) \to P ball (D) x = P ball (D) if (y \leq z, y, z)$
30	29	sseq1d	$⊢ x = if (y \leq z, y, z) \to (P ball (D) x \subseteq B \cap C \leftrightarrow P ball (D) if (y \leq z, y, z) \subseteq B \cap C)$
31	30	rspcev	$⊢ (if (y \leq z, y, z) \in ℝ^{+} \land P ball (D) if (y \leq z, y, z) \subseteq B \cap C) \to \exists x \in ℝ^{+} P ball (D) x \subseteq B \cap C$
32	31	ex	$⊢ if (y \leq z, y, z) \in ℝ^{+} \to (P ball (D) if (y \leq z, y, z) \subseteq B \cap C \to \exists x \in ℝ^{+} P ball (D) x \subseteq B \cap C)$
33	28 32	syl	$⊢ (y \in ℝ^{+} \land z \in ℝ^{+}) \to (P ball (D) if (y \leq z, y, z) \subseteq B \cap C \to \exists x \in ℝ^{+} P ball (D) x \subseteq B \cap C)$
34	33	adantl	$⊢ (((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to (P ball (D) if (y \leq z, y, z) \subseteq B \cap C \to \exists x \in ℝ^{+} P ball (D) x \subseteq B \cap C)$
35	27 34	sylbid	$⊢ (((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to ((P ball (D) y) \cap (P ball (D) z) \subseteq B \cap C \to \exists x \in ℝ^{+} P ball (D) x \subseteq B \cap C)$
36	12 35	syl5	$⊢ (((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to ((P ball (D) y \subseteq B \land P ball (D) z \subseteq C) \to \exists x \in ℝ^{+} P ball (D) x \subseteq B \cap C)$
37	36	rexlimdvva	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to (\exists y \in ℝ^{+} \exists z \in ℝ^{+} (P ball (D) y \subseteq B \land P ball (D) z \subseteq C) \to \exists x \in ℝ^{+} P ball (D) x \subseteq B \cap C)$
38	11 37	biimtrrid	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to ((\exists y \in ℝ^{+} P ball (D) y \subseteq B \land \exists z \in ℝ^{+} P ball (D) z \subseteq C) \to \exists x \in ℝ^{+} P ball (D) x \subseteq B \cap C)$
39	6 10 38	mp2and	$⊢ ((D \in ∞Met (X) \land P \in (B \cap C)) \land (B \in ran ball (D) \land C \in ran ball (D))) \to \exists x \in ℝ^{+} P ball (D) x \subseteq B \cap C$

Metamath Proof Explorer

Theorem blin2

Proof