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 x φ
ballss3.d φ D PsMet X
ballss3.p φ P X
ballss3.r φ R *
ballss3.a φ x X P D x < R x A
Assertion ballss3 φ P ball D R A

Proof

Step Hyp Ref Expression
1 ballss3.y x φ
2 ballss3.d φ D PsMet X
3 ballss3.p φ P X
4 ballss3.r φ R *
5 ballss3.a φ x X P D x < R x A
6 simpl φ x P ball D R φ
7 simpr φ x P ball D R x P ball D R
8 elblps D PsMet X P X R * x P ball D R x X P D x < R
9 2 3 4 8 syl3anc φ x P ball D R x X P D x < R
10 9 adantr φ x P ball D R x P ball D R x X P D x < R
11 7 10 mpbid φ x P ball D R x X P D x < R
12 11 simpld φ x P ball D R x X
13 11 simprd φ x P ball D R P D x < R
14 6 12 13 5 syl3anc φ x P ball D R x A
15 14 ex φ x P ball D R x A
16 1 15 ralrimi φ x P ball D R x A
17 dfss3 P ball D R A x P ball D R x A
18 16 17 sylibr φ P ball D R A