Metamath Proof Explorer

Theorem bndss

Description: A subset of a bounded metric space is bounded. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion bndss ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ∈ ( Bnd ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 metres2 ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ∈ ( Met ‘ 𝑆 ) )
2 1 adantlr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ∈ ( Met ‘ 𝑆 ) )
3 ssel2 ⊢ ( ( 𝑆 ⊆ 𝑋 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑋 )
4 3 ancoms ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑆 ⊆ 𝑋 ) → 𝑥 ∈ 𝑋 )
5 oveq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) )
6 5 eqeq2d ⊢ ( 𝑦 = 𝑥 → ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ↔ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
7 6 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ↔ ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
8 7 rspcva ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) → ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) )
9 4 8 sylan ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑆 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) → ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) )
10 9 adantlll ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) → ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) )
11 dfss ⊢ ( 𝑆 ⊆ 𝑋 ↔ 𝑆 = ( 𝑆 ∩ 𝑋 ) )
12 11 biimpi ⊢ ( 𝑆 ⊆ 𝑋 → 𝑆 = ( 𝑆 ∩ 𝑋 ) )
13 incom ⊢ ( 𝑆 ∩ 𝑋 ) = ( 𝑋 ∩ 𝑆 )
14 12 13 eqtrdi ⊢ ( 𝑆 ⊆ 𝑋 → 𝑆 = ( 𝑋 ∩ 𝑆 ) )
15 ineq1 ⊢ ( 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → ( 𝑋 ∩ 𝑆 ) = ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∩ 𝑆 ) )
16 14 15 sylan9eq ⊢ ( ( 𝑆 ⊆ 𝑋 ∧ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) → 𝑆 = ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∩ 𝑆 ) )
17 16 adantll ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) → 𝑆 = ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∩ 𝑆 ) )
18 17 adantlr ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) → 𝑆 = ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∩ 𝑆 ) )
19 eqid ⊢ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) = ( 𝑀 ↾ ( 𝑆 × 𝑆 ) )
20 19 blssp ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ) 𝑟 ) = ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∩ 𝑆 ) )
21 20 an4s ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ) 𝑟 ) = ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∩ 𝑆 ) )
22 21 anassrs ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ) 𝑟 ) = ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∩ 𝑆 ) )
23 22 adantr ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) → ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ) 𝑟 ) = ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∩ 𝑆 ) )
24 18 23 eqtr4d ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) → 𝑆 = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ) 𝑟 ) )
25 24 ex ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → 𝑆 = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ) 𝑟 ) ) )
26 25 reximdva ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → ∃ 𝑟 ∈ ℝ+ 𝑆 = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ) 𝑟 ) ) )
27 26 imp ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) → ∃ 𝑟 ∈ ℝ+ 𝑆 = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ) 𝑟 ) )
28 10 27 syldan ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) → ∃ 𝑟 ∈ ℝ+ 𝑆 = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ) 𝑟 ) )
29 28 an32s ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ∧ 𝑆 ⊆ 𝑋 ) → ∃ 𝑟 ∈ ℝ+ 𝑆 = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ) 𝑟 ) )
30 29 ex ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) → ( 𝑆 ⊆ 𝑋 → ∃ 𝑟 ∈ ℝ+ 𝑆 = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ) 𝑟 ) ) )
31 30 an32s ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑆 ⊆ 𝑋 → ∃ 𝑟 ∈ ℝ+ 𝑆 = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ) 𝑟 ) ) )
32 31 imp ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑆 ⊆ 𝑋 ) → ∃ 𝑟 ∈ ℝ+ 𝑆 = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ) 𝑟 ) )
33 32 an32s ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) → ∃ 𝑟 ∈ ℝ+ 𝑆 = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ) 𝑟 ) )
34 33 ralrimiva ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ∧ 𝑆 ⊆ 𝑋 ) → ∀ 𝑥 ∈ 𝑆 ∃ 𝑟 ∈ ℝ+ 𝑆 = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ) 𝑟 ) )
35 2 34 jca ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ∈ ( Met ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ∃ 𝑟 ∈ ℝ+ 𝑆 = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ) 𝑟 ) ) )
36 isbnd ⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) )
37 36 anbi1i ⊢ ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ↔ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) ∧ 𝑆 ⊆ 𝑋 ) )
38 isbnd ⊢ ( ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ∈ ( Bnd ‘ 𝑆 ) ↔ ( ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ∈ ( Met ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ∃ 𝑟 ∈ ℝ+ 𝑆 = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ) 𝑟 ) ) )
39 35 37 38 3imtr4i ⊢ ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) ∈ ( Bnd ‘ 𝑆 ) )