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	fovcdmda	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ^* )
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	fovcdmd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 𝐷 𝑥 ) ∈ ( 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	fovcdmd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 𝐷 𝑦 ) ∈ ( 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 ‘ 𝑋 ) )

Metamath Proof Explorer

Theorem isxmet2d

Proof