Metamath Proof Explorer

Theorem ssblex

Description: A nested ball exists whose radius is less than any desired amount. (Contributed by NM, 20-Sep-2007) (Revised by Mario Carneiro, 12-Nov-2013)

Ref Expression
Assertion ssblex ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝑥 < 𝑅 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → 𝑅 ∈ ℝ+ )
2 1 rphalfcld ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → ( 𝑅 / 2 ) ∈ ℝ+ )
3 simprr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → 𝑆 ∈ ℝ+ )
4 2 3 ifcld ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) ∈ ℝ+ )
5 4 rpred ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) ∈ ℝ )
6 2 rpred ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → ( 𝑅 / 2 ) ∈ ℝ )
7 1 rpred ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → 𝑅 ∈ ℝ )
8 3 rpred ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → 𝑆 ∈ ℝ )
9 min1 ⊢ ( ( ( 𝑅 / 2 ) ∈ ℝ ∧ 𝑆 ∈ ℝ ) → if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) ≤ ( 𝑅 / 2 ) )
10 6 8 9 syl2anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) ≤ ( 𝑅 / 2 ) )
11 1 rpgt0d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → 0 < 𝑅 )
12 halfpos ⊢ ( 𝑅 ∈ ℝ → ( 0 < 𝑅 ↔ ( 𝑅 / 2 ) < 𝑅 ) )
13 7 12 syl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → ( 0 < 𝑅 ↔ ( 𝑅 / 2 ) < 𝑅 ) )
14 11 13 mpbid ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → ( 𝑅 / 2 ) < 𝑅 )
15 5 6 7 10 14 lelttrd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) < 𝑅 )
16 simpl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) )
17 4 rpxrd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) ∈ ℝ* )
18 3 rpxrd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → 𝑆 ∈ ℝ* )
19 min2 ⊢ ( ( ( 𝑅 / 2 ) ∈ ℝ ∧ 𝑆 ∈ ℝ ) → if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) ≤ 𝑆 )
20 6 8 19 syl2anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) ≤ 𝑆 )
21 ssbl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) ≤ 𝑆 ) → ( 𝑃 ( ball ‘ 𝐷 ) if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) )
22 16 17 18 20 21 syl121anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → ( 𝑃 ( ball ‘ 𝐷 ) if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) )
23 breq1 ⊢ ( 𝑥 = if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) → ( 𝑥 < 𝑅 ↔ if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) < 𝑅 ) )
24 oveq2 ⊢ ( 𝑥 = if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) = ( 𝑃 ( ball ‘ 𝐷 ) if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) ) )
25 24 sseq1d ⊢ ( 𝑥 = if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑃 ( ball ‘ 𝐷 ) if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) )
26 23 25 anbi12d ⊢ ( 𝑥 = if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) → ( ( 𝑥 < 𝑅 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ ( if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) < 𝑅 ∧ ( 𝑃 ( ball ‘ 𝐷 ) if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) ) )
27 26 rspcev ⊢ ( ( if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) ∈ ℝ+ ∧ ( if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) < 𝑅 ∧ ( 𝑃 ( ball ‘ 𝐷 ) if ( ( 𝑅 / 2 ) ≤ 𝑆 , ( 𝑅 / 2 ) , 𝑆 ) ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝑥 < 𝑅 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) )
28 4 15 22 27 syl12anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+ ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝑥 < 𝑅 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) )