Theorem ssbnd

Description: A subset of a metric space is bounded iff it is contained in a ball around P , for any P in the larger space. (Contributed by Mario Carneiro, 14-Sep-2015)

	Ref	Expression
Hypothesis	ssbnd.2	⊢ 𝑁 = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) )
Assertion	ssbnd	⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑁 ∈ ( Bnd ‘ 𝑌 ) ↔ ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssbnd.2	⊢ 𝑁 = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) )
2		0re	⊢ 0 ∈ ℝ
3	2	ne0ii	⊢ ℝ ≠ ∅
4		0ss	⊢ ∅ ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 )
5		sseq1	⊢ ( 𝑌 = ∅ → ( 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∅ ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
6	4 5	mpbiri	⊢ ( 𝑌 = ∅ → 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) )
7	6	ralrimivw	⊢ ( 𝑌 = ∅ → ∀ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) )
8		r19.2z	⊢ ( ( ℝ ≠ ∅ ∧ ∀ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) )
9	3 7 8	sylancr	⊢ ( 𝑌 = ∅ → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) )
10	9	a1i	⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( Bnd ‘ 𝑌 ) ) → ( 𝑌 = ∅ → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
11		isbnd2	⊢ ( ( 𝑁 ∈ ( Bnd ‘ 𝑌 ) ∧ 𝑌 ≠ ∅ ) ↔ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ ∃ 𝑦 ∈ 𝑌 ∃ 𝑟 ∈ ℝ+ 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ) )
12		simplll	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑀 ∈ ( Met ‘ 𝑋 ) )
13	1	dmeqi	⊢ dom 𝑁 = dom ( 𝑀 ↾ ( 𝑌 × 𝑌 ) )
14		dmres	⊢ dom ( 𝑀 ↾ ( 𝑌 × 𝑌 ) ) = ( ( 𝑌 × 𝑌 ) ∩ dom 𝑀 )
15	13 14	eqtri	⊢ dom 𝑁 = ( ( 𝑌 × 𝑌 ) ∩ dom 𝑀 )
16		xmetf	⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → 𝑁 : ( 𝑌 × 𝑌 ) ⟶ ℝ* )
17	16	fdmd	⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → dom 𝑁 = ( 𝑌 × 𝑌 ) )
18	15 17	eqtr3id	⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → ( ( 𝑌 × 𝑌 ) ∩ dom 𝑀 ) = ( 𝑌 × 𝑌 ) )
19		dfss2	⊢ ( ( 𝑌 × 𝑌 ) ⊆ dom 𝑀 ↔ ( ( 𝑌 × 𝑌 ) ∩ dom 𝑀 ) = ( 𝑌 × 𝑌 ) )
20	18 19	sylibr	⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → ( 𝑌 × 𝑌 ) ⊆ dom 𝑀 )
21	20	ad2antlr	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑌 × 𝑌 ) ⊆ dom 𝑀 )
22		metf	⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
23	22	fdmd	⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → dom 𝑀 = ( 𝑋 × 𝑋 ) )
24	23	ad3antrrr	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → dom 𝑀 = ( 𝑋 × 𝑋 ) )
25	21 24	sseqtrd	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑌 × 𝑌 ) ⊆ ( 𝑋 × 𝑋 ) )
26		dmss	⊢ ( ( 𝑌 × 𝑌 ) ⊆ ( 𝑋 × 𝑋 ) → dom ( 𝑌 × 𝑌 ) ⊆ dom ( 𝑋 × 𝑋 ) )
27	25 26	syl	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → dom ( 𝑌 × 𝑌 ) ⊆ dom ( 𝑋 × 𝑋 ) )
28		dmxpid	⊢ dom ( 𝑌 × 𝑌 ) = 𝑌
29		dmxpid	⊢ dom ( 𝑋 × 𝑋 ) = 𝑋
30	27 28 29	3sstr3g	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑌 ⊆ 𝑋 )
31		simprl	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑦 ∈ 𝑌 )
32	30 31	sseldd	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑦 ∈ 𝑋 )
33		simpllr	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑃 ∈ 𝑋 )
34		metcl	⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑦 𝑀 𝑃 ) ∈ ℝ )
35	12 32 33 34	syl3anc	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑦 𝑀 𝑃 ) ∈ ℝ )
36		rpre	⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ )
37	36	ad2antll	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℝ )
38	35 37	readdcld	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ∈ ℝ )
39		metxmet	⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
40	12 39	syl	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
41	32 31	elind	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑦 ∈ ( 𝑋 ∩ 𝑌 ) )
42		rpxr	⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* )
43	42	ad2antll	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℝ* )
44	1	blres	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ∩ 𝑌 ) ∧ 𝑟 ∈ ℝ* ) → ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) = ( ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ∩ 𝑌 ) )
45	40 41 43 44	syl3anc	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) = ( ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ∩ 𝑌 ) )
46		inss1	⊢ ( ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ∩ 𝑌 ) ⊆ ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 )
47	35	leidd	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑦 𝑀 𝑃 ) ≤ ( 𝑦 𝑀 𝑃 ) )
48	35	recnd	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑦 𝑀 𝑃 ) ∈ ℂ )
49	37	recnd	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℂ )
50	48 49	pncand	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → ( ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) − 𝑟 ) = ( 𝑦 𝑀 𝑃 ) )
51	47 50	breqtrrd	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑦 𝑀 𝑃 ) ≤ ( ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) − 𝑟 ) )
52		blss2	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ ∧ ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ∈ ℝ ∧ ( 𝑦 𝑀 𝑃 ) ≤ ( ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) − 𝑟 ) ) ) → ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ) )
53	40 32 33 37 38 51 52	syl33anc	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ) )
54	46 53	sstrid	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → ( ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ∩ 𝑌 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ) )
55	45 54	eqsstrd	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ) )
56		oveq2	⊢ ( 𝑑 = ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) → ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) = ( 𝑃 ( ball ‘ 𝑀 ) ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ) )
57	56	sseq2d	⊢ ( 𝑑 = ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) → ( ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ) ) )
58	57	rspcev	⊢ ( ( ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ∈ ℝ ∧ ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ) ) → ∃ 𝑑 ∈ ℝ ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) )
59	38 55 58	syl2anc	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → ∃ 𝑑 ∈ ℝ ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) )
60		sseq1	⊢ ( 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) → ( 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
61	60	rexbidv	⊢ ( 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) → ( ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∃ 𝑑 ∈ ℝ ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
62	59 61	syl5ibrcom	⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
63	62	rexlimdvva	⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( ∃ 𝑦 ∈ 𝑌 ∃ 𝑟 ∈ ℝ+ 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
64	63	expimpd	⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ ∃ 𝑦 ∈ 𝑌 ∃ 𝑟 ∈ ℝ+ 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ) → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
65	11 64	biimtrid	⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑁 ∈ ( Bnd ‘ 𝑌 ) ∧ 𝑌 ≠ ∅ ) → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
66	65	expdimp	⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( Bnd ‘ 𝑌 ) ) → ( 𝑌 ≠ ∅ → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
67	10 66	pm2.61dne	⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( Bnd ‘ 𝑌 ) ) → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) )
68	67	ex	⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑁 ∈ ( Bnd ‘ 𝑌 ) → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
69		simprr	⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) )
70		xpss12	⊢ ( ( 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) → ( 𝑌 × 𝑌 ) ⊆ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
71	69 69 70	syl2anc	⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ( 𝑌 × 𝑌 ) ⊆ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
72	71	resabs1d	⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ( ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ↾ ( 𝑌 × 𝑌 ) ) = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) ) )
73	72 1	eqtr4di	⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ( ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ↾ ( 𝑌 × 𝑌 ) ) = 𝑁 )
74		blbnd	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑑 ∈ ℝ ) → ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ∈ ( Bnd ‘ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
75	39 74	syl3an1	⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑑 ∈ ℝ ) → ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ∈ ( Bnd ‘ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
76	75	3expa	⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑑 ∈ ℝ ) → ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ∈ ( Bnd ‘ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
77	76	adantrr	⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ∈ ( Bnd ‘ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
78		bndss	⊢ ( ( ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ∈ ( Bnd ‘ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) → ( ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Bnd ‘ 𝑌 ) )
79	77 69 78	syl2anc	⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ( ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Bnd ‘ 𝑌 ) )
80	73 79	eqeltrrd	⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → 𝑁 ∈ ( Bnd ‘ 𝑌 ) )
81	80	rexlimdvaa	⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) → 𝑁 ∈ ( Bnd ‘ 𝑌 ) ) )
82	68 81	impbid	⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑁 ∈ ( Bnd ‘ 𝑌 ) ↔ ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )