Metamath Proof Explorer

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 df-ss ⊒ ( ( π‘Œ Γ— π‘Œ ) βŠ† 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 β€˜ 𝑀 ) 𝑑 ) ) )