Metamath Proof Explorer

Theorem isxmet2d

Description: It is safe to only require the triangle inequality when the values are real (so that we can use the standard addition over the reals), but in this case the nonnegativity constraint cannot be deduced and must be provided separately. (Counterexample: D ( x , y ) = if ( x = y , 0 , -oo ) satisfies all hypotheses except nonnegativity.) (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses isxmetd.0 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
isxmetd.1 ⊢ ( 𝜑 → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
isxmet2d.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 0 ≤ ( 𝑥 𝐷 𝑦 ) )
isxmet2d.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ↔ 𝑥 = 𝑦 ) )
isxmet2d.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
Assertion isxmet2d ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 isxmetd.0 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 isxmetd.1 ⊢ ( 𝜑 → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
3 isxmet2d.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 0 ≤ ( 𝑥 𝐷 𝑦 ) )
4 isxmet2d.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ↔ 𝑥 = 𝑦 ) )
5 isxmet2d.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
6 2 fovrnda ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ* )
7 0xr ⊢ 0 ∈ ℝ*
8 xrletri3 ⊢ ( ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ∧ 0 ≤ ( 𝑥 𝐷 𝑦 ) ) ) )
9 6 7 8 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ∧ 0 ≤ ( 𝑥 𝐷 𝑦 ) ) ) )
10 3 biantrud ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ↔ ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ∧ 0 ≤ ( 𝑥 𝐷 𝑦 ) ) ) )
11 9 10 4 3bitr2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
12 5 3expa ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
13 rexadd ⊢ ( ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) → ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
14 13 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) → ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
15 12 14 breqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
16 15 anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
17 6 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ* )
18 pnfge ⊢ ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ* → ( 𝑥 𝐷 𝑦 ) ≤ +∞ )
19 17 18 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ≤ +∞ )
20 19 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) ∧ ( 𝑧 𝐷 𝑦 ) = +∞ ) → ( 𝑥 𝐷 𝑦 ) ≤ +∞ )
21 oveq2 ⊢ ( ( 𝑧 𝐷 𝑦 ) = +∞ → ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = ( ( 𝑧 𝐷 𝑥 ) +𝑒 +∞ ) )
22 2 ffnd ⊢ ( 𝜑 → 𝐷 Fn ( 𝑋 × 𝑋 ) )
23 elxrge0 ⊢ ( ( 𝑥 𝐷 𝑦 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ* ∧ 0 ≤ ( 𝑥 𝐷 𝑦 ) ) )
24 6 3 23 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ∈ ( 0 [,] +∞ ) )
25 24 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ∈ ( 0 [,] +∞ ) )
26 ffnov ⊢ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] +∞ ) ↔ ( 𝐷 Fn ( 𝑋 × 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ∈ ( 0 [,] +∞ ) ) )
27 22 25 26 sylanbrc ⊢ ( 𝜑 → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] +∞ ) )
28 27 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] +∞ ) )
29 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑧 ∈ 𝑋 )
30 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
31 28 29 30 fovrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 𝐷 𝑥 ) ∈ ( 0 [,] +∞ ) )
32 eliccxr ⊢ ( ( 𝑧 𝐷 𝑥 ) ∈ ( 0 [,] +∞ ) → ( 𝑧 𝐷 𝑥 ) ∈ ℝ* )
33 31 32 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 𝐷 𝑥 ) ∈ ℝ* )
34 renemnf ⊢ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ → ( 𝑧 𝐷 𝑥 ) ≠ -∞ )
35 xaddpnf1 ⊢ ( ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ* ∧ ( 𝑧 𝐷 𝑥 ) ≠ -∞ ) → ( ( 𝑧 𝐷 𝑥 ) +𝑒 +∞ ) = +∞ )
36 33 34 35 syl2an ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) → ( ( 𝑧 𝐷 𝑥 ) +𝑒 +∞ ) = +∞ )
37 21 36 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) ∧ ( 𝑧 𝐷 𝑦 ) = +∞ ) → ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = +∞ )
38 20 37 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) ∧ ( 𝑧 𝐷 𝑦 ) = +∞ ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
39 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
40 28 29 39 fovrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 𝐷 𝑦 ) ∈ ( 0 [,] +∞ ) )
41 eliccxr ⊢ ( ( 𝑧 𝐷 𝑦 ) ∈ ( 0 [,] +∞ ) → ( 𝑧 𝐷 𝑦 ) ∈ ℝ* )
42 40 41 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 𝐷 𝑦 ) ∈ ℝ* )
43 elxrge0 ⊢ ( ( 𝑧 𝐷 𝑦 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑧 𝐷 𝑦 ) ∈ ℝ* ∧ 0 ≤ ( 𝑧 𝐷 𝑦 ) ) )
44 43 simprbi ⊢ ( ( 𝑧 𝐷 𝑦 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝑧 𝐷 𝑦 ) )
45 40 44 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 0 ≤ ( 𝑧 𝐷 𝑦 ) )
46 ge0nemnf ⊢ ( ( ( 𝑧 𝐷 𝑦 ) ∈ ℝ* ∧ 0 ≤ ( 𝑧 𝐷 𝑦 ) ) → ( 𝑧 𝐷 𝑦 ) ≠ -∞ )
47 42 45 46 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 𝐷 𝑦 ) ≠ -∞ )
48 47 a1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ¬ ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) → ( 𝑧 𝐷 𝑦 ) ≠ -∞ ) )
49 48 necon4bd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑧 𝐷 𝑦 ) = -∞ → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
50 49 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) → ( ( 𝑧 𝐷 𝑦 ) = -∞ → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
51 50 imp ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) ∧ ( 𝑧 𝐷 𝑦 ) = -∞ ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
52 42 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) → ( 𝑧 𝐷 𝑦 ) ∈ ℝ* )
53 elxr ⊢ ( ( 𝑧 𝐷 𝑦 ) ∈ ℝ* ↔ ( ( 𝑧 𝐷 𝑦 ) ∈ ℝ ∨ ( 𝑧 𝐷 𝑦 ) = +∞ ∨ ( 𝑧 𝐷 𝑦 ) = -∞ ) )
54 52 53 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) → ( ( 𝑧 𝐷 𝑦 ) ∈ ℝ ∨ ( 𝑧 𝐷 𝑦 ) = +∞ ∨ ( 𝑧 𝐷 𝑦 ) = -∞ ) )
55 16 38 51 54 mpjao3dan ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
56 19 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) = +∞ ) → ( 𝑥 𝐷 𝑦 ) ≤ +∞ )
57 oveq1 ⊢ ( ( 𝑧 𝐷 𝑥 ) = +∞ → ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = ( +∞ +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
58 xaddpnf2 ⊢ ( ( ( 𝑧 𝐷 𝑦 ) ∈ ℝ* ∧ ( 𝑧 𝐷 𝑦 ) ≠ -∞ ) → ( +∞ +𝑒 ( 𝑧 𝐷 𝑦 ) ) = +∞ )
59 42 47 58 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( +∞ +𝑒 ( 𝑧 𝐷 𝑦 ) ) = +∞ )
60 57 59 sylan9eqr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) = +∞ ) → ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = +∞ )
61 56 60 breqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) = +∞ ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
62 elxrge0 ⊢ ( ( 𝑧 𝐷 𝑥 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝑧 𝐷 𝑥 ) ) )
63 62 simprbi ⊢ ( ( 𝑧 𝐷 𝑥 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝑧 𝐷 𝑥 ) )
64 31 63 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 0 ≤ ( 𝑧 𝐷 𝑥 ) )
65 ge0nemnf ⊢ ( ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝑧 𝐷 𝑥 ) ) → ( 𝑧 𝐷 𝑥 ) ≠ -∞ )
66 33 64 65 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 𝐷 𝑥 ) ≠ -∞ )
67 66 a1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ¬ ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) → ( 𝑧 𝐷 𝑥 ) ≠ -∞ ) )
68 67 necon4bd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑧 𝐷 𝑥 ) = -∞ → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
69 68 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) = -∞ ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
70 elxr ⊢ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ* ↔ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∨ ( 𝑧 𝐷 𝑥 ) = +∞ ∨ ( 𝑧 𝐷 𝑥 ) = -∞ ) )
71 33 70 sylib ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∨ ( 𝑧 𝐷 𝑥 ) = +∞ ∨ ( 𝑧 𝐷 𝑥 ) = -∞ ) )
72 55 61 69 71 mpjao3dan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
73 1 2 11 72 isxmetd ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )