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 ‘ 𝐷 ) 𝑅 ) ⊆ 𝐴 )