Metamath Proof Explorer


Theorem blssexps

Description: Two ways to express the existence of a ball subset. (Contributed by NM, 5-May-2007) (Revised by Mario Carneiro, 12-Nov-2013) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion blssexps
|- ( ( D e. ( PsMet ` X ) /\ P e. X ) -> ( E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) <-> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) )

Proof

Step Hyp Ref Expression
1 blssps
 |-  ( ( D e. ( PsMet ` X ) /\ x e. ran ( ball ` D ) /\ P e. x ) -> E. r e. RR+ ( P ( ball ` D ) r ) C_ x )
2 sstr
 |-  ( ( ( P ( ball ` D ) r ) C_ x /\ x C_ A ) -> ( P ( ball ` D ) r ) C_ A )
3 2 expcom
 |-  ( x C_ A -> ( ( P ( ball ` D ) r ) C_ x -> ( P ( ball ` D ) r ) C_ A ) )
4 3 reximdv
 |-  ( x C_ A -> ( E. r e. RR+ ( P ( ball ` D ) r ) C_ x -> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) )
5 1 4 syl5com
 |-  ( ( D e. ( PsMet ` X ) /\ x e. ran ( ball ` D ) /\ P e. x ) -> ( x C_ A -> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) )
6 5 3expa
 |-  ( ( ( D e. ( PsMet ` X ) /\ x e. ran ( ball ` D ) ) /\ P e. x ) -> ( x C_ A -> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) )
7 6 expimpd
 |-  ( ( D e. ( PsMet ` X ) /\ x e. ran ( ball ` D ) ) -> ( ( P e. x /\ x C_ A ) -> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) )
8 7 adantlr
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ x e. ran ( ball ` D ) ) -> ( ( P e. x /\ x C_ A ) -> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) )
9 8 rexlimdva
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X ) -> ( E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) -> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) )
10 simpll
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( r e. RR+ /\ ( P ( ball ` D ) r ) C_ A ) ) -> D e. ( PsMet ` X ) )
11 simplr
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( r e. RR+ /\ ( P ( ball ` D ) r ) C_ A ) ) -> P e. X )
12 rpxr
 |-  ( r e. RR+ -> r e. RR* )
13 12 ad2antrl
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( r e. RR+ /\ ( P ( ball ` D ) r ) C_ A ) ) -> r e. RR* )
14 blelrnps
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ r e. RR* ) -> ( P ( ball ` D ) r ) e. ran ( ball ` D ) )
15 10 11 13 14 syl3anc
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( r e. RR+ /\ ( P ( ball ` D ) r ) C_ A ) ) -> ( P ( ball ` D ) r ) e. ran ( ball ` D ) )
16 simprl
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( r e. RR+ /\ ( P ( ball ` D ) r ) C_ A ) ) -> r e. RR+ )
17 blcntrps
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ r e. RR+ ) -> P e. ( P ( ball ` D ) r ) )
18 10 11 16 17 syl3anc
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( r e. RR+ /\ ( P ( ball ` D ) r ) C_ A ) ) -> P e. ( P ( ball ` D ) r ) )
19 simprr
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( r e. RR+ /\ ( P ( ball ` D ) r ) C_ A ) ) -> ( P ( ball ` D ) r ) C_ A )
20 eleq2
 |-  ( x = ( P ( ball ` D ) r ) -> ( P e. x <-> P e. ( P ( ball ` D ) r ) ) )
21 sseq1
 |-  ( x = ( P ( ball ` D ) r ) -> ( x C_ A <-> ( P ( ball ` D ) r ) C_ A ) )
22 20 21 anbi12d
 |-  ( x = ( P ( ball ` D ) r ) -> ( ( P e. x /\ x C_ A ) <-> ( P e. ( P ( ball ` D ) r ) /\ ( P ( ball ` D ) r ) C_ A ) ) )
23 22 rspcev
 |-  ( ( ( P ( ball ` D ) r ) e. ran ( ball ` D ) /\ ( P e. ( P ( ball ` D ) r ) /\ ( P ( ball ` D ) r ) C_ A ) ) -> E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) )
24 15 18 19 23 syl12anc
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( r e. RR+ /\ ( P ( ball ` D ) r ) C_ A ) ) -> E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) )
25 24 rexlimdvaa
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X ) -> ( E. r e. RR+ ( P ( ball ` D ) r ) C_ A -> E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) ) )
26 9 25 impbid
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X ) -> ( E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) <-> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) )