This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isbnd2

Description: The predicate "is a bounded metric space". Uses a single point instead of an arbitrary point in the space. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion isbnd2 ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 ≠ ∅ ) ↔ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )

Proof

Step Hyp Ref Expression
1 isbndx ⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
2 1 anbi1i ⊢ ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 ≠ ∅ ) ↔ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) ∧ 𝑋 ≠ ∅ ) )
3 anass ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) ∧ 𝑋 ≠ ∅ ) ↔ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∧ 𝑋 ≠ ∅ ) ) )
4 r19.2z ⊢ ( ( 𝑋 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) )
5 4 ancoms ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∧ 𝑋 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) )
6 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) )
7 6 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ↔ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) )
8 oveq2 ⊢ ( 𝑟 = 𝑠 → ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) )
9 8 eqeq2d ⊢ ( 𝑟 = 𝑠 → ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ↔ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) ) )
10 7 9 cbvrex2vw ⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ↔ ∃ 𝑦 ∈ 𝑋 ∃ 𝑠 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) )
11 2rp ⊢ 2 ∈ ℝ+
12 rpmulcl ⊢ ( ( 2 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) → ( 2 · 𝑠 ) ∈ ℝ+ )
13 11 12 mpan ⊢ ( 𝑠 ∈ ℝ+ → ( 2 · 𝑠 ) ∈ ℝ+ )
14 13 ad2antll ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) → ( 2 · 𝑠 ) ∈ ℝ+ )
15 14 ad2antrr ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) ) → ( 2 · 𝑠 ) ∈ ℝ+ )
16 rpcn ⊢ ( 𝑠 ∈ ℝ+ → 𝑠 ∈ ℂ )
17 2cnd ⊢ ( 𝑠 ∈ ℝ+ → 2 ∈ ℂ )
18 2ne0 ⊢ 2 ≠ 0
19 18 a1i ⊢ ( 𝑠 ∈ ℝ+ → 2 ≠ 0 )
20 divcan3 ⊢ ( ( 𝑠 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · 𝑠 ) / 2 ) = 𝑠 )
21 20 eqcomd ⊢ ( ( 𝑠 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → 𝑠 = ( ( 2 · 𝑠 ) / 2 ) )
22 16 17 19 21 syl3anc ⊢ ( 𝑠 ∈ ℝ+ → 𝑠 = ( ( 2 · 𝑠 ) / 2 ) )
23 22 oveq2d ⊢ ( 𝑠 ∈ ℝ+ → ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) )
24 23 eqeq2d ⊢ ( 𝑠 ∈ ℝ+ → ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) ↔ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) )
25 24 biimpd ⊢ ( 𝑠 ∈ ℝ+ → ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) → 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) )
26 25 ad2antll ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) → ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) → 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) )
27 26 adantr ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) → 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) )
28 27 imp ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) ) → 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) )
29 simpr ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) → 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) )
30 eleq2 ⊢ ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) → ( 𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) )
31 30 biimpac ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) → 𝑥 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) )
32 2re ⊢ 2 ∈ ℝ
33 rpre ⊢ ( 𝑠 ∈ ℝ+ → 𝑠 ∈ ℝ )
34 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝑠 ∈ ℝ ) → ( 2 · 𝑠 ) ∈ ℝ )
35 32 33 34 sylancr ⊢ ( 𝑠 ∈ ℝ+ → ( 2 · 𝑠 ) ∈ ℝ )
36 blhalf ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( ( 2 · 𝑠 ) ∈ ℝ ∧ 𝑥 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) ) → ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) )
37 36 expr ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 2 · 𝑠 ) ∈ ℝ ) → ( 𝑥 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) → ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ) )
38 35 37 sylan2 ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑠 ∈ ℝ+ ) → ( 𝑥 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) → ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ) )
39 38 anasss ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) → ( 𝑥 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) → ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ) )
40 39 imp ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑥 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) → ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) )
41 31 40 sylan2 ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) ) → ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) )
42 41 anassrs ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) → ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) )
43 29 42 eqsstrd ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) → 𝑋 ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) )
44 28 43 syldan ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) ) → 𝑋 ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) )
45 13 adantl ⊢ ( ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) → ( 2 · 𝑠 ) ∈ ℝ+ )
46 rpxr ⊢ ( ( 2 · 𝑠 ) ∈ ℝ+ → ( 2 · 𝑠 ) ∈ ℝ* )
47 blssm ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ ( 2 · 𝑠 ) ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ⊆ 𝑋 )
48 46 47 syl3an3 ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ ( 2 · 𝑠 ) ∈ ℝ+ ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ⊆ 𝑋 )
49 48 3expa ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 2 · 𝑠 ) ∈ ℝ+ ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ⊆ 𝑋 )
50 45 49 sylan2 ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ⊆ 𝑋 )
51 50 an32s ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ⊆ 𝑋 )
52 51 adantr ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ⊆ 𝑋 )
53 44 52 eqssd ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) ) → 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) )
54 oveq2 ⊢ ( 𝑟 = ( 2 · 𝑠 ) → ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) )
55 54 rspceeqv ⊢ ( ( ( 2 · 𝑠 ) ∈ ℝ+ ∧ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ) → ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) )
56 15 53 55 syl2anc ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) ) → ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) )
57 56 ex ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) → ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
58 57 ralrimdva ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ+ ) ) → ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
59 58 rexlimdvva ⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → ( ∃ 𝑦 ∈ 𝑋 ∃ 𝑠 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
60 10 59 biimtrid ⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
61 rexn0 ⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → 𝑋 ≠ ∅ )
62 61 a1i ⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → 𝑋 ≠ ∅ ) )
63 60 62 jcad ⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∧ 𝑋 ≠ ∅ ) ) )
64 5 63 impbid2 ⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → ( ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∧ 𝑋 ≠ ∅ ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
65 64 pm5.32i ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∧ 𝑋 ≠ ∅ ) ) ↔ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
66 2 3 65 3bitri ⊢ ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 ≠ ∅ ) ↔ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )