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 ‘ 𝑚 ) 𝑟 ) } )