blssex

Description: Two ways to express the existence of a ball subset. (Contributed by NM, 5-May-2007) (Revised by Mario Carneiro, 12-Nov-2013)

		Ref	Expression
	Assertion	blssex	$⊢ (D \in ∞Met (X) \land P \in X) \to (\exists x \in ran ball (D) (P \in x \land x \subseteq A) \leftrightarrow \exists r \in ℝ^{+} P ball (D) r \subseteq A)$

Proof

Step	Hyp	Ref	Expression
1		blss	$⊢ (D \in ∞Met (X) \land x \in ran ball (D) \land P \in x) \to \exists r \in ℝ^{+} P ball (D) r \subseteq x$
2		sstr	$⊢ (P ball (D) r \subseteq x \land x \subseteq A) \to P ball (D) r \subseteq A$
3	2	expcom	$⊢ x \subseteq A \to (P ball (D) r \subseteq x \to P ball (D) r \subseteq A)$
4	3	reximdv	$⊢ x \subseteq A \to (\exists r \in ℝ^{+} P ball (D) r \subseteq x \to \exists r \in ℝ^{+} P ball (D) r \subseteq A)$
5	1 4	syl5com	$⊢ (D \in ∞Met (X) \land x \in ran ball (D) \land P \in x) \to (x \subseteq A \to \exists r \in ℝ^{+} P ball (D) r \subseteq A)$
6	5	3expa	$⊢ ((D \in ∞Met (X) \land x \in ran ball (D)) \land P \in x) \to (x \subseteq A \to \exists r \in ℝ^{+} P ball (D) r \subseteq A)$
7	6	expimpd	$⊢ (D \in ∞Met (X) \land x \in ran ball (D)) \to ((P \in x \land x \subseteq A) \to \exists r \in ℝ^{+} P ball (D) r \subseteq A)$
8	7	adantlr	$⊢ ((D \in ∞Met (X) \land P \in X) \land x \in ran ball (D)) \to ((P \in x \land x \subseteq A) \to \exists r \in ℝ^{+} P ball (D) r \subseteq A)$
9	8	rexlimdva	$⊢ (D \in ∞Met (X) \land P \in X) \to (\exists x \in ran ball (D) (P \in x \land x \subseteq A) \to \exists r \in ℝ^{+} P ball (D) r \subseteq A)$
10		simpll	$⊢ ((D \in ∞Met (X) \land P \in X) \land (r \in ℝ^{+} \land P ball (D) r \subseteq A)) \to D \in ∞Met (X)$
11		simplr	$⊢ ((D \in ∞Met (X) \land P \in X) \land (r \in ℝ^{+} \land P ball (D) r \subseteq A)) \to P \in X$
12		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
13	12	ad2antrl	$⊢ ((D \in ∞Met (X) \land P \in X) \land (r \in ℝ^{+} \land P ball (D) r \subseteq A)) \to r \in ℝ^{*}$
14		blelrn	$⊢ (D \in ∞Met (X) \land P \in X \land r \in ℝ^{*}) \to P ball (D) r \in ran ball (D)$
15	10 11 13 14	syl3anc	$⊢ ((D \in ∞Met (X) \land P \in X) \land (r \in ℝ^{+} \land P ball (D) r \subseteq A)) \to P ball (D) r \in ran ball (D)$
16		simprl	$⊢ ((D \in ∞Met (X) \land P \in X) \land (r \in ℝ^{+} \land P ball (D) r \subseteq A)) \to r \in ℝ^{+}$
17		blcntr	$⊢ (D \in ∞Met (X) \land P \in X \land r \in ℝ^{+}) \to P \in (P ball (D) r)$
18	10 11 16 17	syl3anc	$⊢ ((D \in ∞Met (X) \land P \in X) \land (r \in ℝ^{+} \land P ball (D) r \subseteq A)) \to P \in (P ball (D) r)$
19		simprr	$⊢ ((D \in ∞Met (X) \land P \in X) \land (r \in ℝ^{+} \land P ball (D) r \subseteq A)) \to P ball (D) r \subseteq A$
20		eleq2	$⊢ x = P ball (D) r \to (P \in x \leftrightarrow P \in (P ball (D) r))$
21		sseq1	$⊢ x = P ball (D) r \to (x \subseteq A \leftrightarrow P ball (D) r \subseteq A)$
22	20 21	anbi12d	$⊢ x = P ball (D) r \to ((P \in x \land x \subseteq A) \leftrightarrow (P \in (P ball (D) r) \land P ball (D) r \subseteq A))$
23	22	rspcev	$⊢ (P ball (D) r \in ran ball (D) \land (P \in (P ball (D) r) \land P ball (D) r \subseteq A)) \to \exists x \in ran ball (D) (P \in x \land x \subseteq A)$
24	15 18 19 23	syl12anc	$⊢ ((D \in ∞Met (X) \land P \in X) \land (r \in ℝ^{+} \land P ball (D) r \subseteq A)) \to \exists x \in ran ball (D) (P \in x \land x \subseteq A)$
25	24	rexlimdvaa	$⊢ (D \in ∞Met (X) \land P \in X) \to (\exists r \in ℝ^{+} P ball (D) r \subseteq A \to \exists x \in ran ball (D) (P \in x \land x \subseteq A))$
26	9 25	impbid	$⊢ (D \in ∞Met (X) \land P \in X) \to (\exists x \in ran ball (D) (P \in x \land x \subseteq A) \leftrightarrow \exists r \in ℝ^{+} P ball (D) r \subseteq A)$

Metamath Proof Explorer

Theorem blssex

Proof