Metamath Proof Explorer

Theorem blssexps

Description: Two ways to express the existence of a ball subset. (Contributed by NM, 5-May-2007) (Revised by Mario Carneiro, 12-Nov-2013) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion blssexps ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ∃ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ↔ ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 blssps ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑃 ∈ 𝑥 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 )
2 sstr ⊢ ( ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 )
3 2 expcom ⊢ ( 𝑥 ⊆ 𝐴 → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 → ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) )
4 3 reximdv ⊢ ( 𝑥 ⊆ 𝐴 → ( ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) )
5 1 4 syl5com ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑃 ∈ 𝑥 ) → ( 𝑥 ⊆ 𝐴 → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) )
6 5 3expa ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ) ∧ 𝑃 ∈ 𝑥 ) → ( 𝑥 ⊆ 𝐴 → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) )
7 6 expimpd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ) → ( ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) )
8 7 adantlr ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ) → ( ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) )
9 8 rexlimdva ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ∃ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) )
10 simpll ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
11 simplr ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → 𝑃 ∈ 𝑋 )
12 rpxr ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* )
13 12 ad2antrl ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → 𝑟 ∈ ℝ* )
14 blelrnps ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ∈ ran ( ball ‘ 𝐷 ) )
15 10 11 13 14 syl3anc ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ∈ ran ( ball ‘ 𝐷 ) )
16 simprl ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → 𝑟 ∈ ℝ+ )
17 blcntrps ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) → 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) )
18 10 11 16 17 syl3anc ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) )
19 simprr ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 )
20 eleq2 ⊢ ( 𝑥 = ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑃 ∈ 𝑥 ↔ 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ) )
21 sseq1 ⊢ ( 𝑥 = ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑥 ⊆ 𝐴 ↔ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) )
22 20 21 anbi12d ⊢ ( 𝑥 = ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) → ( ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ↔ ( 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) )
23 22 rspcev ⊢ ( ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ∈ ran ( ball ‘ 𝐷 ) ∧ ( 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) )
24 15 18 19 23 syl12anc ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) )
25 24 rexlimdvaa ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 → ∃ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) )
26 9 25 impbid ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ∃ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ↔ ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) )