Theorem isxmet2d 15325

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	⊢ (𝜑 → 𝑋 ∈ V)
isxmetd.1	⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
isxmet2d.2	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (𝑥𝐷𝑦))
isxmet2d.3	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦))
isxmet2d.4	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))

Assertion

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

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

Proof of Theorem isxmet2d

Step	Hyp	Ref	Expression
1		isxmetd.0	. 2 ⊢ (𝜑 → 𝑋 ∈ V)
2		isxmetd.1	. 2 ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
3	2	fovcdmda 6206	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐷𝑦) ∈ ℝ*)
4		0xr 8336	. . . 4 ⊢ 0 ∈ ℝ*
5		xrletri3 10156	. . . 4 ⊢ (((𝑥𝐷𝑦) ∈ ℝ* ∧ 0 ∈ ℝ*) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
6	3, 4, 5	sylancl 413	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
7		isxmet2d.2	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (𝑥𝐷𝑦))
8	7	biantrud 304	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) ≤ 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
9		isxmet2d.3	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦))
10	6, 8, 9	3bitr2d 216	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))
11		isxmet2d.4	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
12	11	3expa 1230	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
13		rexadd 10204	. . . . . . 7 ⊢ (((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ) → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
14	13	adantl 277	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
15	12, 14	breqtrrd 4142	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
16	15	anassrs 400	. . . 4 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) ∈ ℝ) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
17	3	3adantr3 1185	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐷𝑦) ∈ ℝ*)
18		pnfge 10141	. . . . . . 7 ⊢ ((𝑥𝐷𝑦) ∈ ℝ* → (𝑥𝐷𝑦) ≤ +∞)
19	17, 18	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐷𝑦) ≤ +∞)
20	19	ad2antrr 488	. . . . 5 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) = +∞) → (𝑥𝐷𝑦) ≤ +∞)
21		oveq2 6066	. . . . . 6 ⊢ ((𝑧𝐷𝑦) = +∞ → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷𝑥) +𝑒 +∞))
22	2	ffnd 5514	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 Fn (𝑋 × 𝑋))
23		elxrge0 10330	. . . . . . . . . . . . 13 ⊢ ((𝑥𝐷𝑦) ∈ (0[,]+∞) ↔ ((𝑥𝐷𝑦) ∈ ℝ* ∧ 0 ≤ (𝑥𝐷𝑦)))
24	3, 7, 23	sylanbrc 417	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐷𝑦) ∈ (0[,]+∞))
25	24	ralrimivva 2626	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) ∈ (0[,]+∞))
26		ffnov 6165	. . . . . . . . . . 11 ⊢ (𝐷:(𝑋 × 𝑋)⟶(0[,]+∞) ↔ (𝐷 Fn (𝑋 × 𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) ∈ (0[,]+∞)))
27	22, 25, 26	sylanbrc 417	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
28	27	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
29		simpr3 1032	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑧 ∈ 𝑋)
30		simpr1 1030	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑥 ∈ 𝑋)
31	28, 29, 30	fovcdmd 6207	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧𝐷𝑥) ∈ (0[,]+∞))
32		elxrge0 10330	. . . . . . . . 9 ⊢ ((𝑧𝐷𝑥) ∈ (0[,]+∞) ↔ ((𝑧𝐷𝑥) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑥)))
33	32	simplbi 274	. . . . . . . 8 ⊢ ((𝑧𝐷𝑥) ∈ (0[,]+∞) → (𝑧𝐷𝑥) ∈ ℝ*)
34	31, 33	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧𝐷𝑥) ∈ ℝ*)
35		renemnf 8338	. . . . . . 7 ⊢ ((𝑧𝐷𝑥) ∈ ℝ → (𝑧𝐷𝑥) ≠ -∞)
36		xaddpnf1 10198	. . . . . . 7 ⊢ (((𝑧𝐷𝑥) ∈ ℝ* ∧ (𝑧𝐷𝑥) ≠ -∞) → ((𝑧𝐷𝑥) +𝑒 +∞) = +∞)
37	34, 35, 36	syl2an 289	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → ((𝑧𝐷𝑥) +𝑒 +∞) = +∞)
38	21, 37	sylan9eqr 2289	. . . . 5 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) = +∞) → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = +∞)
39	20, 38	breqtrrd 4142	. . . 4 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) = +∞) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
40		simpr2 1031	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑦 ∈ 𝑋)
41	28, 29, 40	fovcdmd 6207	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧𝐷𝑦) ∈ (0[,]+∞))
42		elxrge0 10330	. . . . . . . . . . 11 ⊢ ((𝑧𝐷𝑦) ∈ (0[,]+∞) ↔ ((𝑧𝐷𝑦) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑦)))
43	42	simplbi 274	. . . . . . . . . 10 ⊢ ((𝑧𝐷𝑦) ∈ (0[,]+∞) → (𝑧𝐷𝑦) ∈ ℝ*)
44	41, 43	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧𝐷𝑦) ∈ ℝ*)
45	42	simprbi 275	. . . . . . . . . 10 ⊢ ((𝑧𝐷𝑦) ∈ (0[,]+∞) → 0 ≤ (𝑧𝐷𝑦))
46	41, 45	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 0 ≤ (𝑧𝐷𝑦))
47		ge0nemnf 10176	. . . . . . . . 9 ⊢ (((𝑧𝐷𝑦) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑦)) → (𝑧𝐷𝑦) ≠ -∞)
48	44, 46, 47	syl2anc 411	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧𝐷𝑦) ≠ -∞)
49	48	neneqd 2435	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ¬ (𝑧𝐷𝑦) = -∞)
50	49	pm2.21d 624	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑧𝐷𝑦) = -∞ → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))
51	50	adantr 276	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → ((𝑧𝐷𝑦) = -∞ → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))
52	51	imp 124	. . . 4 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) = -∞) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
53	44	adantr 276	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → (𝑧𝐷𝑦) ∈ ℝ*)
54		elxr 10128	. . . . 5 ⊢ ((𝑧𝐷𝑦) ∈ ℝ* ↔ ((𝑧𝐷𝑦) ∈ ℝ ∨ (𝑧𝐷𝑦) = +∞ ∨ (𝑧𝐷𝑦) = -∞))
55	53, 54	sylib 122	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → ((𝑧𝐷𝑦) ∈ ℝ ∨ (𝑧𝐷𝑦) = +∞ ∨ (𝑧𝐷𝑦) = -∞))
56	16, 39, 52, 55	mpjao3dan 1344	. . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
57	19	adantr 276	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) = +∞) → (𝑥𝐷𝑦) ≤ +∞)
58		oveq1 6065	. . . . 5 ⊢ ((𝑧𝐷𝑥) = +∞ → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = (+∞ +𝑒 (𝑧𝐷𝑦)))
59		xaddpnf2 10199	. . . . . 6 ⊢ (((𝑧𝐷𝑦) ∈ ℝ* ∧ (𝑧𝐷𝑦) ≠ -∞) → (+∞ +𝑒 (𝑧𝐷𝑦)) = +∞)
60	44, 48, 59	syl2anc 411	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (+∞ +𝑒 (𝑧𝐷𝑦)) = +∞)
61	58, 60	sylan9eqr 2289	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) = +∞) → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = +∞)
62	57, 61	breqtrrd 4142	. . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) = +∞) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
63	32	simprbi 275	. . . . . . . 8 ⊢ ((𝑧𝐷𝑥) ∈ (0[,]+∞) → 0 ≤ (𝑧𝐷𝑥))
64	31, 63	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 0 ≤ (𝑧𝐷𝑥))
65		ge0nemnf 10176	. . . . . . 7 ⊢ (((𝑧𝐷𝑥) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑥)) → (𝑧𝐷𝑥) ≠ -∞)
66	34, 64, 65	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧𝐷𝑥) ≠ -∞)
67	66	neneqd 2435	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ¬ (𝑧𝐷𝑥) = -∞)
68	67	pm2.21d 624	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑧𝐷𝑥) = -∞ → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))
69	68	imp 124	. . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷𝑥) = -∞) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
70		elxr 10128	. . . 4 ⊢ ((𝑧𝐷𝑥) ∈ ℝ* ↔ ((𝑧𝐷𝑥) ∈ ℝ ∨ (𝑧𝐷𝑥) = +∞ ∨ (𝑧𝐷𝑥) = -∞))
71	34, 70	sylib 122	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑧𝐷𝑥) ∈ ℝ ∨ (𝑧𝐷𝑥) = +∞ ∨ (𝑧𝐷𝑥) = -∞))
72	56, 62, 69, 71	mpjao3dan 1344	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
73	1, 2, 10, 72	isxmetd 15324	1 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∨ w3o 1004   ∧ w3a 1005   = wceq 1398   ∈ wcel 2205   ≠ wne 2414  ∀wral 2522  Vcvv 2815   class class class wbr 4114   × cxp 4752   Fn wfn 5352  ⟶wf 5353  ‘cfv 5357  (class class class)co 6058  ℝcr 8142  0cc0 8143   + caddc 8146  +∞cpnf 8321  -∞cmnf 8322  ℝ^*cxr 8323   ≤ cle 8325   +_𝑒 cxad 10122  [,]cicc 10243  ∞Metcxmet 14796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327  ax-un 4559  ax-setind 4664  ax-cnex 8234  ax-resscn 8235  ax-1re 8237  ax-addrcl 8240  ax-rnegex 8252  ax-pre-ltirr 8255  ax-pre-ltwlin 8256  ax-pre-lttrn 8257  ax-pre-apti 8258

This theorem depends on definitions:  df-bi 117  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-nel 2510  df-ral 2527  df-rex 2528  df-rab 2531  df-v 2817  df-sbc 3046  df-csb 3142  df-dif 3216  df-un 3218  df-in 3220  df-ss 3227  df-if 3625  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-iun 3998  df-br 4115  df-opab 4177  df-mpt 4178  df-id 4419  df-po 4422  df-iso 4423  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-rn 4765  df-res 4766  df-ima 4767  df-iota 5317  df-fun 5359  df-fn 5360  df-f 5361  df-fv 5365  df-ov 6061  df-oprab 6062  df-mpo 6063  df-1st 6347  df-2nd 6348  df-map 6897  df-pnf 8326  df-mnf 8327  df-xr 8328  df-ltxr 8329  df-le 8330  df-xadd 10125  df-icc 10247  df-xmet 14804

This theorem is referenced by: (None)