Theorem isxmet2d 24222

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: 𝐷(𝑥, 𝑦) = if(𝑥 = 𝑦, 0, -∞) satisfies all hypotheses except nonnegativity.) (Contributed by Mario Carneiro, 20-Aug-2015.)

Hypotheses

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

Assertion

Ref	Expression
isxmet2d	⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))

Distinct variable groups:   𝑥,𝑦,𝑧,𝐷   𝜑,𝑥,𝑦,𝑧   𝑥,𝑋,𝑦,𝑧

Allowed substitution hints:   𝑉(𝑥,𝑦,𝑧)

Proof of Theorem isxmet2d

Step	Hyp	Ref	Expression
1		isxmetd.0	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
2		isxmetd.1	. 2 ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
3	2	fovcdmda 7563	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐷𝑦) ∈ ℝ*)
4		0xr 11228	. . . 4 ⊢ 0 ∈ ℝ*
5		xrletri3 13121	. . . 4 ⊢ (((𝑥𝐷𝑦) ∈ ℝ* ∧ 0 ∈ ℝ*) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
6	3, 4, 5	sylancl 586	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
7		isxmet2d.2	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (𝑥𝐷𝑦))
8	7	biantrud 531	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) ≤ 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
9		isxmet2d.3	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦))
10	6, 8, 9	3bitr2d 307	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))
11		isxmet2d.4	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
12	11	3expa 1118	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
13		rexadd 13199	. . . . . . 7 ⊢ (((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ) → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
14	13	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
15	12, 14	breqtrrd 5138	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
16	15	anassrs 467	. . . 4 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) ∈ ℝ) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
17	3	3adantr3 1172	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐷𝑦) ∈ ℝ*)
18		pnfge 13097	. . . . . . 7 ⊢ ((𝑥𝐷𝑦) ∈ ℝ* → (𝑥𝐷𝑦) ≤ +∞)
19	17, 18	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐷𝑦) ≤ +∞)
20	19	ad2antrr 726	. . . . 5 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) = +∞) → (𝑥𝐷𝑦) ≤ +∞)
21		oveq2 7398	. . . . . 6 ⊢ ((𝑧𝐷𝑦) = +∞ → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷𝑥) +𝑒 +∞))
22	2	ffnd 6692	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 Fn (𝑋 × 𝑋))
23		elxrge0 13425	. . . . . . . . . . . . 13 ⊢ ((𝑥𝐷𝑦) ∈ (0[,]+∞) ↔ ((𝑥𝐷𝑦) ∈ ℝ* ∧ 0 ≤ (𝑥𝐷𝑦)))
24	3, 7, 23	sylanbrc 583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐷𝑦) ∈ (0[,]+∞))
25	24	ralrimivva 3181	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) ∈ (0[,]+∞))
26		ffnov 7518	. . . . . . . . . . 11 ⊢ (𝐷:(𝑋 × 𝑋)⟶(0[,]+∞) ↔ (𝐷 Fn (𝑋 × 𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) ∈ (0[,]+∞)))
27	22, 25, 26	sylanbrc 583	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
28	27	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
29		simpr3 1197	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑧 ∈ 𝑋)
30		simpr1 1195	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑥 ∈ 𝑋)
31	28, 29, 30	fovcdmd 7564	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧𝐷𝑥) ∈ (0[,]+∞))
32		eliccxr 13403	. . . . . . . 8 ⊢ ((𝑧𝐷𝑥) ∈ (0[,]+∞) → (𝑧𝐷𝑥) ∈ ℝ*)
33	31, 32	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧𝐷𝑥) ∈ ℝ*)
34		renemnf 11230	. . . . . . 7 ⊢ ((𝑧𝐷𝑥) ∈ ℝ → (𝑧𝐷𝑥) ≠ -∞)
35		xaddpnf1 13193	. . . . . . 7 ⊢ (((𝑧𝐷𝑥) ∈ ℝ* ∧ (𝑧𝐷𝑥) ≠ -∞) → ((𝑧𝐷𝑥) +𝑒 +∞) = +∞)
36	33, 34, 35	syl2an 596	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → ((𝑧𝐷𝑥) +𝑒 +∞) = +∞)
37	21, 36	sylan9eqr 2787	. . . . 5 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) = +∞) → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = +∞)
38	20, 37	breqtrrd 5138	. . . 4 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) = +∞) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
39		simpr2 1196	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑦 ∈ 𝑋)
40	28, 29, 39	fovcdmd 7564	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧𝐷𝑦) ∈ (0[,]+∞))
41		eliccxr 13403	. . . . . . . . . 10 ⊢ ((𝑧𝐷𝑦) ∈ (0[,]+∞) → (𝑧𝐷𝑦) ∈ ℝ*)
42	40, 41	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧𝐷𝑦) ∈ ℝ*)
43		elxrge0 13425	. . . . . . . . . . 11 ⊢ ((𝑧𝐷𝑦) ∈ (0[,]+∞) ↔ ((𝑧𝐷𝑦) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑦)))
44	43	simprbi 496	. . . . . . . . . 10 ⊢ ((𝑧𝐷𝑦) ∈ (0[,]+∞) → 0 ≤ (𝑧𝐷𝑦))
45	40, 44	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 0 ≤ (𝑧𝐷𝑦))
46		ge0nemnf 13140	. . . . . . . . 9 ⊢ (((𝑧𝐷𝑦) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑦)) → (𝑧𝐷𝑦) ≠ -∞)
47	42, 45, 46	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧𝐷𝑦) ≠ -∞)
48	47	a1d 25	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (¬ (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) → (𝑧𝐷𝑦) ≠ -∞))
49	48	necon4bd 2946	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑧𝐷𝑦) = -∞ → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))
50	49	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → ((𝑧𝐷𝑦) = -∞ → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))
51	50	imp 406	. . . 4 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) = -∞) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
52	42	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → (𝑧𝐷𝑦) ∈ ℝ*)
53		elxr 13083	. . . . 5 ⊢ ((𝑧𝐷𝑦) ∈ ℝ* ↔ ((𝑧𝐷𝑦) ∈ ℝ ∨ (𝑧𝐷𝑦) = +∞ ∨ (𝑧𝐷𝑦) = -∞))
54	52, 53	sylib 218	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → ((𝑧𝐷𝑦) ∈ ℝ ∨ (𝑧𝐷𝑦) = +∞ ∨ (𝑧𝐷𝑦) = -∞))
55	16, 38, 51, 54	mpjao3dan 1434	. . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
56	19	adantr 480	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) = +∞) → (𝑥𝐷𝑦) ≤ +∞)
57		oveq1 7397	. . . . 5 ⊢ ((𝑧𝐷𝑥) = +∞ → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = (+∞ +𝑒 (𝑧𝐷𝑦)))
58		xaddpnf2 13194	. . . . . 6 ⊢ (((𝑧𝐷𝑦) ∈ ℝ* ∧ (𝑧𝐷𝑦) ≠ -∞) → (+∞ +𝑒 (𝑧𝐷𝑦)) = +∞)
59	42, 47, 58	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (+∞ +𝑒 (𝑧𝐷𝑦)) = +∞)
60	57, 59	sylan9eqr 2787	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) = +∞) → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = +∞)
61	56, 60	breqtrrd 5138	. . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) = +∞) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
62		elxrge0 13425	. . . . . . . . 9 ⊢ ((𝑧𝐷𝑥) ∈ (0[,]+∞) ↔ ((𝑧𝐷𝑥) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑥)))
63	62	simprbi 496	. . . . . . . 8 ⊢ ((𝑧𝐷𝑥) ∈ (0[,]+∞) → 0 ≤ (𝑧𝐷𝑥))
64	31, 63	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 0 ≤ (𝑧𝐷𝑥))
65		ge0nemnf 13140	. . . . . . 7 ⊢ (((𝑧𝐷𝑥) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑥)) → (𝑧𝐷𝑥) ≠ -∞)
66	33, 64, 65	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧𝐷𝑥) ≠ -∞)
67	66	a1d 25	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (¬ (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) → (𝑧𝐷𝑥) ≠ -∞))
68	67	necon4bd 2946	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑧𝐷𝑥) = -∞ → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))
69	68	imp 406	. . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) = -∞) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
70		elxr 13083	. . . 4 ⊢ ((𝑧𝐷𝑥) ∈ ℝ* ↔ ((𝑧𝐷𝑥) ∈ ℝ ∨ (𝑧𝐷𝑥) = +∞ ∨ (𝑧𝐷𝑥) = -∞))
71	33, 70	sylib 218	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑧𝐷𝑥) ∈ ℝ ∨ (𝑧𝐷𝑥) = +∞ ∨ (𝑧𝐷𝑥) = -∞))
72	55, 61, 69, 71	mpjao3dan 1434	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
73	1, 2, 10, 72	isxmetd 24221	1 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ w3o 1085   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2926  ∀wral 3045   class class class wbr 5110   × cxp 5639   Fn wfn 6509  ⟶wf 6510  ‘cfv 6514  (class class class)co 7390  ℝcr 11074  0cc0 11075   + caddc 11078  +∞cpnf 11212  -∞cmnf 11213  ℝ^*cxr 11214   ≤ cle 11216   +_𝑒 cxad 13077  [,]cicc 13316  ∞Metcxmet 21256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-i2m1 11143  ax-rnegex 11146  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-1st 7971  df-2nd 7972  df-er 8674  df-map 8804  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-xadd 13080  df-icc 13320  df-xmet 21264

This theorem is referenced by:  prdsxmetlem  24263  xrsxmet  24705