xblss2ps

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 for extended metrics, we have to assume the balls are a finite distance apart, or else P will not even be in the infinity ball around Q . (Contributed by Mario Carneiro, 23-Aug-2015) (Revised by Thierry Arnoux, 11-Mar-2018)

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

Proof

Step	Hyp	Ref	Expression
1		xblss2ps.1	⊢ ( 𝜑 → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
2		xblss2ps.2	⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
3		xblss2ps.3	⊢ ( 𝜑 → 𝑄 ∈ 𝑋 )
4		xblss2ps.4	⊢ ( 𝜑 → 𝑅 ∈ ℝ^* )
5		xblss2ps.5	⊢ ( 𝜑 → 𝑆 ∈ ℝ^* )
6		xblss2ps.6	⊢ ( 𝜑 → ( 𝑃 𝐷 𝑄 ) ∈ ℝ )
7		xblss2ps.7	⊢ ( 𝜑 → ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 +_𝑒 -_𝑒 𝑅 ) )
8		elblps	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ^* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
9	1 2 4 8	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
10	9	simprbda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑥 ∈ 𝑋 )
11	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
12	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑄 ∈ 𝑋 )
13		psmetcl	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑄 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑄 𝐷 𝑥 ) ∈ ℝ^* )
14	11 12 10 13	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑄 𝐷 𝑥 ) ∈ ℝ^* )
15	14	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 ∈ ℝ ) → ( 𝑄 𝐷 𝑥 ) ∈ ℝ^* )
16	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ )
17	16	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ^* )
18	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑅 ∈ ℝ^* )
19	17 18	xaddcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( ( 𝑃 𝐷 𝑄 ) +_𝑒 𝑅 ) ∈ ℝ^* )
20	19	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 ∈ ℝ ) → ( ( 𝑃 𝐷 𝑄 ) +_𝑒 𝑅 ) ∈ ℝ^* )
21	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 ∈ ℝ ) → 𝑆 ∈ ℝ^* )
22	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑃 ∈ 𝑋 )
23		psmetcl	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ^* )
24	11 22 10 23	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ^* )
25	17 24	xaddcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( ( 𝑃 𝐷 𝑄 ) +_𝑒 ( 𝑃 𝐷 𝑥 ) ) ∈ ℝ^* )
26		psmettri2	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑄 𝐷 𝑥 ) ≤ ( ( 𝑃 𝐷 𝑄 ) +_𝑒 ( 𝑃 𝐷 𝑥 ) ) )
27	11 22 12 10 26	syl13anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑄 𝐷 𝑥 ) ≤ ( ( 𝑃 𝐷 𝑄 ) +_𝑒 ( 𝑃 𝐷 𝑥 ) ) )
28	9	simplbda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑃 𝐷 𝑥 ) < 𝑅 )
29		xltadd2	⊢ ( ( ( 𝑃 𝐷 𝑥 ) ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ∧ ( 𝑃 𝐷 𝑄 ) ∈ ℝ ) → ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ↔ ( ( 𝑃 𝐷 𝑄 ) +_𝑒 ( 𝑃 𝐷 𝑥 ) ) < ( ( 𝑃 𝐷 𝑄 ) +_𝑒 𝑅 ) ) )
30	24 18 16 29	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ↔ ( ( 𝑃 𝐷 𝑄 ) +_𝑒 ( 𝑃 𝐷 𝑥 ) ) < ( ( 𝑃 𝐷 𝑄 ) +_𝑒 𝑅 ) ) )
31	28 30	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( ( 𝑃 𝐷 𝑄 ) +_𝑒 ( 𝑃 𝐷 𝑥 ) ) < ( ( 𝑃 𝐷 𝑄 ) +_𝑒 𝑅 ) )
32	14 25 19 27 31	xrlelttrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑄 𝐷 𝑥 ) < ( ( 𝑃 𝐷 𝑄 ) +_𝑒 𝑅 ) )
33	32	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 ∈ ℝ ) → ( 𝑄 𝐷 𝑥 ) < ( ( 𝑃 𝐷 𝑄 ) +_𝑒 𝑅 ) )
34	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑆 ∈ ℝ^* )
35	18	xnegcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → -_𝑒 𝑅 ∈ ℝ^* )
36	34 35	xaddcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑆 +_𝑒 -_𝑒 𝑅 ) ∈ ℝ^* )
37	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 +_𝑒 -_𝑒 𝑅 ) )
38		xleadd1a	⊢ ( ( ( ( 𝑃 𝐷 𝑄 ) ∈ ℝ^* ∧ ( 𝑆 +_𝑒 -_𝑒 𝑅 ) ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ) ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 +_𝑒 -_𝑒 𝑅 ) ) → ( ( 𝑃 𝐷 𝑄 ) +_𝑒 𝑅 ) ≤ ( ( 𝑆 +_𝑒 -_𝑒 𝑅 ) +_𝑒 𝑅 ) )
39	17 36 18 37 38	syl31anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( ( 𝑃 𝐷 𝑄 ) +_𝑒 𝑅 ) ≤ ( ( 𝑆 +_𝑒 -_𝑒 𝑅 ) +_𝑒 𝑅 ) )
40	39	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 ∈ ℝ ) → ( ( 𝑃 𝐷 𝑄 ) +_𝑒 𝑅 ) ≤ ( ( 𝑆 +_𝑒 -_𝑒 𝑅 ) +_𝑒 𝑅 ) )
41		xnpcan	⊢ ( ( 𝑆 ∈ ℝ^* ∧ 𝑅 ∈ ℝ ) → ( ( 𝑆 +_𝑒 -_𝑒 𝑅 ) +_𝑒 𝑅 ) = 𝑆 )
42	34 41	sylan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 ∈ ℝ ) → ( ( 𝑆 +_𝑒 -_𝑒 𝑅 ) +_𝑒 𝑅 ) = 𝑆 )
43	40 42	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 ∈ ℝ ) → ( ( 𝑃 𝐷 𝑄 ) +_𝑒 𝑅 ) ≤ 𝑆 )
44	15 20 21 33 43	xrltletrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 ∈ ℝ ) → ( 𝑄 𝐷 𝑥 ) < 𝑆 )
45	14	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑄 𝐷 𝑥 ) ∈ ℝ^* )
46	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ )
47		simpll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝜑 )
48		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) )
49		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑅 = +∞ )
50	49	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) = ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) )
51	48 50	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) )
52		xblpnfps	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
53	1 2 52	syl2anc	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
54	53	simplbda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ )
55	47 51 54	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ )
56	46 55	readdcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( ( 𝑃 𝐷 𝑄 ) + ( 𝑃 𝐷 𝑥 ) ) ∈ ℝ )
57	56	rexrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( ( 𝑃 𝐷 𝑄 ) + ( 𝑃 𝐷 𝑥 ) ) ∈ ℝ^* )
58		pnfxr	⊢ +∞ ∈ ℝ^*
59	58	a1i	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → +∞ ∈ ℝ^* )
60	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
61	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑃 ∈ 𝑋 )
62	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑄 ∈ 𝑋 )
63	10	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑥 ∈ 𝑋 )
64	60 61 62 63 26	syl13anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑄 𝐷 𝑥 ) ≤ ( ( 𝑃 𝐷 𝑄 ) +_𝑒 ( 𝑃 𝐷 𝑥 ) ) )
65	46 55	rexaddd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( ( 𝑃 𝐷 𝑄 ) +_𝑒 ( 𝑃 𝐷 𝑥 ) ) = ( ( 𝑃 𝐷 𝑄 ) + ( 𝑃 𝐷 𝑥 ) ) )
66	64 65	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑄 𝐷 𝑥 ) ≤ ( ( 𝑃 𝐷 𝑄 ) + ( 𝑃 𝐷 𝑥 ) ) )
67	56	ltpnfd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( ( 𝑃 𝐷 𝑄 ) + ( 𝑃 𝐷 𝑥 ) ) < +∞ )
68	45 57 59 66 67	xrlelttrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑄 𝐷 𝑥 ) < +∞ )
69		0xr	⊢ 0 ∈ ℝ^*
70	69	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ∈ ℝ^* )
71		psmetge0	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → 0 ≤ ( 𝑃 𝐷 𝑄 ) )
72	11 22 12 71	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ≤ ( 𝑃 𝐷 𝑄 ) )
73	70 17 36 72 37	xrletrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ≤ ( 𝑆 +_𝑒 -_𝑒 𝑅 ) )
74		ge0nemnf	⊢ ( ( ( 𝑆 +_𝑒 -_𝑒 𝑅 ) ∈ ℝ^* ∧ 0 ≤ ( 𝑆 +_𝑒 -_𝑒 𝑅 ) ) → ( 𝑆 +_𝑒 -_𝑒 𝑅 ) ≠ -∞ )
75	36 73 74	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑆 +_𝑒 -_𝑒 𝑅 ) ≠ -∞ )
76	75	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑆 +_𝑒 -_𝑒 𝑅 ) ≠ -∞ )
77	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑆 ∈ ℝ^* )
78		xaddmnf1	⊢ ( ( 𝑆 ∈ ℝ^* ∧ 𝑆 ≠ +∞ ) → ( 𝑆 +_𝑒 -∞ ) = -∞ )
79	78	ex	⊢ ( 𝑆 ∈ ℝ^* → ( 𝑆 ≠ +∞ → ( 𝑆 +_𝑒 -∞ ) = -∞ ) )
80	77 79	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑆 ≠ +∞ → ( 𝑆 +_𝑒 -∞ ) = -∞ ) )
81		xnegeq	⊢ ( 𝑅 = +∞ → -_𝑒 𝑅 = -_𝑒 +∞ )
82	49 81	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → -_𝑒 𝑅 = -_𝑒 +∞ )
83		xnegpnf	⊢ -_𝑒 +∞ = -∞
84	82 83	eqtrdi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → -_𝑒 𝑅 = -∞ )
85	84	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑆 +_𝑒 -_𝑒 𝑅 ) = ( 𝑆 +_𝑒 -∞ ) )
86	85	eqeq1d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( ( 𝑆 +_𝑒 -_𝑒 𝑅 ) = -∞ ↔ ( 𝑆 +_𝑒 -∞ ) = -∞ ) )
87	80 86	sylibrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑆 ≠ +∞ → ( 𝑆 +_𝑒 -_𝑒 𝑅 ) = -∞ ) )
88	87	necon1d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( ( 𝑆 +_𝑒 -_𝑒 𝑅 ) ≠ -∞ → 𝑆 = +∞ ) )
89	76 88	mpd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑆 = +∞ )
90	68 89	breqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑄 𝐷 𝑥 ) < 𝑆 )
91		psmetge0	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( 𝑃 𝐷 𝑥 ) )
92	11 22 10 91	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ≤ ( 𝑃 𝐷 𝑥 ) )
93	70 24 18 92 28	xrlelttrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 < 𝑅 )
94	70 18 93	xrltled	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ≤ 𝑅 )
95		ge0nemnf	⊢ ( ( 𝑅 ∈ ℝ^* ∧ 0 ≤ 𝑅 ) → 𝑅 ≠ -∞ )
96	18 94 95	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑅 ≠ -∞ )
97	18 96	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑅 ∈ ℝ^* ∧ 𝑅 ≠ -∞ ) )
98		xrnemnf	⊢ ( ( 𝑅 ∈ ℝ^* ∧ 𝑅 ≠ -∞ ) ↔ ( 𝑅 ∈ ℝ ∨ 𝑅 = +∞ ) )
99	97 98	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑅 ∈ ℝ ∨ 𝑅 = +∞ ) )
100	44 90 99	mpjaodan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑄 𝐷 𝑥 ) < 𝑆 )
101		elblps	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑄 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ) → ( 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) )
102	11 12 34 101	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) )
103	10 100 102	mpbir2and	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) )
104	103	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) → 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) )
105	104	ssrdv	⊢ ( 𝜑 → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) )

Metamath Proof Explorer

Theorem xblss2ps

Proof