Metamath Proof Explorer

Theorem totbndbnd

Description: A totally bounded metric space is bounded. This theorem fails for extended metrics - a bounded extended metric is a metric, but there are totally bounded extended metrics that are not metrics (if we were to weaken istotbnd to only require that M be an extended metric). A counterexample is the discrete extended metric (assigning distinct points distance +oo ) on a finite set. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion totbndbnd ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) → 𝑀 ∈ ( Bnd ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 totbndmet ⊢ ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) → 𝑀 ∈ ( Met ‘ 𝑋 ) )
2 1rp ⊢ 1 ∈ ℝ+
3 istotbnd3 ⊢ ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) )
4 3 simprbi ⊢ ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) → ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 )
5 oveq2 ⊢ ( 𝑑 = 1 → ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = ( 𝑥 ( ball ‘ 𝑀 ) 1 ) )
6 5 iuneq2d ⊢ ( 𝑑 = 1 → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) )
7 6 eqeq1d ⊢ ( 𝑑 = 1 → ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ↔ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) )
8 7 rexbidv ⊢ ( 𝑑 = 1 → ( ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ↔ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) )
9 8 rspcv ⊢ ( 1 ∈ ℝ+ → ( ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) )
10 2 4 9 mpsyl ⊢ ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 )
11 simplll ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → 𝑀 ∈ ( Met ‘ 𝑋 ) )
12 elfpw ⊢ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ↔ ( 𝑣 ⊆ 𝑋 ∧ 𝑣 ∈ Fin ) )
13 12 simplbi ⊢ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑣 ⊆ 𝑋 )
14 13 ad2antrl ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → 𝑣 ⊆ 𝑋 )
15 14 sselda ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → 𝑧 ∈ 𝑋 )
16 simpllr ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → 𝑦 ∈ 𝑋 )
17 metcl ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑧 𝑀 𝑦 ) ∈ ℝ )
18 11 15 16 17 syl3anc ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → ( 𝑧 𝑀 𝑦 ) ∈ ℝ )
19 metge0 ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ ( 𝑧 𝑀 𝑦 ) )
20 11 15 16 19 syl3anc ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → 0 ≤ ( 𝑧 𝑀 𝑦 ) )
21 18 20 ge0p1rpd ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → ( ( 𝑧 𝑀 𝑦 ) + 1 ) ∈ ℝ+ )
22 21 fmpttd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) : 𝑣 ⟶ ℝ+ )
23 22 frnd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ⊆ ℝ+ )
24 12 simprbi ⊢ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑣 ∈ Fin )
25 mptfi ⊢ ( 𝑣 ∈ Fin → ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ∈ Fin )
26 rnfi ⊢ ( ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ∈ Fin → ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ∈ Fin )
27 24 25 26 3syl ⊢ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) → ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ∈ Fin )
28 27 ad2antrl ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ∈ Fin )
29 simplr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → 𝑦 ∈ 𝑋 )
30 simprr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 )
31 29 30 eleqtrrd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → 𝑦 ∈ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) )
32 ne0i ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) ≠ ∅ )
33 dm0rn0 ⊢ ( dom ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) = ∅ ↔ ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) = ∅ )
34 ovex ⊢ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ∈ V
35 eqid ⊢ ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) = ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) )
36 34 35 dmmpti ⊢ dom ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) = 𝑣
37 36 eqeq1i ⊢ ( dom ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) = ∅ ↔ 𝑣 = ∅ )
38 iuneq1 ⊢ ( 𝑣 = ∅ → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = ∪ 𝑥 ∈ ∅ ( 𝑥 ( ball ‘ 𝑀 ) 1 ) )
39 37 38 sylbi ⊢ ( dom ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) = ∅ → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = ∪ 𝑥 ∈ ∅ ( 𝑥 ( ball ‘ 𝑀 ) 1 ) )
40 0iun ⊢ ∪ 𝑥 ∈ ∅ ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = ∅
41 39 40 eqtrdi ⊢ ( dom ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) = ∅ → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = ∅ )
42 33 41 sylbir ⊢ ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) = ∅ → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = ∅ )
43 42 necon3i ⊢ ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) ≠ ∅ → ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ≠ ∅ )
44 31 32 43 3syl ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ≠ ∅ )
45 rpssre ⊢ ℝ+ ⊆ ℝ
46 23 45 sstrdi ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ⊆ ℝ )
47 ltso ⊢ < Or ℝ
48 fisupcl ⊢ ( ( < Or ℝ ∧ ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ∈ Fin ∧ ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ≠ ∅ ∧ ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ⊆ ℝ ) ) → sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ∈ ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) )
49 47 48 mpan ⊢ ( ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ∈ Fin ∧ ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ≠ ∅ ∧ ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ⊆ ℝ ) → sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ∈ ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) )
50 28 44 46 49 syl3anc ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ∈ ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) )
51 23 50 sseldd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ∈ ℝ+ )
52 metxmet ⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
53 52 ad2antrr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
54 53 adantr ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
55 1red ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → 1 ∈ ℝ )
56 46 50 sseldd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ∈ ℝ )
57 56 adantr ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ∈ ℝ )
58 46 adantr ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ⊆ ℝ )
59 44 adantr ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ≠ ∅ )
60 28 adantr ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ∈ Fin )
61 fimaxre2 ⊢ ( ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ⊆ ℝ ∧ ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ∈ Fin ) → ∃ 𝑑 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) 𝑤 ≤ 𝑑 )
62 58 60 61 syl2anc ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → ∃ 𝑑 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) 𝑤 ≤ 𝑑 )
63 35 elrnmpt1 ⊢ ( ( 𝑧 ∈ 𝑣 ∧ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ∈ V ) → ( ( 𝑧 𝑀 𝑦 ) + 1 ) ∈ ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) )
64 34 63 mpan2 ⊢ ( 𝑧 ∈ 𝑣 → ( ( 𝑧 𝑀 𝑦 ) + 1 ) ∈ ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) )
65 64 adantl ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → ( ( 𝑧 𝑀 𝑦 ) + 1 ) ∈ ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) )
66 suprub ⊢ ( ( ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ⊆ ℝ ∧ ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ≠ ∅ ∧ ∃ 𝑑 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) 𝑤 ≤ 𝑑 ) ∧ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ∈ ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) ) → ( ( 𝑧 𝑀 𝑦 ) + 1 ) ≤ sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) )
67 58 59 62 65 66 syl31anc ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → ( ( 𝑧 𝑀 𝑦 ) + 1 ) ≤ sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) )
68 leaddsub ⊢ ( ( ( 𝑧 𝑀 𝑦 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ∈ ℝ ) → ( ( ( 𝑧 𝑀 𝑦 ) + 1 ) ≤ sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ↔ ( 𝑧 𝑀 𝑦 ) ≤ ( sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) − 1 ) ) )
69 18 55 57 68 syl3anc ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → ( ( ( 𝑧 𝑀 𝑦 ) + 1 ) ≤ sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ↔ ( 𝑧 𝑀 𝑦 ) ≤ ( sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) − 1 ) ) )
70 67 69 mpbid ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → ( 𝑧 𝑀 𝑦 ) ≤ ( sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) − 1 ) )
71 blss2 ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 1 ∈ ℝ ∧ sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ∈ ℝ ∧ ( 𝑧 𝑀 𝑦 ) ≤ ( sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) − 1 ) ) ) → ( 𝑧 ( ball ‘ 𝑀 ) 1 ) ⊆ ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ) )
72 54 15 16 55 57 70 71 syl33anc ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) ∧ 𝑧 ∈ 𝑣 ) → ( 𝑧 ( ball ‘ 𝑀 ) 1 ) ⊆ ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ) )
73 72 ralrimiva ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → ∀ 𝑧 ∈ 𝑣 ( 𝑧 ( ball ‘ 𝑀 ) 1 ) ⊆ ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ) )
74 nfcv ⊢ Ⅎ 𝑧 ( 𝑥 ( ball ‘ 𝑀 ) 1 )
75 nfcv ⊢ Ⅎ 𝑧 𝑦
76 nfcv ⊢ Ⅎ 𝑧 ( ball ‘ 𝑀 )
77 nfmpt1 ⊢ Ⅎ 𝑧 ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) )
78 77 nfrn ⊢ Ⅎ 𝑧 ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) )
79 nfcv ⊢ Ⅎ 𝑧 ℝ
80 nfcv ⊢ Ⅎ 𝑧 <
81 78 79 80 nfsup ⊢ Ⅎ 𝑧 sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < )
82 75 76 81 nfov ⊢ Ⅎ 𝑧 ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) )
83 74 82 nfss ⊢ Ⅎ 𝑧 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) ⊆ ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) )
84 nfv ⊢ Ⅎ 𝑥 ( 𝑧 ( ball ‘ 𝑀 ) 1 ) ⊆ ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) )
85 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = ( 𝑧 ( ball ‘ 𝑀 ) 1 ) )
86 85 sseq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ( ball ‘ 𝑀 ) 1 ) ⊆ ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ) ↔ ( 𝑧 ( ball ‘ 𝑀 ) 1 ) ⊆ ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ) ) )
87 83 84 86 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) ⊆ ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ) ↔ ∀ 𝑧 ∈ 𝑣 ( 𝑧 ( ball ‘ 𝑀 ) 1 ) ⊆ ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ) )
88 73 87 sylibr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → ∀ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) ⊆ ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ) )
89 iunss ⊢ ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) ⊆ ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ) ↔ ∀ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) ⊆ ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ) )
90 88 89 sylibr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) ⊆ ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ) )
91 30 90 eqsstrrd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → 𝑋 ⊆ ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ) )
92 51 rpxrd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ∈ ℝ* )
93 blssm ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ∈ ℝ* ) → ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ) ⊆ 𝑋 )
94 53 29 92 93 syl3anc ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ) ⊆ 𝑋 )
95 91 94 eqssd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ) )
96 oveq2 ⊢ ( 𝑑 = sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) → ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) = ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ) )
97 96 rspceeqv ⊢ ( ( sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ∈ ℝ+ ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) sup ( ran ( 𝑧 ∈ 𝑣 ↦ ( ( 𝑧 𝑀 𝑦 ) + 1 ) ) , ℝ , < ) ) ) → ∃ 𝑑 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) )
98 51 95 97 syl2anc ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 ) ) → ∃ 𝑑 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) )
99 98 rexlimdvaa ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 → ∃ 𝑑 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) ) )
100 99 ralrimdva ⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 → ∀ 𝑦 ∈ 𝑋 ∃ 𝑑 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) ) )
101 isbnd ⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑑 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) ) )
102 101 baib ⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ∀ 𝑦 ∈ 𝑋 ∃ 𝑑 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) ) )
103 100 102 sylibrd ⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 1 ) = 𝑋 → 𝑀 ∈ ( Bnd ‘ 𝑋 ) ) )
104 1 10 103 sylc ⊢ ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) → 𝑀 ∈ ( Bnd ‘ 𝑋 ) )