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

Metamath Proof Explorer

Theorem ballss3

Description: A sufficient condition for a ball being a subset. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses ballss3.y 
|- F/ x ph
ballss3.d 
|- ( ph -> D e. ( PsMet ` X ) )
ballss3.p 
|- ( ph -> P e. X )
ballss3.r 
|- ( ph -> R e. RR* )
ballss3.a 
|- ( ( ph /\ x e. X /\ ( P D x ) < R ) -> x e. A )
Assertion ballss3 
|- ( ph -> ( P ( ball ` D ) R ) C_ A )

Proof

Step Hyp Ref Expression
1 ballss3.y 
 |-  F/ x ph
2 ballss3.d 
 |-  ( ph -> D e. ( PsMet ` X ) )
3 ballss3.p 
 |-  ( ph -> P e. X )
4 ballss3.r 
 |-  ( ph -> R e. RR* )
5 ballss3.a 
 |-  ( ( ph /\ x e. X /\ ( P D x ) < R ) -> x e. A )
6 simpl 
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ph )
7 simpr 
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> x e. ( P ( ball ` D ) R ) )
8 elblps 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) -> ( x e. ( P ( ball ` D ) R ) <-> ( x e. X /\ ( P D x ) < R ) ) )
9 2 3 4 8 syl3anc 
 |-  ( ph -> ( x e. ( P ( ball ` D ) R ) <-> ( x e. X /\ ( P D x ) < R ) ) )
10 9 adantr 
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( x e. ( P ( ball ` D ) R ) <-> ( x e. X /\ ( P D x ) < R ) ) )
11 7 10 mpbid 
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( x e. X /\ ( P D x ) < R ) )
12 11 simpld 
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> x e. X )
13 11 simprd 
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( P D x ) < R )
14 6 12 13 5 syl3anc 
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> x e. A )
15 14 ex 
 |-  ( ph -> ( x e. ( P ( ball ` D ) R ) -> x e. A ) )
16 1 15 ralrimi 
 |-  ( ph -> A. x e. ( P ( ball ` D ) R ) x e. A )
17 dfss3 
 |-  ( ( P ( ball ` D ) R ) C_ A <-> A. x e. ( P ( ball ` D ) R ) x e. A )
18 16 17 sylibr 
 |-  ( ph -> ( P ( ball ` D ) R ) C_ A )