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