Theorem blss

Description: Any point P in a ball B can be centered in another ball that is a subset of B . (Contributed by NM, 31-Aug-2006) (Revised by Mario Carneiro, 24-Aug-2015)

	Ref	Expression
Assertion	blss	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑃 ∈ 𝐵 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		blrn	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ↔ ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ* 𝐵 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
2		elbl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( 𝑃 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ↔ ( 𝑃 ∈ 𝑋 ∧ ( 𝑦 𝐷 𝑃 ) < 𝑟 ) ) )
3		simpl1	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
4		simpl2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
5		simpr	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) → 𝑃 ∈ 𝑋 )
6		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑦 𝐷 𝑃 ) ∈ ℝ* )
7	3 4 5 6	syl3anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑦 𝐷 𝑃 ) ∈ ℝ* )
8		simpl3	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) → 𝑟 ∈ ℝ* )
9		qbtwnxr	⊢ ( ( ( 𝑦 𝐷 𝑃 ) ∈ ℝ* ∧ 𝑟 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑃 ) < 𝑟 ) → ∃ 𝑧 ∈ ℚ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) )
10	9	3expia	⊢ ( ( ( 𝑦 𝐷 𝑃 ) ∈ ℝ* ∧ 𝑟 ∈ ℝ* ) → ( ( 𝑦 𝐷 𝑃 ) < 𝑟 → ∃ 𝑧 ∈ ℚ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) )
11	7 8 10	syl2anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑦 𝐷 𝑃 ) < 𝑟 → ∃ 𝑧 ∈ ℚ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) )
12		qre	⊢ ( 𝑧 ∈ ℚ → 𝑧 ∈ ℝ )
13		simpll1	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
14		simplr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝑃 ∈ 𝑋 )
15		simpll2	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝑦 ∈ 𝑋 )
16		xmetsym	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑃 ) )
17	13 14 15 16	syl3anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑃 ) )
18		simprrl	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑦 𝐷 𝑃 ) < 𝑧 )
19	17 18	eqbrtrd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 𝐷 𝑦 ) < 𝑧 )
20		simprl	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝑧 ∈ ℝ )
21		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑦 ) ∈ ℝ* )
22	13 14 15 21	syl3anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 𝐷 𝑦 ) ∈ ℝ* )
23		rexr	⊢ ( 𝑧 ∈ ℝ → 𝑧 ∈ ℝ* )
24	23	ad2antrl	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝑧 ∈ ℝ* )
25	22 24 19	xrltled	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 𝐷 𝑦 ) ≤ 𝑧 )
26		xmetlecl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑃 𝐷 𝑦 ) ≤ 𝑧 ) ) → ( 𝑃 𝐷 𝑦 ) ∈ ℝ )
27	13 14 15 20 25 26	syl122anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 𝐷 𝑦 ) ∈ ℝ )
28		difrp	⊢ ( ( ( 𝑃 𝐷 𝑦 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝑃 𝐷 𝑦 ) < 𝑧 ↔ ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ∈ ℝ+ ) )
29	27 20 28	syl2anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( ( 𝑃 𝐷 𝑦 ) < 𝑧 ↔ ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ∈ ℝ+ ) )
30	19 29	mpbid	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ∈ ℝ+ )
31	20 27	resubcld	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ∈ ℝ )
32	22	xrleidd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 𝐷 𝑦 ) ≤ ( 𝑃 𝐷 𝑦 ) )
33	20	recnd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝑧 ∈ ℂ )
34	27	recnd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 𝐷 𝑦 ) ∈ ℂ )
35	33 34	nncand	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑧 − ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) = ( 𝑃 𝐷 𝑦 ) )
36	32 35	breqtrrd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 𝐷 𝑦 ) ≤ ( 𝑧 − ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) )
37		blss2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ ( 𝑃 𝐷 𝑦 ) ≤ ( 𝑧 − ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) ) ) → ( 𝑃 ( ball ‘ 𝐷 ) ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑧 ) )
38	13 14 15 31 20 36 37	syl33anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 ( ball ‘ 𝐷 ) ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑧 ) )
39		simpll3	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝑟 ∈ ℝ* )
40		simprrr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝑧 < 𝑟 )
41	24 39 40	xrltled	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝑧 ≤ 𝑟 )
42		ssbl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ* ∧ 𝑟 ∈ ℝ* ) ∧ 𝑧 ≤ 𝑟 ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑧 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
43	13 15 24 39 41 42	syl221anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑧 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
44	38 43	sstrd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 ( ball ‘ 𝐷 ) ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
45		oveq2	⊢ ( 𝑥 = ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) = ( 𝑃 ( ball ‘ 𝐷 ) ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) )
46	45	sseq1d	⊢ ( 𝑥 = ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ↔ ( 𝑃 ( ball ‘ 𝐷 ) ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
47	46	rspcev	⊢ ( ( ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
48	30 44 47	syl2anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
49	48	expr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑧 ∈ ℝ ) → ( ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
50	12 49	sylan2	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑧 ∈ ℚ ) → ( ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
51	50	rexlimdva	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) → ( ∃ 𝑧 ∈ ℚ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
52	11 51	syld	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑦 𝐷 𝑃 ) < 𝑟 → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
53	52	expimpd	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( ( 𝑃 ∈ 𝑋 ∧ ( 𝑦 𝐷 𝑃 ) < 𝑟 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
54	2 53	sylbid	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( 𝑃 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
55		eleq2	⊢ ( 𝐵 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑃 ∈ 𝐵 ↔ 𝑃 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
56		sseq2	⊢ ( 𝐵 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 ↔ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
57	56	rexbidv	⊢ ( 𝐵 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ( ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 ↔ ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
58	55 57	imbi12d	⊢ ( 𝐵 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ( ( 𝑃 ∈ 𝐵 → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 ) ↔ ( 𝑃 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) ) )
59	54 58	syl5ibrcom	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( 𝐵 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑃 ∈ 𝐵 → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 ) ) )
60	59	3expib	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( 𝐵 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑃 ∈ 𝐵 → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 ) ) ) )
61	60	rexlimdvv	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ* 𝐵 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑃 ∈ 𝐵 → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 ) ) )
62	1 61	sylbid	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) → ( 𝑃 ∈ 𝐵 → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 ) ) )
63	62	3imp	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑃 ∈ 𝐵 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 )