| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | xmetcl 24341 | . . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑃𝐷𝑥) ∈
ℝ*) | 
| 2 | 1 | ad4ant124 1174 | . . . . 5
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*))
∧ 𝑥 ∈ 𝑋) → (𝑃𝐷𝑥) ∈
ℝ*) | 
| 3 |  | simplrl 777 | . . . . 5
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*))
∧ 𝑥 ∈ 𝑋) → 𝑅 ∈
ℝ*) | 
| 4 |  | simplrr 778 | . . . . 5
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*))
∧ 𝑥 ∈ 𝑋) → 𝑆 ∈
ℝ*) | 
| 5 |  | xrltmin 13224 | . . . . 5
⊢ (((𝑃𝐷𝑥) ∈ ℝ* ∧ 𝑅 ∈ ℝ*
∧ 𝑆 ∈
ℝ*) → ((𝑃𝐷𝑥) < if(𝑅 ≤ 𝑆, 𝑅, 𝑆) ↔ ((𝑃𝐷𝑥) < 𝑅 ∧ (𝑃𝐷𝑥) < 𝑆))) | 
| 6 | 2, 3, 4, 5 | syl3anc 1373 | . . . 4
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*))
∧ 𝑥 ∈ 𝑋) → ((𝑃𝐷𝑥) < if(𝑅 ≤ 𝑆, 𝑅, 𝑆) ↔ ((𝑃𝐷𝑥) < 𝑅 ∧ (𝑃𝐷𝑥) < 𝑆))) | 
| 7 | 6 | pm5.32da 579 | . . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*))
→ ((𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < if(𝑅 ≤ 𝑆, 𝑅, 𝑆)) ↔ (𝑥 ∈ 𝑋 ∧ ((𝑃𝐷𝑥) < 𝑅 ∧ (𝑃𝐷𝑥) < 𝑆)))) | 
| 8 |  | ifcl 4571 | . . . 4
⊢ ((𝑅 ∈ ℝ*
∧ 𝑆 ∈
ℝ*) → if(𝑅 ≤ 𝑆, 𝑅, 𝑆) ∈
ℝ*) | 
| 9 |  | elbl 24398 | . . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ if(𝑅 ≤ 𝑆, 𝑅, 𝑆) ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘𝐷)if(𝑅 ≤ 𝑆, 𝑅, 𝑆)) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < if(𝑅 ≤ 𝑆, 𝑅, 𝑆)))) | 
| 10 | 9 | 3expa 1119 | . . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ if(𝑅 ≤ 𝑆, 𝑅, 𝑆) ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘𝐷)if(𝑅 ≤ 𝑆, 𝑅, 𝑆)) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < if(𝑅 ≤ 𝑆, 𝑅, 𝑆)))) | 
| 11 | 8, 10 | sylan2 593 | . . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*))
→ (𝑥 ∈ (𝑃(ball‘𝐷)if(𝑅 ≤ 𝑆, 𝑅, 𝑆)) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < if(𝑅 ≤ 𝑆, 𝑅, 𝑆)))) | 
| 12 |  | elbl 24398 | . . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))) | 
| 13 | 12 | 3expa 1119 | . . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑅 ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))) | 
| 14 | 13 | adantrr 717 | . . . . 5
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*))
→ (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))) | 
| 15 |  | elbl 24398 | . . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘𝐷)𝑆) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑆))) | 
| 16 | 15 | 3expa 1119 | . . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑆 ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘𝐷)𝑆) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑆))) | 
| 17 | 16 | adantrl 716 | . . . . 5
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*))
→ (𝑥 ∈ (𝑃(ball‘𝐷)𝑆) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑆))) | 
| 18 | 14, 17 | anbi12d 632 | . . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*))
→ ((𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑆)) ↔ ((𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) ∧ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑆)))) | 
| 19 |  | elin 3967 | . . . 4
⊢ (𝑥 ∈ ((𝑃(ball‘𝐷)𝑅) ∩ (𝑃(ball‘𝐷)𝑆)) ↔ (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ∧ 𝑥 ∈ (𝑃(ball‘𝐷)𝑆))) | 
| 20 |  | anandi 676 | . . . 4
⊢ ((𝑥 ∈ 𝑋 ∧ ((𝑃𝐷𝑥) < 𝑅 ∧ (𝑃𝐷𝑥) < 𝑆)) ↔ ((𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) ∧ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑆))) | 
| 21 | 18, 19, 20 | 3bitr4g 314 | . . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*))
→ (𝑥 ∈ ((𝑃(ball‘𝐷)𝑅) ∩ (𝑃(ball‘𝐷)𝑆)) ↔ (𝑥 ∈ 𝑋 ∧ ((𝑃𝐷𝑥) < 𝑅 ∧ (𝑃𝐷𝑥) < 𝑆)))) | 
| 22 | 7, 11, 21 | 3bitr4rd 312 | . 2
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*))
→ (𝑥 ∈ ((𝑃(ball‘𝐷)𝑅) ∩ (𝑃(ball‘𝐷)𝑆)) ↔ 𝑥 ∈ (𝑃(ball‘𝐷)if(𝑅 ≤ 𝑆, 𝑅, 𝑆)))) | 
| 23 | 22 | eqrdv 2735 | 1
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*))
→ ((𝑃(ball‘𝐷)𝑅) ∩ (𝑃(ball‘𝐷)𝑆)) = (𝑃(ball‘𝐷)if(𝑅 ≤ 𝑆, 𝑅, 𝑆))) |