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 ) )