Metamath Proof Explorer

Theorem blbnd

Description: A ball is bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 15-Jan-2014)

Ref Expression
Assertion blbnd ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) → ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ∈ ( Bnd ‘ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
2 rexr ⊢ ( 𝑅 ∈ ℝ → 𝑅 ∈ ℝ* )
3 blssm ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ⊆ 𝑋 )
4 2 3 syl3an3 ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) → ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ⊆ 𝑋 )
5 xmetres2 ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ⊆ 𝑋 ) → ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ∈ ( ∞Met ‘ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) )
6 1 4 5 syl2anc ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) → ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ∈ ( ∞Met ‘ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) )
7 6 adantr ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) = ∅ ) → ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ∈ ( ∞Met ‘ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) )
8 rzal ⊢ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) = ∅ → ∀ 𝑥 ∈ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ∃ 𝑟 ∈ ℝ+ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ) 𝑟 ) )
9 8 adantl ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) = ∅ ) → ∀ 𝑥 ∈ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ∃ 𝑟 ∈ ℝ+ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ) 𝑟 ) )
10 isbndx ⊢ ( ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ∈ ( Bnd ‘ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ↔ ( ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ∈ ( ∞Met ‘ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ∃ 𝑟 ∈ ℝ+ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ) 𝑟 ) ) )
11 7 9 10 sylanbrc ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) = ∅ ) → ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ∈ ( Bnd ‘ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) )
12 6 adantr ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ) → ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ∈ ( ∞Met ‘ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) )
13 1 adantr ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
14 simpl2 ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ) → 𝑌 ∈ 𝑋 )
15 simpl3 ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ) → 𝑅 ∈ ℝ )
16 xbln0 ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ↔ 0 < 𝑅 ) )
17 2 16 syl3an3 ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) → ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ↔ 0 < 𝑅 ) )
18 17 biimpa ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ) → 0 < 𝑅 )
19 15 18 elrpd ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ) → 𝑅 ∈ ℝ+ )
20 blcntr ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → 𝑌 ∈ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) )
21 13 14 19 20 syl3anc ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ) → 𝑌 ∈ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) )
22 14 21 elind ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ) → 𝑌 ∈ ( 𝑋 ∩ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) )
23 15 rexrd ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ) → 𝑅 ∈ ℝ* )
24 eqid ⊢ ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) = ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) )
25 24 blres ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ ( 𝑋 ∩ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑌 ( ball ‘ ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ) 𝑅 ) = ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ∩ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) )
26 13 22 23 25 syl3anc ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ) → ( 𝑌 ( ball ‘ ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ) 𝑅 ) = ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ∩ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) )
27 inidm ⊢ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ∩ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) = ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 )
28 26 27 eqtr2di ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ) → ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) = ( 𝑌 ( ball ‘ ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ) 𝑅 ) )
29 rspceov ⊢ ( ( 𝑌 ∈ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) = ( 𝑌 ( ball ‘ ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ) 𝑅 ) ) → ∃ 𝑥 ∈ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ∃ 𝑟 ∈ ℝ+ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ) 𝑟 ) )
30 21 19 28 29 syl3anc ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ) → ∃ 𝑥 ∈ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ∃ 𝑟 ∈ ℝ+ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ) 𝑟 ) )
31 isbnd2 ⊢ ( ( ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ∈ ( Bnd ‘ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ) ↔ ( ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ∈ ( ∞Met ‘ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ∧ ∃ 𝑥 ∈ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ∃ 𝑟 ∈ ℝ+ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) = ( 𝑥 ( ball ‘ ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ) 𝑟 ) ) )
32 12 30 31 sylanbrc ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ) → ( ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ∈ ( Bnd ‘ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ) )
33 32 simpld ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) ∧ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ≠ ∅ ) → ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ∈ ( Bnd ‘ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) )
34 11 33 pm2.61dane ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ ) → ( 𝑀 ↾ ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) × ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) ) ∈ ( Bnd ‘ ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ) )