Metamath Proof Explorer

Theorem isbnd3

Description: A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 13-Sep-2015)

Ref Expression
Assertion isbnd3 ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∃ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 bndmet ⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) → 𝑀 ∈ ( Met ‘ 𝑋 ) )
2 0re ⊢ 0 ∈ ℝ
3 2 ne0ii ⊢ ℝ ≠ ∅
4 metf ⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
5 4 ffnd ⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → 𝑀 Fn ( 𝑋 × 𝑋 ) )
6 1 5 syl ⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) → 𝑀 Fn ( 𝑋 × 𝑋 ) )
7 6 ad2antrr ⊢ ( ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 = ∅ ) ∧ 𝑥 ∈ ℝ ) → 𝑀 Fn ( 𝑋 × 𝑋 ) )
8 1 4 syl ⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
9 8 fdmd ⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) → dom 𝑀 = ( 𝑋 × 𝑋 ) )
10 xpeq2 ⊢ ( 𝑋 = ∅ → ( 𝑋 × 𝑋 ) = ( 𝑋 × ∅ ) )
11 xp0 ⊢ ( 𝑋 × ∅ ) = ∅
12 10 11 eqtrdi ⊢ ( 𝑋 = ∅ → ( 𝑋 × 𝑋 ) = ∅ )
13 9 12 sylan9eq ⊢ ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 = ∅ ) → dom 𝑀 = ∅ )
14 13 adantr ⊢ ( ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 = ∅ ) ∧ 𝑥 ∈ ℝ ) → dom 𝑀 = ∅ )
15 dm0rn0 ⊢ ( dom 𝑀 = ∅ ↔ ran 𝑀 = ∅ )
16 14 15 sylib ⊢ ( ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 = ∅ ) ∧ 𝑥 ∈ ℝ ) → ran 𝑀 = ∅ )
17 0ss ⊢ ∅ ⊆ ( 0 [,] 𝑥 )
18 16 17 eqsstrdi ⊢ ( ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 = ∅ ) ∧ 𝑥 ∈ ℝ ) → ran 𝑀 ⊆ ( 0 [,] 𝑥 ) )
19 df-f ⊢ ( 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ↔ ( 𝑀 Fn ( 𝑋 × 𝑋 ) ∧ ran 𝑀 ⊆ ( 0 [,] 𝑥 ) ) )
20 7 18 19 sylanbrc ⊢ ( ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 = ∅ ) ∧ 𝑥 ∈ ℝ ) → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) )
21 20 ralrimiva ⊢ ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 = ∅ ) → ∀ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) )
22 r19.2z ⊢ ( ( ℝ ≠ ∅ ∧ ∀ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) → ∃ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) )
23 3 21 22 sylancr ⊢ ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 = ∅ ) → ∃ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) )
24 isbnd2 ⊢ ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 ≠ ∅ ) ↔ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) )
25 24 simprbi ⊢ ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) )
26 2re ⊢ 2 ∈ ℝ
27 simprlr ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) → 𝑟 ∈ ℝ+ )
28 27 rpred ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) → 𝑟 ∈ ℝ )
29 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( 2 · 𝑟 ) ∈ ℝ )
30 26 28 29 sylancr ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) → ( 2 · 𝑟 ) ∈ ℝ )
31 5 adantr ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) → 𝑀 Fn ( 𝑋 × 𝑋 ) )
32 simpll ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑀 ∈ ( Met ‘ 𝑋 ) )
33 simprl ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
34 simprr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑧 ∈ 𝑋 )
35 metcl ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑥 𝑀 𝑧 ) ∈ ℝ )
36 32 33 34 35 syl3anc ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝑀 𝑧 ) ∈ ℝ )
37 metge0 ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → 0 ≤ ( 𝑥 𝑀 𝑧 ) )
38 32 33 34 37 syl3anc ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 0 ≤ ( 𝑥 𝑀 𝑧 ) )
39 30 adantr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 2 · 𝑟 ) ∈ ℝ )
40 simprll ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) → 𝑦 ∈ 𝑋 )
41 40 adantr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
42 metcl ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 𝑀 𝑥 ) ∈ ℝ )
43 32 41 33 42 syl3anc ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 𝑀 𝑥 ) ∈ ℝ )
44 metcl ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 𝑀 𝑧 ) ∈ ℝ )
45 32 41 34 44 syl3anc ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 𝑀 𝑧 ) ∈ ℝ )
46 43 45 readdcld ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑦 𝑀 𝑥 ) + ( 𝑦 𝑀 𝑧 ) ) ∈ ℝ )
47 mettri2 ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝑀 𝑧 ) ≤ ( ( 𝑦 𝑀 𝑥 ) + ( 𝑦 𝑀 𝑧 ) ) )
48 32 41 33 34 47 syl13anc ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝑀 𝑧 ) ≤ ( ( 𝑦 𝑀 𝑥 ) + ( 𝑦 𝑀 𝑧 ) ) )
49 28 adantr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑟 ∈ ℝ )
50 simplrr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) )
51 33 50 eleqtrd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑥 ∈ ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) )
52 metxmet ⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
53 32 52 syl ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
54 rpxr ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* )
55 54 ad2antlr ⊢ ( ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) → 𝑟 ∈ ℝ* )
56 55 ad2antlr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑟 ∈ ℝ* )
57 elbl2 ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ* ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑥 ∈ ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ↔ ( 𝑦 𝑀 𝑥 ) < 𝑟 ) )
58 53 56 41 33 57 syl22anc ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 ∈ ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ↔ ( 𝑦 𝑀 𝑥 ) < 𝑟 ) )
59 51 58 mpbid ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 𝑀 𝑥 ) < 𝑟 )
60 34 50 eleqtrd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑧 ∈ ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) )
61 elbl2 ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ* ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 ∈ ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ↔ ( 𝑦 𝑀 𝑧 ) < 𝑟 ) )
62 53 56 41 34 61 syl22anc ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 ∈ ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ↔ ( 𝑦 𝑀 𝑧 ) < 𝑟 ) )
63 60 62 mpbid ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 𝑀 𝑧 ) < 𝑟 )
64 43 45 49 49 59 63 lt2addd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑦 𝑀 𝑥 ) + ( 𝑦 𝑀 𝑧 ) ) < ( 𝑟 + 𝑟 ) )
65 49 recnd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑟 ∈ ℂ )
66 65 2timesd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 2 · 𝑟 ) = ( 𝑟 + 𝑟 ) )
67 64 66 breqtrrd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑦 𝑀 𝑥 ) + ( 𝑦 𝑀 𝑧 ) ) < ( 2 · 𝑟 ) )
68 36 46 39 48 67 lelttrd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝑀 𝑧 ) < ( 2 · 𝑟 ) )
69 36 39 68 ltled ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝑀 𝑧 ) ≤ ( 2 · 𝑟 ) )
70 elicc2 ⊢ ( ( 0 ∈ ℝ ∧ ( 2 · 𝑟 ) ∈ ℝ ) → ( ( 𝑥 𝑀 𝑧 ) ∈ ( 0 [,] ( 2 · 𝑟 ) ) ↔ ( ( 𝑥 𝑀 𝑧 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 𝑀 𝑧 ) ∧ ( 𝑥 𝑀 𝑧 ) ≤ ( 2 · 𝑟 ) ) ) )
71 2 39 70 sylancr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑥 𝑀 𝑧 ) ∈ ( 0 [,] ( 2 · 𝑟 ) ) ↔ ( ( 𝑥 𝑀 𝑧 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 𝑀 𝑧 ) ∧ ( 𝑥 𝑀 𝑧 ) ≤ ( 2 · 𝑟 ) ) ) )
72 36 38 69 71 mpbir3and ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝑀 𝑧 ) ∈ ( 0 [,] ( 2 · 𝑟 ) ) )
73 72 ralrimivva ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑀 𝑧 ) ∈ ( 0 [,] ( 2 · 𝑟 ) ) )
74 ffnov ⊢ ( 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] ( 2 · 𝑟 ) ) ↔ ( 𝑀 Fn ( 𝑋 × 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑀 𝑧 ) ∈ ( 0 [,] ( 2 · 𝑟 ) ) ) )
75 31 73 74 sylanbrc ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] ( 2 · 𝑟 ) ) )
76 oveq2 ⊢ ( 𝑥 = ( 2 · 𝑟 ) → ( 0 [,] 𝑥 ) = ( 0 [,] ( 2 · 𝑟 ) ) )
77 76 feq3d ⊢ ( 𝑥 = ( 2 · 𝑟 ) → ( 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ↔ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] ( 2 · 𝑟 ) ) ) )
78 77 rspcev ⊢ ( ( ( 2 · 𝑟 ) ∈ ℝ ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] ( 2 · 𝑟 ) ) ) → ∃ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) )
79 30 75 78 syl2anc ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ) → ∃ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) )
80 79 expr ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) → ∃ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) )
81 80 rexlimdvva ⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → ( ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) → ∃ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) )
82 1 81 syl ⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) → ( ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) → ∃ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) )
83 82 adantr ⊢ ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 ≠ ∅ ) → ( ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) → ∃ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) )
84 25 83 mpd ⊢ ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 ≠ ∅ ) → ∃ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) )
85 23 84 pm2.61dane ⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) → ∃ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) )
86 1 85 jca ⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) → ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∃ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) )
87 simpll ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) → 𝑀 ∈ ( Met ‘ 𝑋 ) )
88 simpllr ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → 𝑥 ∈ ℝ )
89 87 adantr ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → 𝑀 ∈ ( Met ‘ 𝑋 ) )
90 simpr ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
91 met0 ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 𝑀 𝑦 ) = 0 )
92 89 90 91 syl2anc ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 𝑀 𝑦 ) = 0 )
93 simplr ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) )
94 93 90 90 fovrnd ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 𝑀 𝑦 ) ∈ ( 0 [,] 𝑥 ) )
95 elicc2 ⊢ ( ( 0 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝑦 𝑀 𝑦 ) ∈ ( 0 [,] 𝑥 ) ↔ ( ( 𝑦 𝑀 𝑦 ) ∈ ℝ ∧ 0 ≤ ( 𝑦 𝑀 𝑦 ) ∧ ( 𝑦 𝑀 𝑦 ) ≤ 𝑥 ) ) )
96 2 88 95 sylancr ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑦 𝑀 𝑦 ) ∈ ( 0 [,] 𝑥 ) ↔ ( ( 𝑦 𝑀 𝑦 ) ∈ ℝ ∧ 0 ≤ ( 𝑦 𝑀 𝑦 ) ∧ ( 𝑦 𝑀 𝑦 ) ≤ 𝑥 ) ) )
97 94 96 mpbid ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑦 𝑀 𝑦 ) ∈ ℝ ∧ 0 ≤ ( 𝑦 𝑀 𝑦 ) ∧ ( 𝑦 𝑀 𝑦 ) ≤ 𝑥 ) )
98 97 simp3d ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 𝑀 𝑦 ) ≤ 𝑥 )
99 92 98 eqbrtrrd ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ 𝑥 )
100 88 99 ge0p1rpd ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 + 1 ) ∈ ℝ+ )
101 fovrn ⊢ ( ( 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 𝑀 𝑧 ) ∈ ( 0 [,] 𝑥 ) )
102 101 3expa ⊢ ( ( ( 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 𝑀 𝑧 ) ∈ ( 0 [,] 𝑥 ) )
103 102 adantlll ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 𝑀 𝑧 ) ∈ ( 0 [,] 𝑥 ) )
104 elicc2 ⊢ ( ( 0 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝑦 𝑀 𝑧 ) ∈ ( 0 [,] 𝑥 ) ↔ ( ( 𝑦 𝑀 𝑧 ) ∈ ℝ ∧ 0 ≤ ( 𝑦 𝑀 𝑧 ) ∧ ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 ) ) )
105 2 88 104 sylancr ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑦 𝑀 𝑧 ) ∈ ( 0 [,] 𝑥 ) ↔ ( ( 𝑦 𝑀 𝑧 ) ∈ ℝ ∧ 0 ≤ ( 𝑦 𝑀 𝑧 ) ∧ ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 ) ) )
106 105 adantr ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑦 𝑀 𝑧 ) ∈ ( 0 [,] 𝑥 ) ↔ ( ( 𝑦 𝑀 𝑧 ) ∈ ℝ ∧ 0 ≤ ( 𝑦 𝑀 𝑧 ) ∧ ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 ) ) )
107 103 106 mpbid ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑦 𝑀 𝑧 ) ∈ ℝ ∧ 0 ≤ ( 𝑦 𝑀 𝑧 ) ∧ ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 ) )
108 107 simp1d ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 𝑀 𝑧 ) ∈ ℝ )
109 88 adantr ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑥 ∈ ℝ )
110 peano2re ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ )
111 88 110 syl ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 + 1 ) ∈ ℝ )
112 111 adantr ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑥 + 1 ) ∈ ℝ )
113 107 simp3d ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 )
114 109 ltp1d ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑥 < ( 𝑥 + 1 ) )
115 108 109 112 113 114 lelttrd ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 𝑀 𝑧 ) < ( 𝑥 + 1 ) )
116 115 ralrimiva ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑀 𝑧 ) < ( 𝑥 + 1 ) )
117 rabid2 ⊢ ( 𝑋 = { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝑀 𝑧 ) < ( 𝑥 + 1 ) } ↔ ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑀 𝑧 ) < ( 𝑥 + 1 ) )
118 116 117 sylibr ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → 𝑋 = { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝑀 𝑧 ) < ( 𝑥 + 1 ) } )
119 89 52 syl ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
120 111 rexrd ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 + 1 ) ∈ ℝ* )
121 blval ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ ( 𝑥 + 1 ) ∈ ℝ* ) → ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑥 + 1 ) ) = { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝑀 𝑧 ) < ( 𝑥 + 1 ) } )
122 119 90 120 121 syl3anc ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑥 + 1 ) ) = { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝑀 𝑧 ) < ( 𝑥 + 1 ) } )
123 118 122 eqtr4d ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑥 + 1 ) ) )
124 oveq2 ⊢ ( 𝑟 = ( 𝑥 + 1 ) → ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) = ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑥 + 1 ) ) )
125 124 rspceeqv ⊢ ( ( ( 𝑥 + 1 ) ∈ ℝ+ ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑥 + 1 ) ) ) → ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) )
126 100 123 125 syl2anc ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ∧ 𝑦 ∈ 𝑋 ) → ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) )
127 126 ralrimiva ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) → ∀ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) )
128 isbnd ⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) )
129 87 127 128 sylanbrc ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) → 𝑀 ∈ ( Bnd ‘ 𝑋 ) )
130 129 r19.29an ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∃ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) → 𝑀 ∈ ( Bnd ‘ 𝑋 ) )
131 86 130 impbii ⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∃ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) )