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 )