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 ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝐵 ∩ 𝐶 ) )