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

Metamath Proof Explorer

Definition df-bnd

Description: Define the class of bounded metrics. A metric space is bounded iff it can be covered by a single ball. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion df-bnd Bnd = ( 𝑥 ∈ V ↦ { 𝑚 ∈ ( Met ‘ 𝑥 ) ∣ ∀ 𝑦 ∈ 𝑥 ∃ 𝑟 ∈ ℝ+ 𝑥 = ( 𝑦 ( ball ‘ 𝑚 ) 𝑟 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbnd ⊢ Bnd
1 vx ⊢ 𝑥
2 cvv ⊢ V
3 vm ⊢ 𝑚
4 cmet ⊢ Met
5 1 cv ⊢ 𝑥
6 5 4 cfv ⊢ ( Met ‘ 𝑥 )
7 vy ⊢ 𝑦
8 vr ⊢ 𝑟
9 crp ⊢ ℝ+
10 7 cv ⊢ 𝑦
11 cbl ⊢ ball
12 3 cv ⊢ 𝑚
13 12 11 cfv ⊢ ( ball ‘ 𝑚 )
14 8 cv ⊢ 𝑟
15 10 14 13 co ⊢ ( 𝑦 ( ball ‘ 𝑚 ) 𝑟 )
16 5 15 wceq ⊢ 𝑥 = ( 𝑦 ( ball ‘ 𝑚 ) 𝑟 )
17 16 8 9 wrex ⊢ ∃ 𝑟 ∈ ℝ+ 𝑥 = ( 𝑦 ( ball ‘ 𝑚 ) 𝑟 )
18 17 7 5 wral ⊢ ∀ 𝑦 ∈ 𝑥 ∃ 𝑟 ∈ ℝ+ 𝑥 = ( 𝑦 ( ball ‘ 𝑚 ) 𝑟 )
19 18 3 6 crab ⊢ { 𝑚 ∈ ( Met ‘ 𝑥 ) ∣ ∀ 𝑦 ∈ 𝑥 ∃ 𝑟 ∈ ℝ+ 𝑥 = ( 𝑦 ( ball ‘ 𝑚 ) 𝑟 ) }
20 1 2 19 cmpt ⊢ ( 𝑥 ∈ V ↦ { 𝑚 ∈ ( Met ‘ 𝑥 ) ∣ ∀ 𝑦 ∈ 𝑥 ∃ 𝑟 ∈ ℝ+ 𝑥 = ( 𝑦 ( ball ‘ 𝑚 ) 𝑟 ) } )
21 0 20 wceq ⊢ Bnd = ( 𝑥 ∈ V ↦ { 𝑚 ∈ ( Met ‘ 𝑥 ) ∣ ∀ 𝑦 ∈ 𝑥 ∃ 𝑟 ∈ ℝ+ 𝑥 = ( 𝑦 ( ball ‘ 𝑚 ) 𝑟 ) } )