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

Metamath Proof Explorer

Theorem blin2

Description: Given any two balls and a point in their intersection, there is a ball contained in the intersection with the given center point. (Contributed by Mario Carneiro, 12-Nov-2013)

Ref Expression
Assertion blin2 ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝐵 ∩ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
2 simprl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → 𝐵 ∈ ran ( ball ‘ 𝐷 ) )
3 simplr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) )
4 3 elin1d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → 𝑃 ∈ 𝐵 )
5 blss ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑃 ∈ 𝐵 ) → ∃ 𝑦 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐵 )
6 1 2 4 5 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → ∃ 𝑦 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐵 )
7 simprr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → 𝐶 ∈ ran ( ball ‘ 𝐷 ) )
8 3 elin2d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → 𝑃 ∈ 𝐶 )
9 blss ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑃 ∈ 𝐶 ) → ∃ 𝑧 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑧 ) ⊆ 𝐶 )
10 1 7 8 9 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → ∃ 𝑧 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑧 ) ⊆ 𝐶 )
11 reeanv ⊢ ( ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐵 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑧 ) ⊆ 𝐶 ) ↔ ( ∃ 𝑦 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐵 ∧ ∃ 𝑧 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑧 ) ⊆ 𝐶 ) )
12 ss2in ⊢ ( ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐵 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑧 ) ⊆ 𝐶 ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑧 ) ) ⊆ ( 𝐵 ∩ 𝐶 ) )
13 inss1 ⊢ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐵
14 blf ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ball ‘ 𝐷 ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 )
15 frn ⊢ ( ( ball ‘ 𝐷 ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 → ran ( ball ‘ 𝐷 ) ⊆ 𝒫 𝑋 )
16 1 14 15 3syl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → ran ( ball ‘ 𝐷 ) ⊆ 𝒫 𝑋 )
17 16 2 sseldd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → 𝐵 ∈ 𝒫 𝑋 )
18 17 elpwid ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → 𝐵 ⊆ 𝑋 )
19 13 18 sstrid ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → ( 𝐵 ∩ 𝐶 ) ⊆ 𝑋 )
20 19 3 sseldd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → 𝑃 ∈ 𝑋 )
21 1 20 jca ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) )
22 rpxr ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ* )
23 rpxr ⊢ ( 𝑧 ∈ ℝ+ → 𝑧 ∈ ℝ* )
24 22 23 anim12i ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) → ( 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) )
25 blin ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑧 ) ) = ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) )
26 21 24 25 syl2an ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑧 ) ) = ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) )
27 26 sseq1d ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑧 ) ) ⊆ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) ⊆ ( 𝐵 ∩ 𝐶 ) ) )
28 ifcl ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) → if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ∈ ℝ+ )
29 oveq2 ⊢ ( 𝑥 = if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) = ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) )
30 29 sseq1d ⊢ ( 𝑥 = if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) ⊆ ( 𝐵 ∩ 𝐶 ) ) )
31 30 rspcev ⊢ ( ( if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) ⊆ ( 𝐵 ∩ 𝐶 ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝐵 ∩ 𝐶 ) )
32 31 ex ⊢ ( if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ∈ ℝ+ → ( ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) ⊆ ( 𝐵 ∩ 𝐶 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝐵 ∩ 𝐶 ) ) )
33 28 32 syl ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) → ( ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) ⊆ ( 𝐵 ∩ 𝐶 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝐵 ∩ 𝐶 ) ) )
34 33 adantl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) ⊆ ( 𝐵 ∩ 𝐶 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝐵 ∩ 𝐶 ) ) )
35 27 34 sylbid ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑧 ) ) ⊆ ( 𝐵 ∩ 𝐶 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝐵 ∩ 𝐶 ) ) )
36 12 35 syl5 ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐵 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑧 ) ⊆ 𝐶 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝐵 ∩ 𝐶 ) ) )
37 36 rexlimdvva ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → ( ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐵 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑧 ) ⊆ 𝐶 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝐵 ∩ 𝐶 ) ) )
38 11 37 biimtrrid ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → ( ( ∃ 𝑦 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐵 ∧ ∃ 𝑧 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑧 ) ⊆ 𝐶 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝐵 ∩ 𝐶 ) ) )
39 6 10 38 mp2and ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝐶 ∈ ran ( ball ‘ 𝐷 ) ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝐵 ∩ 𝐶 ) )