xblss2ps - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > xblss2ps		GIF version

Theorem xblss2ps 14946

Description: One ball is contained in another if the center-to-center distance is less than the difference of the radii. In this version of blss2 14949 for extended metrics, we have to assume the balls are a finite distance apart, or else 𝑃 will not even be in the infinity ball around 𝑄. (Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)

**Hypotheses**
Ref	Expression
xblss2ps.1	⊢ (𝜑 → 𝐷 ∈ (PsMet‘𝑋))
xblss2ps.2	⊢ (𝜑 → 𝑃 ∈ 𝑋)
xblss2ps.3	⊢ (𝜑 → 𝑄 ∈ 𝑋)
xblss2ps.4	⊢ (𝜑 → 𝑅 ∈ ℝ^*)
xblss2ps.5	⊢ (𝜑 → 𝑆 ∈ ℝ^*)
xblss2ps.6	⊢ (𝜑 → (𝑃𝐷𝑄) ∈ ℝ)
xblss2ps.7	⊢ (𝜑 → (𝑃𝐷𝑄) ≤ (𝑆 +_𝑒 -_𝑒𝑅))

**Assertion**
Ref	Expression
xblss2ps	⊢ (𝜑 → (𝑃(ball‘𝐷)𝑅) ⊆ (𝑄(ball‘𝐷)𝑆))

Proof of Theorem xblss2ps Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		xblss2ps.1	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ (PsMet‘𝑋))
2		xblss2ps.2	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ 𝑋)
3		xblss2ps.4	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ ℝ^*)
4		elblps 14932	. . . . . 6 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ^*) → (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅)))
5	1, 2, 3, 4	syl3anc 1250	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅)))
6	5	simprbda 383	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → 𝑥 ∈ 𝑋)
7	1	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → 𝐷 ∈ (PsMet‘𝑋))
8		xblss2ps.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ 𝑋)
9	8	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → 𝑄 ∈ 𝑋)
10		psmetcl 14868	. . . . . . . 8 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑄 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑄𝐷𝑥) ∈ ℝ^*)
11	7, 9, 6, 10	syl3anc 1250	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → (𝑄𝐷𝑥) ∈ ℝ^*)
12	11	adantr 276	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 ∈ ℝ) → (𝑄𝐷𝑥) ∈ ℝ^*)
13		xblss2ps.6	. . . . . . . . . 10 ⊢ (𝜑 → (𝑃𝐷𝑄) ∈ ℝ)
14	13	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → (𝑃𝐷𝑄) ∈ ℝ)
15	14	rexrd 8137	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → (𝑃𝐷𝑄) ∈ ℝ^*)
16	3	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → 𝑅 ∈ ℝ^*)
17	15, 16	xaddcld 10021	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → ((𝑃𝐷𝑄) +_𝑒 𝑅) ∈ ℝ^*)
18	17	adantr 276	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 ∈ ℝ) → ((𝑃𝐷𝑄) +_𝑒 𝑅) ∈ ℝ^*)
19		xblss2ps.5	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ ℝ^*)
20	19	ad2antrr 488	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 ∈ ℝ) → 𝑆 ∈ ℝ^*)
21	2	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → 𝑃 ∈ 𝑋)
22		psmetcl 14868	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑃𝐷𝑥) ∈ ℝ^*)
23	7, 21, 6, 22	syl3anc 1250	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → (𝑃𝐷𝑥) ∈ ℝ^*)
24	15, 23	xaddcld 10021	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → ((𝑃𝐷𝑄) +_𝑒 (𝑃𝐷𝑥)) ∈ ℝ^*)
25		psmettri2 14870	. . . . . . . . 9 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝑄𝐷𝑥) ≤ ((𝑃𝐷𝑄) +_𝑒 (𝑃𝐷𝑥)))
26	7, 21, 9, 6, 25	syl13anc 1252	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → (𝑄𝐷𝑥) ≤ ((𝑃𝐷𝑄) +_𝑒 (𝑃𝐷𝑥)))
27	5	simplbda 384	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → (𝑃𝐷𝑥) < 𝑅)
28		xltadd2 10014	. . . . . . . . . 10 ⊢ (((𝑃𝐷𝑥) ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ∧ (𝑃𝐷𝑄) ∈ ℝ) → ((𝑃𝐷𝑥) < 𝑅 ↔ ((𝑃𝐷𝑄) +_𝑒 (𝑃𝐷𝑥)) < ((𝑃𝐷𝑄) +_𝑒 𝑅)))
29	23, 16, 14, 28	syl3anc 1250	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → ((𝑃𝐷𝑥) < 𝑅 ↔ ((𝑃𝐷𝑄) +_𝑒 (𝑃𝐷𝑥)) < ((𝑃𝐷𝑄) +_𝑒 𝑅)))
30	27, 29	mpbid 147	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → ((𝑃𝐷𝑄) +_𝑒 (𝑃𝐷𝑥)) < ((𝑃𝐷𝑄) +_𝑒 𝑅))
31	11, 24, 17, 26, 30	xrlelttrd 9947	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → (𝑄𝐷𝑥) < ((𝑃𝐷𝑄) +_𝑒 𝑅))
32	31	adantr 276	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 ∈ ℝ) → (𝑄𝐷𝑥) < ((𝑃𝐷𝑄) +_𝑒 𝑅))
33	19	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → 𝑆 ∈ ℝ^*)
34	16	xnegcld 9992	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → -_𝑒𝑅 ∈ ℝ^*)
35	33, 34	xaddcld 10021	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → (𝑆 +_𝑒 -_𝑒𝑅) ∈ ℝ^*)
36		xblss2ps.7	. . . . . . . . . 10 ⊢ (𝜑 → (𝑃𝐷𝑄) ≤ (𝑆 +_𝑒 -_𝑒𝑅))
37	36	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → (𝑃𝐷𝑄) ≤ (𝑆 +_𝑒 -_𝑒𝑅))
38		xleadd1a 10010	. . . . . . . . 9 ⊢ ((((𝑃𝐷𝑄) ∈ ℝ^* ∧ (𝑆 +_𝑒 -_𝑒𝑅) ∈ ℝ^* ∧ 𝑅 ∈ ℝ^*) ∧ (𝑃𝐷𝑄) ≤ (𝑆 +_𝑒 -_𝑒𝑅)) → ((𝑃𝐷𝑄) +_𝑒 𝑅) ≤ ((𝑆 +_𝑒 -_𝑒𝑅) +_𝑒 𝑅))
39	15, 35, 16, 37, 38	syl31anc 1253	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → ((𝑃𝐷𝑄) +_𝑒 𝑅) ≤ ((𝑆 +_𝑒 -_𝑒𝑅) +_𝑒 𝑅))
40	39	adantr 276	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 ∈ ℝ) → ((𝑃𝐷𝑄) +_𝑒 𝑅) ≤ ((𝑆 +_𝑒 -_𝑒𝑅) +_𝑒 𝑅))
41		xnpcan 10009	. . . . . . . 8 ⊢ ((𝑆 ∈ ℝ^* ∧ 𝑅 ∈ ℝ) → ((𝑆 +_𝑒 -_𝑒𝑅) +_𝑒 𝑅) = 𝑆)
42	33, 41	sylan 283	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 ∈ ℝ) → ((𝑆 +_𝑒 -_𝑒𝑅) +_𝑒 𝑅) = 𝑆)
43	40, 42	breqtrd 4076	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 ∈ ℝ) → ((𝑃𝐷𝑄) +_𝑒 𝑅) ≤ 𝑆)
44	12, 18, 20, 32, 43	xrltletrd 9948	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 ∈ ℝ) → (𝑄𝐷𝑥) < 𝑆)
45	11	adantr 276	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → (𝑄𝐷𝑥) ∈ ℝ^*)
46	13	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → (𝑃𝐷𝑄) ∈ ℝ)
47		simpll 527	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → 𝜑)
48		simplr 528	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → 𝑥 ∈ (𝑃(ball‘𝐷)𝑅))
49		simpr 110	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → 𝑅 = +∞)
50	49	oveq2d 5972	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → (𝑃(ball‘𝐷)𝑅) = (𝑃(ball‘𝐷)+∞))
51	48, 50	eleqtrd 2285	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → 𝑥 ∈ (𝑃(ball‘𝐷)+∞))
52		xblpnfps 14940	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑥 ∈ (𝑃(ball‘𝐷)+∞) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) ∈ ℝ)))
53	1, 2, 52	syl2anc 411	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑃(ball‘𝐷)+∞) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) ∈ ℝ)))
54	53	simplbda 384	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)+∞)) → (𝑃𝐷𝑥) ∈ ℝ)
55	47, 51, 54	syl2anc 411	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → (𝑃𝐷𝑥) ∈ ℝ)
56	46, 55	readdcld 8117	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → ((𝑃𝐷𝑄) + (𝑃𝐷𝑥)) ∈ ℝ)
57	56	rexrd 8137	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → ((𝑃𝐷𝑄) + (𝑃𝐷𝑥)) ∈ ℝ^*)
58		pnfxr 8140	. . . . . . . 8 ⊢ +∞ ∈ ℝ^*
59	58	a1i 9	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → +∞ ∈ ℝ^*)
60	1	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → 𝐷 ∈ (PsMet‘𝑋))
61	2	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → 𝑃 ∈ 𝑋)
62	8	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → 𝑄 ∈ 𝑋)
63	6	adantr 276	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → 𝑥 ∈ 𝑋)
64	60, 61, 62, 63, 25	syl13anc 1252	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → (𝑄𝐷𝑥) ≤ ((𝑃𝐷𝑄) +_𝑒 (𝑃𝐷𝑥)))
65	46, 55	rexaddd 9991	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → ((𝑃𝐷𝑄) +_𝑒 (𝑃𝐷𝑥)) = ((𝑃𝐷𝑄) + (𝑃𝐷𝑥)))
66	64, 65	breqtrd 4076	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → (𝑄𝐷𝑥) ≤ ((𝑃𝐷𝑄) + (𝑃𝐷𝑥)))
67		ltpnf 9917	. . . . . . . 8 ⊢ (((𝑃𝐷𝑄) + (𝑃𝐷𝑥)) ∈ ℝ → ((𝑃𝐷𝑄) + (𝑃𝐷𝑥)) < +∞)
68	56, 67	syl 14	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → ((𝑃𝐷𝑄) + (𝑃𝐷𝑥)) < +∞)
69	45, 57, 59, 66, 68	xrlelttrd 9947	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → (𝑄𝐷𝑥) < +∞)
70	19	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → 𝑆 ∈ ℝ^*)
71		xrpnfdc 9979	. . . . . . . 8 ⊢ (𝑆 ∈ ℝ^* → DECID 𝑆 = +∞)
72	70, 71	syl 14	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → DECID 𝑆 = +∞)
73		0xr 8134	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ^*
74	73	a1i 9	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → 0 ∈ ℝ^*)
75		psmetge0 14873	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) → 0 ≤ (𝑃𝐷𝑄))
76	7, 21, 9, 75	syl3anc 1250	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → 0 ≤ (𝑃𝐷𝑄))
77	74, 15, 35, 76, 37	xrletrd 9949	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → 0 ≤ (𝑆 +_𝑒 -_𝑒𝑅))
78		ge0nemnf 9961	. . . . . . . . 9 ⊢ (((𝑆 +_𝑒 -_𝑒𝑅) ∈ ℝ^* ∧ 0 ≤ (𝑆 +_𝑒 -_𝑒𝑅)) → (𝑆 +_𝑒 -_𝑒𝑅) ≠ -∞)
79	35, 77, 78	syl2anc 411	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → (𝑆 +_𝑒 -_𝑒𝑅) ≠ -∞)
80	79	adantr 276	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → (𝑆 +_𝑒 -_𝑒𝑅) ≠ -∞)
81		xaddmnf1 9985	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℝ^* ∧ 𝑆 ≠ +∞) → (𝑆 +_𝑒 -∞) = -∞)
82	81	ex 115	. . . . . . . . . . 11 ⊢ (𝑆 ∈ ℝ^* → (𝑆 ≠ +∞ → (𝑆 +_𝑒 -∞) = -∞))
83	70, 82	syl 14	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → (𝑆 ≠ +∞ → (𝑆 +_𝑒 -∞) = -∞))
84		xnegeq 9964	. . . . . . . . . . . . . 14 ⊢ (𝑅 = +∞ → -_𝑒𝑅 = -_𝑒+∞)
85	49, 84	syl 14	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → -_𝑒𝑅 = -_𝑒+∞)
86		xnegpnf 9965	. . . . . . . . . . . . 13 ⊢ -_𝑒+∞ = -∞
87	85, 86	eqtrdi 2255	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → -_𝑒𝑅 = -∞)
88	87	oveq2d 5972	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → (𝑆 +_𝑒 -_𝑒𝑅) = (𝑆 +_𝑒 -∞))
89	88	eqeq1d 2215	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → ((𝑆 +_𝑒 -_𝑒𝑅) = -∞ ↔ (𝑆 +_𝑒 -∞) = -∞))
90	83, 89	sylibrd 169	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → (𝑆 ≠ +∞ → (𝑆 +_𝑒 -_𝑒𝑅) = -∞))
91	90	a1d 22	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → (DECID 𝑆 = +∞ → (𝑆 ≠ +∞ → (𝑆 +_𝑒 -_𝑒𝑅) = -∞)))
92	91	necon1ddc 2455	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → (DECID 𝑆 = +∞ → ((𝑆 +_𝑒 -_𝑒𝑅) ≠ -∞ → 𝑆 = +∞)))
93	72, 80, 92	mp2d 47	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → 𝑆 = +∞)
94	69, 93	breqtrrd 4078	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) ∧ 𝑅 = +∞) → (𝑄𝐷𝑥) < 𝑆)
95		psmetge0 14873	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → 0 ≤ (𝑃𝐷𝑥))
96	7, 21, 6, 95	syl3anc 1250	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → 0 ≤ (𝑃𝐷𝑥))
97	74, 23, 16, 96, 27	xrlelttrd 9947	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → 0 < 𝑅)
98	74, 16, 97	xrltled 9936	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → 0 ≤ 𝑅)
99		ge0nemnf 9961	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ^* ∧ 0 ≤ 𝑅) → 𝑅 ≠ -∞)
100	16, 98, 99	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → 𝑅 ≠ -∞)
101	16, 100	jca 306	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → (𝑅 ∈ ℝ^* ∧ 𝑅 ≠ -∞))
102		xrnemnf 9914	. . . . . 6 ⊢ ((𝑅 ∈ ℝ^* ∧ 𝑅 ≠ -∞) ↔ (𝑅 ∈ ℝ ∨ 𝑅 = +∞))
103	101, 102	sylib 122	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → (𝑅 ∈ ℝ ∨ 𝑅 = +∞))
104	44, 94, 103	mpjaodan 800	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → (𝑄𝐷𝑥) < 𝑆)
105		elblps 14932	. . . . 5 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑄 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^*) → (𝑥 ∈ (𝑄(ball‘𝐷)𝑆) ↔ (𝑥 ∈ 𝑋 ∧ (𝑄𝐷𝑥) < 𝑆)))
106	7, 9, 33, 105	syl3anc 1250	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → (𝑥 ∈ (𝑄(ball‘𝐷)𝑆) ↔ (𝑥 ∈ 𝑋 ∧ (𝑄𝐷𝑥) < 𝑆)))
107	6, 104, 106	mpbir2and 947	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) → 𝑥 ∈ (𝑄(ball‘𝐷)𝑆))
108	107	ex 115	. 2 ⊢ (𝜑 → (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) → 𝑥 ∈ (𝑄(ball‘𝐷)𝑆)))
109	108	ssrdv 3203	1 ⊢ (𝜑 → (𝑃(ball‘𝐷)𝑅) ⊆ (𝑄(ball‘𝐷)𝑆))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 710 DECID wdc 836 = wceq 1373 ∈ wcel 2177 ≠ wne 2377 ⊆ wss 3170 class class class wbr 4050 ‘cfv 5279 (class class class)co 5956 ℝcr 7939 0cc0 7940 + caddc 7943 +∞cpnf 8119 -∞cmnf 8120 ℝ^*cxr 8121 < clt 8122 ≤ cle 8123 -_𝑒cxne 9906 +_𝑒 cxad 9907 PsMetcpsmet 14367 ballcbl 14370

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-sep 4169 ax-pow 4225 ax-pr 4260 ax-un 4487 ax-setind 4592 ax-cnex 8031 ax-resscn 8032 ax-1cn 8033 ax-1re 8034 ax-icn 8035 ax-addcl 8036 ax-addrcl 8037 ax-mulcl 8038 ax-mulrcl 8039 ax-addcom 8040 ax-mulcom 8041 ax-addass 8042 ax-mulass 8043 ax-distr 8044 ax-i2m1 8045 ax-0lt1 8046 ax-1rid 8047 ax-0id 8048 ax-rnegex 8049 ax-precex 8050 ax-cnre 8051 ax-pre-ltirr 8052 ax-pre-ltwlin 8053 ax-pre-lttrn 8054 ax-pre-apti 8055 ax-pre-ltadd 8056 ax-pre-mulgt0 8057

This theorem depends on definitions: df-bi 117 df-stab 833 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rab 2494 df-v 2775 df-sbc 3003 df-csb 3098 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-if 3576 df-pw 3622 df-sn 3643 df-pr 3644 df-op 3646 df-uni 3856 df-iun 3934 df-br 4051 df-opab 4113 df-mpt 4114 df-id 4347 df-po 4350 df-iso 4351 df-xp 4688 df-rel 4689 df-cnv 4690 df-co 4691 df-dm 4692 df-rn 4693 df-res 4694 df-ima 4695 df-iota 5240 df-fun 5281 df-fn 5282 df-f 5283 df-fv 5287 df-riota 5911 df-ov 5959 df-oprab 5960 df-mpo 5961 df-1st 6238 df-2nd 6239 df-map 6749 df-pnf 8124 df-mnf 8125 df-xr 8126 df-ltxr 8127 df-le 8128 df-sub 8260 df-neg 8261 df-2 9110 df-xneg 9909 df-xadd 9910 df-psmet 14375 df-bl 14378

This theorem is referenced by: blss2ps 14948 ssblps 14967

W3C validator