# Metamath Proof Explorer

## Theorem stdbdxmet

Description: The standard bounded metric is an extended metric given an extended metric and a positive extended real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypothesis stdbdmet.1 ${⊢}{D}=\left({x}\in {X},{y}\in {X}⟼if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\right)$
Assertion stdbdxmet ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 stdbdmet.1 ${⊢}{D}=\left({x}\in {X},{y}\in {X}⟼if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\right)$
2 simp1 ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to {C}\in \mathrm{\infty Met}\left({X}\right)$
3 xmetcl ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\wedge {y}\in {X}\right)\to {x}{C}{y}\in {ℝ}^{*}$
4 xmetge0 ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\wedge {y}\in {X}\right)\to 0\le {x}{C}{y}$
5 elxrge0 ${⊢}{x}{C}{y}\in \left[0,\mathrm{+\infty }\right]↔\left({x}{C}{y}\in {ℝ}^{*}\wedge 0\le {x}{C}{y}\right)$
6 3 4 5 sylanbrc ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\wedge {y}\in {X}\right)\to {x}{C}{y}\in \left[0,\mathrm{+\infty }\right]$
7 6 3expb ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{C}{y}\in \left[0,\mathrm{+\infty }\right]$
8 2 7 sylan ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{C}{y}\in \left[0,\mathrm{+\infty }\right]$
9 xmetf ${⊢}{C}\in \mathrm{\infty Met}\left({X}\right)\to {C}:{X}×{X}⟶{ℝ}^{*}$
10 9 3ad2ant1 ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to {C}:{X}×{X}⟶{ℝ}^{*}$
11 10 ffnd ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to {C}Fn\left({X}×{X}\right)$
12 fnov ${⊢}{C}Fn\left({X}×{X}\right)↔{C}=\left({x}\in {X},{y}\in {X}⟼{x}{C}{y}\right)$
13 11 12 sylib ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to {C}=\left({x}\in {X},{y}\in {X}⟼{x}{C}{y}\right)$
14 eqidd ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)=\left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)$
15 breq1 ${⊢}{z}={x}{C}{y}\to \left({z}\le {R}↔{x}{C}{y}\le {R}\right)$
16 id ${⊢}{z}={x}{C}{y}\to {z}={x}{C}{y}$
17 15 16 ifbieq1d ${⊢}{z}={x}{C}{y}\to if\left({z}\le {R},{z},{R}\right)=if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)$
18 8 13 14 17 fmpoco ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\circ {C}=\left({x}\in {X},{y}\in {X}⟼if\left({x}{C}{y}\le {R},{x}{C}{y},{R}\right)\right)$
19 18 1 syl6eqr ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\circ {C}={D}$
20 eliccxr ${⊢}{z}\in \left[0,\mathrm{+\infty }\right]\to {z}\in {ℝ}^{*}$
21 simp2 ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to {R}\in {ℝ}^{*}$
22 ifcl ${⊢}\left({z}\in {ℝ}^{*}\wedge {R}\in {ℝ}^{*}\right)\to if\left({z}\le {R},{z},{R}\right)\in {ℝ}^{*}$
23 20 21 22 syl2anr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge {z}\in \left[0,\mathrm{+\infty }\right]\right)\to if\left({z}\le {R},{z},{R}\right)\in {ℝ}^{*}$
24 23 fmpttd ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right):\left[0,\mathrm{+\infty }\right]⟶{ℝ}^{*}$
25 id ${⊢}{a}\in \left[0,\mathrm{+\infty }\right]\to {a}\in \left[0,\mathrm{+\infty }\right]$
26 vex ${⊢}{a}\in \mathrm{V}$
27 ifexg ${⊢}\left({a}\in \mathrm{V}\wedge {R}\in {ℝ}^{*}\right)\to if\left({a}\le {R},{a},{R}\right)\in \mathrm{V}$
28 26 21 27 sylancr ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to if\left({a}\le {R},{a},{R}\right)\in \mathrm{V}$
29 breq1 ${⊢}{z}={a}\to \left({z}\le {R}↔{a}\le {R}\right)$
30 id ${⊢}{z}={a}\to {z}={a}$
31 29 30 ifbieq1d ${⊢}{z}={a}\to if\left({z}\le {R},{z},{R}\right)=if\left({a}\le {R},{a},{R}\right)$
32 eqid ${⊢}\left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)=\left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)$
33 31 32 fvmptg ${⊢}\left({a}\in \left[0,\mathrm{+\infty }\right]\wedge if\left({a}\le {R},{a},{R}\right)\in \mathrm{V}\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({a}\right)=if\left({a}\le {R},{a},{R}\right)$
34 25 28 33 syl2anr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge {a}\in \left[0,\mathrm{+\infty }\right]\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({a}\right)=if\left({a}\le {R},{a},{R}\right)$
35 34 eqeq1d ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge {a}\in \left[0,\mathrm{+\infty }\right]\right)\to \left(\left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({a}\right)=0↔if\left({a}\le {R},{a},{R}\right)=0\right)$
36 eqeq1 ${⊢}{a}=if\left({a}\le {R},{a},{R}\right)\to \left({a}=0↔if\left({a}\le {R},{a},{R}\right)=0\right)$
37 36 bibi1d ${⊢}{a}=if\left({a}\le {R},{a},{R}\right)\to \left(\left({a}=0↔{a}=0\right)↔\left(if\left({a}\le {R},{a},{R}\right)=0↔{a}=0\right)\right)$
38 eqeq1 ${⊢}{R}=if\left({a}\le {R},{a},{R}\right)\to \left({R}=0↔if\left({a}\le {R},{a},{R}\right)=0\right)$
39 38 bibi1d ${⊢}{R}=if\left({a}\le {R},{a},{R}\right)\to \left(\left({R}=0↔{a}=0\right)↔\left(if\left({a}\le {R},{a},{R}\right)=0↔{a}=0\right)\right)$
40 biidd ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge {a}\in \left[0,\mathrm{+\infty }\right]\right)\wedge {a}\le {R}\right)\to \left({a}=0↔{a}=0\right)$
41 simp3 ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to 0<{R}$
42 41 gt0ne0d ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to {R}\ne 0$
43 42 neneqd ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to ¬{R}=0$
44 43 ad2antrr ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge {a}\in \left[0,\mathrm{+\infty }\right]\right)\wedge ¬{a}\le {R}\right)\to ¬{R}=0$
45 0xr ${⊢}0\in {ℝ}^{*}$
46 xrltle ${⊢}\left(0\in {ℝ}^{*}\wedge {R}\in {ℝ}^{*}\right)\to \left(0<{R}\to 0\le {R}\right)$
47 45 21 46 sylancr ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to \left(0<{R}\to 0\le {R}\right)$
48 41 47 mpd ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to 0\le {R}$
49 48 adantr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge {a}\in \left[0,\mathrm{+\infty }\right]\right)\to 0\le {R}$
50 breq1 ${⊢}{a}=0\to \left({a}\le {R}↔0\le {R}\right)$
51 49 50 syl5ibrcom ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge {a}\in \left[0,\mathrm{+\infty }\right]\right)\to \left({a}=0\to {a}\le {R}\right)$
52 51 con3dimp ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge {a}\in \left[0,\mathrm{+\infty }\right]\right)\wedge ¬{a}\le {R}\right)\to ¬{a}=0$
53 44 52 2falsed ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge {a}\in \left[0,\mathrm{+\infty }\right]\right)\wedge ¬{a}\le {R}\right)\to \left({R}=0↔{a}=0\right)$
54 37 39 40 53 ifbothda ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge {a}\in \left[0,\mathrm{+\infty }\right]\right)\to \left(if\left({a}\le {R},{a},{R}\right)=0↔{a}=0\right)$
55 35 54 bitrd ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge {a}\in \left[0,\mathrm{+\infty }\right]\right)\to \left(\left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({a}\right)=0↔{a}=0\right)$
56 eliccxr ${⊢}{a}\in \left[0,\mathrm{+\infty }\right]\to {a}\in {ℝ}^{*}$
57 56 ad2antrl ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to {a}\in {ℝ}^{*}$
58 21 adantr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to {R}\in {ℝ}^{*}$
59 xrmin1 ${⊢}\left({a}\in {ℝ}^{*}\wedge {R}\in {ℝ}^{*}\right)\to if\left({a}\le {R},{a},{R}\right)\le {a}$
60 57 58 59 syl2anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to if\left({a}\le {R},{a},{R}\right)\le {a}$
61 57 58 ifcld ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to if\left({a}\le {R},{a},{R}\right)\in {ℝ}^{*}$
62 eliccxr ${⊢}{b}\in \left[0,\mathrm{+\infty }\right]\to {b}\in {ℝ}^{*}$
63 62 ad2antll ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to {b}\in {ℝ}^{*}$
64 xrletr ${⊢}\left(if\left({a}\le {R},{a},{R}\right)\in {ℝ}^{*}\wedge {a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\to \left(\left(if\left({a}\le {R},{a},{R}\right)\le {a}\wedge {a}\le {b}\right)\to if\left({a}\le {R},{a},{R}\right)\le {b}\right)$
65 61 57 63 64 syl3anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to \left(\left(if\left({a}\le {R},{a},{R}\right)\le {a}\wedge {a}\le {b}\right)\to if\left({a}\le {R},{a},{R}\right)\le {b}\right)$
66 60 65 mpand ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to \left({a}\le {b}\to if\left({a}\le {R},{a},{R}\right)\le {b}\right)$
67 xrmin2 ${⊢}\left({a}\in {ℝ}^{*}\wedge {R}\in {ℝ}^{*}\right)\to if\left({a}\le {R},{a},{R}\right)\le {R}$
68 57 58 67 syl2anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to if\left({a}\le {R},{a},{R}\right)\le {R}$
69 66 68 jctird ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to \left({a}\le {b}\to \left(if\left({a}\le {R},{a},{R}\right)\le {b}\wedge if\left({a}\le {R},{a},{R}\right)\le {R}\right)\right)$
70 xrlemin ${⊢}\left(if\left({a}\le {R},{a},{R}\right)\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\wedge {R}\in {ℝ}^{*}\right)\to \left(if\left({a}\le {R},{a},{R}\right)\le if\left({b}\le {R},{b},{R}\right)↔\left(if\left({a}\le {R},{a},{R}\right)\le {b}\wedge if\left({a}\le {R},{a},{R}\right)\le {R}\right)\right)$
71 61 63 58 70 syl3anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to \left(if\left({a}\le {R},{a},{R}\right)\le if\left({b}\le {R},{b},{R}\right)↔\left(if\left({a}\le {R},{a},{R}\right)\le {b}\wedge if\left({a}\le {R},{a},{R}\right)\le {R}\right)\right)$
72 69 71 sylibrd ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to \left({a}\le {b}\to if\left({a}\le {R},{a},{R}\right)\le if\left({b}\le {R},{b},{R}\right)\right)$
73 34 adantrr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({a}\right)=if\left({a}\le {R},{a},{R}\right)$
74 simpr ${⊢}\left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\to {b}\in \left[0,\mathrm{+\infty }\right]$
75 vex ${⊢}{b}\in \mathrm{V}$
76 ifexg ${⊢}\left({b}\in \mathrm{V}\wedge {R}\in {ℝ}^{*}\right)\to if\left({b}\le {R},{b},{R}\right)\in \mathrm{V}$
77 75 21 76 sylancr ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to if\left({b}\le {R},{b},{R}\right)\in \mathrm{V}$
78 breq1 ${⊢}{z}={b}\to \left({z}\le {R}↔{b}\le {R}\right)$
79 id ${⊢}{z}={b}\to {z}={b}$
80 78 79 ifbieq1d ${⊢}{z}={b}\to if\left({z}\le {R},{z},{R}\right)=if\left({b}\le {R},{b},{R}\right)$
81 80 32 fvmptg ${⊢}\left({b}\in \left[0,\mathrm{+\infty }\right]\wedge if\left({b}\le {R},{b},{R}\right)\in \mathrm{V}\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({b}\right)=if\left({b}\le {R},{b},{R}\right)$
82 74 77 81 syl2anr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({b}\right)=if\left({b}\le {R},{b},{R}\right)$
83 73 82 breq12d ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to \left(\left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({a}\right)\le \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({b}\right)↔if\left({a}\le {R},{a},{R}\right)\le if\left({b}\le {R},{b},{R}\right)\right)$
84 72 83 sylibrd ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to \left({a}\le {b}\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({a}\right)\le \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({b}\right)\right)$
85 57 63 xaddcld ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to {a}{+}_{𝑒}{b}\in {ℝ}^{*}$
86 xrmin1 ${⊢}\left({a}{+}_{𝑒}{b}\in {ℝ}^{*}\wedge {R}\in {ℝ}^{*}\right)\to if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {a}{+}_{𝑒}{b}$
87 85 58 86 syl2anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {a}{+}_{𝑒}{b}$
88 85 58 ifcld ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\in {ℝ}^{*}$
89 57 58 xaddcld ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to {a}{+}_{𝑒}{R}\in {ℝ}^{*}$
90 xrmin2 ${⊢}\left({a}{+}_{𝑒}{b}\in {ℝ}^{*}\wedge {R}\in {ℝ}^{*}\right)\to if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {R}$
91 85 58 90 syl2anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {R}$
92 xaddid2 ${⊢}{R}\in {ℝ}^{*}\to 0{+}_{𝑒}{R}={R}$
93 58 92 syl ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to 0{+}_{𝑒}{R}={R}$
94 45 a1i ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to 0\in {ℝ}^{*}$
95 elxrge0 ${⊢}{a}\in \left[0,\mathrm{+\infty }\right]↔\left({a}\in {ℝ}^{*}\wedge 0\le {a}\right)$
96 95 simprbi ${⊢}{a}\in \left[0,\mathrm{+\infty }\right]\to 0\le {a}$
97 96 ad2antrl ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to 0\le {a}$
98 xleadd1a ${⊢}\left(\left(0\in {ℝ}^{*}\wedge {a}\in {ℝ}^{*}\wedge {R}\in {ℝ}^{*}\right)\wedge 0\le {a}\right)\to 0{+}_{𝑒}{R}\le {a}{+}_{𝑒}{R}$
99 94 57 58 97 98 syl31anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to 0{+}_{𝑒}{R}\le {a}{+}_{𝑒}{R}$
100 93 99 eqbrtrrd ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to {R}\le {a}{+}_{𝑒}{R}$
101 88 58 89 91 100 xrletrd ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {a}{+}_{𝑒}{R}$
102 oveq2 ${⊢}{b}=if\left({b}\le {R},{b},{R}\right)\to {a}{+}_{𝑒}{b}={a}{+}_{𝑒}if\left({b}\le {R},{b},{R}\right)$
103 102 breq2d ${⊢}{b}=if\left({b}\le {R},{b},{R}\right)\to \left(if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {a}{+}_{𝑒}{b}↔if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {a}{+}_{𝑒}if\left({b}\le {R},{b},{R}\right)\right)$
104 oveq2 ${⊢}{R}=if\left({b}\le {R},{b},{R}\right)\to {a}{+}_{𝑒}{R}={a}{+}_{𝑒}if\left({b}\le {R},{b},{R}\right)$
105 104 breq2d ${⊢}{R}=if\left({b}\le {R},{b},{R}\right)\to \left(if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {a}{+}_{𝑒}{R}↔if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {a}{+}_{𝑒}if\left({b}\le {R},{b},{R}\right)\right)$
106 103 105 ifboth ${⊢}\left(if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {a}{+}_{𝑒}{b}\wedge if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {a}{+}_{𝑒}{R}\right)\to if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {a}{+}_{𝑒}if\left({b}\le {R},{b},{R}\right)$
107 87 101 106 syl2anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {a}{+}_{𝑒}if\left({b}\le {R},{b},{R}\right)$
108 63 58 ifcld ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to if\left({b}\le {R},{b},{R}\right)\in {ℝ}^{*}$
109 58 108 xaddcld ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to {R}{+}_{𝑒}if\left({b}\le {R},{b},{R}\right)\in {ℝ}^{*}$
110 58 xaddid1d ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to {R}{+}_{𝑒}0={R}$
111 elxrge0 ${⊢}{b}\in \left[0,\mathrm{+\infty }\right]↔\left({b}\in {ℝ}^{*}\wedge 0\le {b}\right)$
112 111 simprbi ${⊢}{b}\in \left[0,\mathrm{+\infty }\right]\to 0\le {b}$
113 112 ad2antll ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to 0\le {b}$
114 48 adantr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to 0\le {R}$
115 breq2 ${⊢}{b}=if\left({b}\le {R},{b},{R}\right)\to \left(0\le {b}↔0\le if\left({b}\le {R},{b},{R}\right)\right)$
116 breq2 ${⊢}{R}=if\left({b}\le {R},{b},{R}\right)\to \left(0\le {R}↔0\le if\left({b}\le {R},{b},{R}\right)\right)$
117 115 116 ifboth ${⊢}\left(0\le {b}\wedge 0\le {R}\right)\to 0\le if\left({b}\le {R},{b},{R}\right)$
118 113 114 117 syl2anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to 0\le if\left({b}\le {R},{b},{R}\right)$
119 xleadd2a ${⊢}\left(\left(0\in {ℝ}^{*}\wedge if\left({b}\le {R},{b},{R}\right)\in {ℝ}^{*}\wedge {R}\in {ℝ}^{*}\right)\wedge 0\le if\left({b}\le {R},{b},{R}\right)\right)\to {R}{+}_{𝑒}0\le {R}{+}_{𝑒}if\left({b}\le {R},{b},{R}\right)$
120 94 108 58 118 119 syl31anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to {R}{+}_{𝑒}0\le {R}{+}_{𝑒}if\left({b}\le {R},{b},{R}\right)$
121 110 120 eqbrtrrd ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to {R}\le {R}{+}_{𝑒}if\left({b}\le {R},{b},{R}\right)$
122 88 58 109 91 121 xrletrd ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {R}{+}_{𝑒}if\left({b}\le {R},{b},{R}\right)$
123 oveq1 ${⊢}{a}=if\left({a}\le {R},{a},{R}\right)\to {a}{+}_{𝑒}if\left({b}\le {R},{b},{R}\right)=if\left({a}\le {R},{a},{R}\right){+}_{𝑒}if\left({b}\le {R},{b},{R}\right)$
124 123 breq2d ${⊢}{a}=if\left({a}\le {R},{a},{R}\right)\to \left(if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {a}{+}_{𝑒}if\left({b}\le {R},{b},{R}\right)↔if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le if\left({a}\le {R},{a},{R}\right){+}_{𝑒}if\left({b}\le {R},{b},{R}\right)\right)$
125 oveq1 ${⊢}{R}=if\left({a}\le {R},{a},{R}\right)\to {R}{+}_{𝑒}if\left({b}\le {R},{b},{R}\right)=if\left({a}\le {R},{a},{R}\right){+}_{𝑒}if\left({b}\le {R},{b},{R}\right)$
126 125 breq2d ${⊢}{R}=if\left({a}\le {R},{a},{R}\right)\to \left(if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {R}{+}_{𝑒}if\left({b}\le {R},{b},{R}\right)↔if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le if\left({a}\le {R},{a},{R}\right){+}_{𝑒}if\left({b}\le {R},{b},{R}\right)\right)$
127 124 126 ifboth ${⊢}\left(if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {a}{+}_{𝑒}if\left({b}\le {R},{b},{R}\right)\wedge if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le {R}{+}_{𝑒}if\left({b}\le {R},{b},{R}\right)\right)\to if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le if\left({a}\le {R},{a},{R}\right){+}_{𝑒}if\left({b}\le {R},{b},{R}\right)$
128 107 122 127 syl2anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\le if\left({a}\le {R},{a},{R}\right){+}_{𝑒}if\left({b}\le {R},{b},{R}\right)$
129 ge0xaddcl ${⊢}\left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\to {a}{+}_{𝑒}{b}\in \left[0,\mathrm{+\infty }\right]$
130 ovex ${⊢}{a}{+}_{𝑒}{b}\in \mathrm{V}$
131 ifexg ${⊢}\left({a}{+}_{𝑒}{b}\in \mathrm{V}\wedge {R}\in {ℝ}^{*}\right)\to if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\in \mathrm{V}$
132 130 21 131 sylancr ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\in \mathrm{V}$
133 breq1 ${⊢}{z}={a}{+}_{𝑒}{b}\to \left({z}\le {R}↔{a}{+}_{𝑒}{b}\le {R}\right)$
134 id ${⊢}{z}={a}{+}_{𝑒}{b}\to {z}={a}{+}_{𝑒}{b}$
135 133 134 ifbieq1d ${⊢}{z}={a}{+}_{𝑒}{b}\to if\left({z}\le {R},{z},{R}\right)=if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)$
136 135 32 fvmptg ${⊢}\left({a}{+}_{𝑒}{b}\in \left[0,\mathrm{+\infty }\right]\wedge if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)\in \mathrm{V}\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({a}{+}_{𝑒}{b}\right)=if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)$
137 129 132 136 syl2anr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({a}{+}_{𝑒}{b}\right)=if\left({a}{+}_{𝑒}{b}\le {R},{a}{+}_{𝑒}{b},{R}\right)$
138 73 82 oveq12d ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({a}\right){+}_{𝑒}\left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({b}\right)=if\left({a}\le {R},{a},{R}\right){+}_{𝑒}if\left({b}\le {R},{b},{R}\right)$
139 128 137 138 3brtr4d ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\wedge \left({a}\in \left[0,\mathrm{+\infty }\right]\wedge {b}\in \left[0,\mathrm{+\infty }\right]\right)\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({a}{+}_{𝑒}{b}\right)\le \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({a}\right){+}_{𝑒}\left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\left({b}\right)$
140 2 24 55 84 139 comet ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to \left({z}\in \left[0,\mathrm{+\infty }\right]⟼if\left({z}\le {R},{z},{R}\right)\right)\circ {C}\in \mathrm{\infty Met}\left({X}\right)$
141 19 140 eqeltrrd ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {R}\in {ℝ}^{*}\wedge 0<{R}\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$