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 
|- ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( B i^i C ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> D e. ( *Met ` X ) )
2 simprl 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> B e. ran ( ball ` D ) )
3 simplr 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> P e. ( B i^i C ) )
4 3 elin1d 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> P e. B )
5 blss 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ran ( ball ` D ) /\ P e. B ) -> E. y e. RR+ ( P ( ball ` D ) y ) C_ B )
6 1 2 4 5 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> E. y e. RR+ ( P ( ball ` D ) y ) C_ B )
7 simprr 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> C e. ran ( ball ` D ) )
8 3 elin2d 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> P e. C )
9 blss 
 |-  ( ( D e. ( *Met ` X ) /\ C e. ran ( ball ` D ) /\ P e. C ) -> E. z e. RR+ ( P ( ball ` D ) z ) C_ C )
10 1 7 8 9 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> E. z e. RR+ ( P ( ball ` D ) z ) C_ C )
11 reeanv 
 |-  ( E. y e. RR+ E. z e. RR+ ( ( P ( ball ` D ) y ) C_ B /\ ( P ( ball ` D ) z ) C_ C ) <-> ( E. y e. RR+ ( P ( ball ` D ) y ) C_ B /\ E. z e. RR+ ( P ( ball ` D ) z ) C_ C ) )
12 ss2in 
 |-  ( ( ( P ( ball ` D ) y ) C_ B /\ ( P ( ball ` D ) z ) C_ C ) -> ( ( P ( ball ` D ) y ) i^i ( P ( ball ` D ) z ) ) C_ ( B i^i C ) )
13 inss1 
 |-  ( B i^i C ) C_ B
14 blf 
 |-  ( D e. ( *Met ` X ) -> ( ball ` D ) : ( X X. RR* ) --> ~P X )
15 frn 
 |-  ( ( ball ` D ) : ( X X. RR* ) --> ~P X -> ran ( ball ` D ) C_ ~P X )
16 1 14 15 3syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> ran ( ball ` D ) C_ ~P X )
17 16 2 sseldd 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> B e. ~P X )
18 17 elpwid 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> B C_ X )
19 13 18 sstrid 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> ( B i^i C ) C_ X )
20 19 3 sseldd 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> P e. X )
21 1 20 jca 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> ( D e. ( *Met ` X ) /\ P e. X ) )
22 rpxr 
 |-  ( y e. RR+ -> y e. RR* )
23 rpxr 
 |-  ( z e. RR+ -> z e. RR* )
24 22 23 anim12i 
 |-  ( ( y e. RR+ /\ z e. RR+ ) -> ( y e. RR* /\ z e. RR* ) )
25 blin 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( y e. RR* /\ z e. RR* ) ) -> ( ( P ( ball ` D ) y ) i^i ( P ( ball ` D ) z ) ) = ( P ( ball ` D ) if ( y <_ z , y , z ) ) )
26 21 24 25 syl2an 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) /\ ( y e. RR+ /\ z e. RR+ ) ) -> ( ( P ( ball ` D ) y ) i^i ( P ( ball ` D ) z ) ) = ( P ( ball ` D ) if ( y <_ z , y , z ) ) )
27 26 sseq1d 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) /\ ( y e. RR+ /\ z e. RR+ ) ) -> ( ( ( P ( ball ` D ) y ) i^i ( P ( ball ` D ) z ) ) C_ ( B i^i C ) <-> ( P ( ball ` D ) if ( y <_ z , y , z ) ) C_ ( B i^i C ) ) )
28 ifcl 
 |-  ( ( y e. RR+ /\ z e. RR+ ) -> if ( y <_ z , y , z ) e. RR+ )
29 oveq2 
 |-  ( x = if ( y <_ z , y , z ) -> ( P ( ball ` D ) x ) = ( P ( ball ` D ) if ( y <_ z , y , z ) ) )
30 29 sseq1d 
 |-  ( x = if ( y <_ z , y , z ) -> ( ( P ( ball ` D ) x ) C_ ( B i^i C ) <-> ( P ( ball ` D ) if ( y <_ z , y , z ) ) C_ ( B i^i C ) ) )
31 30 rspcev 
 |-  ( ( if ( y <_ z , y , z ) e. RR+ /\ ( P ( ball ` D ) if ( y <_ z , y , z ) ) C_ ( B i^i C ) ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( B i^i C ) )
32 31 ex 
 |-  ( if ( y <_ z , y , z ) e. RR+ -> ( ( P ( ball ` D ) if ( y <_ z , y , z ) ) C_ ( B i^i C ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( B i^i C ) ) )
33 28 32 syl 
 |-  ( ( y e. RR+ /\ z e. RR+ ) -> ( ( P ( ball ` D ) if ( y <_ z , y , z ) ) C_ ( B i^i C ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( B i^i C ) ) )
34 33 adantl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) /\ ( y e. RR+ /\ z e. RR+ ) ) -> ( ( P ( ball ` D ) if ( y <_ z , y , z ) ) C_ ( B i^i C ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( B i^i C ) ) )
35 27 34 sylbid 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) /\ ( y e. RR+ /\ z e. RR+ ) ) -> ( ( ( P ( ball ` D ) y ) i^i ( P ( ball ` D ) z ) ) C_ ( B i^i C ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( B i^i C ) ) )
36 12 35 syl5 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) /\ ( y e. RR+ /\ z e. RR+ ) ) -> ( ( ( P ( ball ` D ) y ) C_ B /\ ( P ( ball ` D ) z ) C_ C ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( B i^i C ) ) )
37 36 rexlimdvva 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> ( E. y e. RR+ E. z e. RR+ ( ( P ( ball ` D ) y ) C_ B /\ ( P ( ball ` D ) z ) C_ C ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( B i^i C ) ) )
38 11 37 syl5bir 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> ( ( E. y e. RR+ ( P ( ball ` D ) y ) C_ B /\ E. z e. RR+ ( P ( ball ` D ) z ) C_ C ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( B i^i C ) ) )
39 6 10 38 mp2and 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( B i^i C ) )