MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isxmet2d Structured version   Visualization version   GIF version

Theorem isxmet2d 23602
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
StepHypRef Expression
1 isxmetd.0 . 2 (πœ‘ β†’ 𝑋 ∈ 𝑉)
2 isxmetd.1 . 2 (πœ‘ β†’ 𝐷:(𝑋 Γ— 𝑋)βŸΆβ„*)
32fovcdmda 7517 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (π‘₯𝐷𝑦) ∈ ℝ*)
4 0xr 11135 . . . 4 0 ∈ ℝ*
5 xrletri3 13001 . . . 4 (((π‘₯𝐷𝑦) ∈ ℝ* ∧ 0 ∈ ℝ*) β†’ ((π‘₯𝐷𝑦) = 0 ↔ ((π‘₯𝐷𝑦) ≀ 0 ∧ 0 ≀ (π‘₯𝐷𝑦))))
63, 4, 5sylancl 586 . . 3 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ ((π‘₯𝐷𝑦) = 0 ↔ ((π‘₯𝐷𝑦) ≀ 0 ∧ 0 ≀ (π‘₯𝐷𝑦))))
7 isxmet2d.2 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ 0 ≀ (π‘₯𝐷𝑦))
87biantrud 532 . . 3 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ ((π‘₯𝐷𝑦) ≀ 0 ↔ ((π‘₯𝐷𝑦) ≀ 0 ∧ 0 ≀ (π‘₯𝐷𝑦))))
9 isxmet2d.3 . . 3 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ ((π‘₯𝐷𝑦) ≀ 0 ↔ π‘₯ = 𝑦))
106, 8, 93bitr2d 306 . 2 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ ((π‘₯𝐷𝑦) = 0 ↔ π‘₯ = 𝑦))
11 isxmet2d.4 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ ((𝑧𝐷π‘₯) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) β†’ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) + (𝑧𝐷𝑦)))
12113expa 1118 . . . . . 6 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ ((𝑧𝐷π‘₯) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) β†’ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) + (𝑧𝐷𝑦)))
13 rexadd 13079 . . . . . . 7 (((𝑧𝐷π‘₯) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ) β†’ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷π‘₯) + (𝑧𝐷𝑦)))
1413adantl 482 . . . . . 6 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ ((𝑧𝐷π‘₯) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) β†’ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷π‘₯) + (𝑧𝐷𝑦)))
1512, 14breqtrrd 5131 . . . . 5 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ ((𝑧𝐷π‘₯) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) β†’ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)))
1615anassrs 468 . . . 4 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷π‘₯) ∈ ℝ) ∧ (𝑧𝐷𝑦) ∈ ℝ) β†’ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)))
1733adantr3 1171 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ (π‘₯𝐷𝑦) ∈ ℝ*)
18 pnfge 12979 . . . . . . 7 ((π‘₯𝐷𝑦) ∈ ℝ* β†’ (π‘₯𝐷𝑦) ≀ +∞)
1917, 18syl 17 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ (π‘₯𝐷𝑦) ≀ +∞)
2019ad2antrr 724 . . . . 5 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷π‘₯) ∈ ℝ) ∧ (𝑧𝐷𝑦) = +∞) β†’ (π‘₯𝐷𝑦) ≀ +∞)
21 oveq2 7357 . . . . . 6 ((𝑧𝐷𝑦) = +∞ β†’ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷π‘₯) +𝑒 +∞))
222ffnd 6664 . . . . . . . . . . 11 (πœ‘ β†’ 𝐷 Fn (𝑋 Γ— 𝑋))
23 elxrge0 13302 . . . . . . . . . . . . 13 ((π‘₯𝐷𝑦) ∈ (0[,]+∞) ↔ ((π‘₯𝐷𝑦) ∈ ℝ* ∧ 0 ≀ (π‘₯𝐷𝑦)))
243, 7, 23sylanbrc 583 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (π‘₯𝐷𝑦) ∈ (0[,]+∞))
2524ralrimivva 3195 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 (π‘₯𝐷𝑦) ∈ (0[,]+∞))
26 ffnov 7475 . . . . . . . . . . 11 (𝐷:(𝑋 Γ— 𝑋)⟢(0[,]+∞) ↔ (𝐷 Fn (𝑋 Γ— 𝑋) ∧ βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 (π‘₯𝐷𝑦) ∈ (0[,]+∞)))
2722, 25, 26sylanbrc 583 . . . . . . . . . 10 (πœ‘ β†’ 𝐷:(𝑋 Γ— 𝑋)⟢(0[,]+∞))
2827adantr 481 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ 𝐷:(𝑋 Γ— 𝑋)⟢(0[,]+∞))
29 simpr3 1196 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ 𝑧 ∈ 𝑋)
30 simpr1 1194 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ π‘₯ ∈ 𝑋)
3128, 29, 30fovcdmd 7518 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ (𝑧𝐷π‘₯) ∈ (0[,]+∞))
32 eliccxr 13280 . . . . . . . 8 ((𝑧𝐷π‘₯) ∈ (0[,]+∞) β†’ (𝑧𝐷π‘₯) ∈ ℝ*)
3331, 32syl 17 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ (𝑧𝐷π‘₯) ∈ ℝ*)
34 renemnf 11137 . . . . . . 7 ((𝑧𝐷π‘₯) ∈ ℝ β†’ (𝑧𝐷π‘₯) β‰  -∞)
35 xaddpnf1 13073 . . . . . . 7 (((𝑧𝐷π‘₯) ∈ ℝ* ∧ (𝑧𝐷π‘₯) β‰  -∞) β†’ ((𝑧𝐷π‘₯) +𝑒 +∞) = +∞)
3633, 34, 35syl2an 596 . . . . . 6 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷π‘₯) ∈ ℝ) β†’ ((𝑧𝐷π‘₯) +𝑒 +∞) = +∞)
3721, 36sylan9eqr 2799 . . . . 5 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷π‘₯) ∈ ℝ) ∧ (𝑧𝐷𝑦) = +∞) β†’ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)) = +∞)
3820, 37breqtrrd 5131 . . . 4 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷π‘₯) ∈ ℝ) ∧ (𝑧𝐷𝑦) = +∞) β†’ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)))
39 simpr2 1195 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ 𝑦 ∈ 𝑋)
4028, 29, 39fovcdmd 7518 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ (𝑧𝐷𝑦) ∈ (0[,]+∞))
41 eliccxr 13280 . . . . . . . . . 10 ((𝑧𝐷𝑦) ∈ (0[,]+∞) β†’ (𝑧𝐷𝑦) ∈ ℝ*)
4240, 41syl 17 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ (𝑧𝐷𝑦) ∈ ℝ*)
43 elxrge0 13302 . . . . . . . . . . 11 ((𝑧𝐷𝑦) ∈ (0[,]+∞) ↔ ((𝑧𝐷𝑦) ∈ ℝ* ∧ 0 ≀ (𝑧𝐷𝑦)))
4443simprbi 497 . . . . . . . . . 10 ((𝑧𝐷𝑦) ∈ (0[,]+∞) β†’ 0 ≀ (𝑧𝐷𝑦))
4540, 44syl 17 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ 0 ≀ (𝑧𝐷𝑦))
46 ge0nemnf 13020 . . . . . . . . 9 (((𝑧𝐷𝑦) ∈ ℝ* ∧ 0 ≀ (𝑧𝐷𝑦)) β†’ (𝑧𝐷𝑦) β‰  -∞)
4742, 45, 46syl2anc 584 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ (𝑧𝐷𝑦) β‰  -∞)
4847a1d 25 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ (Β¬ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)) β†’ (𝑧𝐷𝑦) β‰  -∞))
4948necon4bd 2961 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ ((𝑧𝐷𝑦) = -∞ β†’ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦))))
5049adantr 481 . . . . 5 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷π‘₯) ∈ ℝ) β†’ ((𝑧𝐷𝑦) = -∞ β†’ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦))))
5150imp 407 . . . 4 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷π‘₯) ∈ ℝ) ∧ (𝑧𝐷𝑦) = -∞) β†’ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)))
5242adantr 481 . . . . 5 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷π‘₯) ∈ ℝ) β†’ (𝑧𝐷𝑦) ∈ ℝ*)
53 elxr 12965 . . . . 5 ((𝑧𝐷𝑦) ∈ ℝ* ↔ ((𝑧𝐷𝑦) ∈ ℝ ∨ (𝑧𝐷𝑦) = +∞ ∨ (𝑧𝐷𝑦) = -∞))
5452, 53sylib 217 . . . 4 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷π‘₯) ∈ ℝ) β†’ ((𝑧𝐷𝑦) ∈ ℝ ∨ (𝑧𝐷𝑦) = +∞ ∨ (𝑧𝐷𝑦) = -∞))
5516, 38, 51, 54mpjao3dan 1431 . . 3 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷π‘₯) ∈ ℝ) β†’ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)))
5619adantr 481 . . . 4 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷π‘₯) = +∞) β†’ (π‘₯𝐷𝑦) ≀ +∞)
57 oveq1 7356 . . . . 5 ((𝑧𝐷π‘₯) = +∞ β†’ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)) = (+∞ +𝑒 (𝑧𝐷𝑦)))
58 xaddpnf2 13074 . . . . . 6 (((𝑧𝐷𝑦) ∈ ℝ* ∧ (𝑧𝐷𝑦) β‰  -∞) β†’ (+∞ +𝑒 (𝑧𝐷𝑦)) = +∞)
5942, 47, 58syl2anc 584 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ (+∞ +𝑒 (𝑧𝐷𝑦)) = +∞)
6057, 59sylan9eqr 2799 . . . 4 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷π‘₯) = +∞) β†’ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)) = +∞)
6156, 60breqtrrd 5131 . . 3 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷π‘₯) = +∞) β†’ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)))
62 elxrge0 13302 . . . . . . . . 9 ((𝑧𝐷π‘₯) ∈ (0[,]+∞) ↔ ((𝑧𝐷π‘₯) ∈ ℝ* ∧ 0 ≀ (𝑧𝐷π‘₯)))
6362simprbi 497 . . . . . . . 8 ((𝑧𝐷π‘₯) ∈ (0[,]+∞) β†’ 0 ≀ (𝑧𝐷π‘₯))
6431, 63syl 17 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ 0 ≀ (𝑧𝐷π‘₯))
65 ge0nemnf 13020 . . . . . . 7 (((𝑧𝐷π‘₯) ∈ ℝ* ∧ 0 ≀ (𝑧𝐷π‘₯)) β†’ (𝑧𝐷π‘₯) β‰  -∞)
6633, 64, 65syl2anc 584 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ (𝑧𝐷π‘₯) β‰  -∞)
6766a1d 25 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ (Β¬ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)) β†’ (𝑧𝐷π‘₯) β‰  -∞))
6867necon4bd 2961 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ ((𝑧𝐷π‘₯) = -∞ β†’ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦))))
6968imp 407 . . 3 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (𝑧𝐷π‘₯) = -∞) β†’ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)))
70 elxr 12965 . . . 4 ((𝑧𝐷π‘₯) ∈ ℝ* ↔ ((𝑧𝐷π‘₯) ∈ ℝ ∨ (𝑧𝐷π‘₯) = +∞ ∨ (𝑧𝐷π‘₯) = -∞))
7133, 70sylib 217 . . 3 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ ((𝑧𝐷π‘₯) ∈ ℝ ∨ (𝑧𝐷π‘₯) = +∞ ∨ (𝑧𝐷π‘₯) = -∞))
7255, 61, 69, 71mpjao3dan 1431 . 2 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) +𝑒 (𝑧𝐷𝑦)))
731, 2, 10, 72isxmetd 23601 1 (πœ‘ β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ w3o 1086   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2941  βˆ€wral 3062   class class class wbr 5103   Γ— cxp 5628   Fn wfn 6486  βŸΆwf 6487  β€˜cfv 6491  (class class class)co 7349  β„cr 10983  0cc0 10984   + caddc 10987  +∞cpnf 11119  -∞cmnf 11120  β„*cxr 11121   ≀ cle 11123   +𝑒 cxad 12959  [,]cicc 13195  βˆžMetcxmet 20704
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7662  ax-cnex 11040  ax-resscn 11041  ax-1cn 11042  ax-icn 11043  ax-addcl 11044  ax-addrcl 11045  ax-mulcl 11046  ax-i2m1 11052  ax-rnegex 11055  ax-cnre 11057  ax-pre-lttri 11058  ax-pre-lttrn 11059
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-id 5528  df-po 5542  df-so 5543  df-xp 5636  df-rel 5637  df-cnv 5638  df-co 5639  df-dm 5640  df-rn 5641  df-res 5642  df-ima 5643  df-iota 6443  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-ov 7352  df-oprab 7353  df-mpo 7354  df-1st 7911  df-2nd 7912  df-er 8581  df-map 8700  df-en 8817  df-dom 8818  df-sdom 8819  df-pnf 11124  df-mnf 11125  df-xr 11126  df-ltxr 11127  df-le 11128  df-xadd 12962  df-icc 13199  df-xmet 20712
This theorem is referenced by:  prdsxmetlem  23643  xrsxmet  24094
  Copyright terms: Public domain W3C validator