| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elfvdm 6942 | . . . . . . 7
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 ∈ dom ∞Met) | 
| 2 |  | isxmet 24335 | . . . . . . 7
⊢ (𝑋 ∈ dom ∞Met →
(𝐷 ∈
(∞Met‘𝑋) ↔
(𝐷:(𝑋 × 𝑋)⟶ℝ* ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))))) | 
| 3 | 1, 2 | syl 17 | . . . . . 6
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐷 ∈ (∞Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))))) | 
| 4 | 3 | ibi 267 | . . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))) | 
| 5 |  | simpr 484 | . . . . . 6
⊢ ((((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))) → ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))) | 
| 6 | 5 | 2ralimi 3122 | . . . . 5
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))) | 
| 7 | 4, 6 | simpl2im 503 | . . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))) | 
| 8 |  | oveq1 7439 | . . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥𝐷𝑦) = (𝐴𝐷𝑦)) | 
| 9 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑧𝐷𝑥) = (𝑧𝐷𝐴)) | 
| 10 | 9 | oveq1d 7447 | . . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷𝐴) +𝑒 (𝑧𝐷𝑦))) | 
| 11 | 8, 10 | breq12d 5155 | . . . . 5
⊢ (𝑥 = 𝐴 → ((𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) ↔ (𝐴𝐷𝑦) ≤ ((𝑧𝐷𝐴) +𝑒 (𝑧𝐷𝑦)))) | 
| 12 |  | oveq2 7440 | . . . . . 6
⊢ (𝑦 = 𝐵 → (𝐴𝐷𝑦) = (𝐴𝐷𝐵)) | 
| 13 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑧𝐷𝑦) = (𝑧𝐷𝐵)) | 
| 14 | 13 | oveq2d 7448 | . . . . . 6
⊢ (𝑦 = 𝐵 → ((𝑧𝐷𝐴) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷𝐴) +𝑒 (𝑧𝐷𝐵))) | 
| 15 | 12, 14 | breq12d 5155 | . . . . 5
⊢ (𝑦 = 𝐵 → ((𝐴𝐷𝑦) ≤ ((𝑧𝐷𝐴) +𝑒 (𝑧𝐷𝑦)) ↔ (𝐴𝐷𝐵) ≤ ((𝑧𝐷𝐴) +𝑒 (𝑧𝐷𝐵)))) | 
| 16 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑧 = 𝐶 → (𝑧𝐷𝐴) = (𝐶𝐷𝐴)) | 
| 17 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑧 = 𝐶 → (𝑧𝐷𝐵) = (𝐶𝐷𝐵)) | 
| 18 | 16, 17 | oveq12d 7450 | . . . . . 6
⊢ (𝑧 = 𝐶 → ((𝑧𝐷𝐴) +𝑒 (𝑧𝐷𝐵)) = ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵))) | 
| 19 | 18 | breq2d 5154 | . . . . 5
⊢ (𝑧 = 𝐶 → ((𝐴𝐷𝐵) ≤ ((𝑧𝐷𝐴) +𝑒 (𝑧𝐷𝐵)) ↔ (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵)))) | 
| 20 | 11, 15, 19 | rspc3v 3637 | . . . 4
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵)))) | 
| 21 | 7, 20 | syl5 34 | . . 3
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐷 ∈ (∞Met‘𝑋) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵)))) | 
| 22 | 21 | 3comr 1125 | . 2
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐷 ∈ (∞Met‘𝑋) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵)))) | 
| 23 | 22 | impcom 407 | 1
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵))) |