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 ⊢ Ⅎ 𝑥 𝜑
ballss3.d ⊢ ( 𝜑 → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
ballss3.p ⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
ballss3.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
ballss3.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) → 𝑥 ∈ 𝐴 )
Assertion ballss3 ( 𝜑 → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 ballss3.y ⊢ Ⅎ 𝑥 𝜑
2 ballss3.d ⊢ ( 𝜑 → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
3 ballss3.p ⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
4 ballss3.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
5 ballss3.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) → 𝑥 ∈ 𝐴 )
6 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝜑 )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) )
8 elblps ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
9 2 3 4 8 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
11 7 10 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) )
12 11 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑥 ∈ 𝑋 )
13 11 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑃 𝐷 𝑥 ) < 𝑅 )
14 6 12 13 5 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑥 ∈ 𝐴 )
15 14 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) → 𝑥 ∈ 𝐴 ) )
16 1 15 ralrimi ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) 𝑥 ∈ 𝐴 )
17 dfss3 ⊢ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝐴 ↔ ∀ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) 𝑥 ∈ 𝐴 )
18 16 17 sylibr ⊢ ( 𝜑 → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝐴 )