# Metamath Proof Explorer

## Theorem imasf1oxmet

Description: The image of an extended metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses imasf1oxmet.u ${⊢}{\phi }\to {U}={F}{“}_{𝑠}{R}$
imasf1oxmet.v ${⊢}{\phi }\to {V}={\mathrm{Base}}_{{R}}$
imasf1oxmet.f ${⊢}{\phi }\to {F}:{V}\underset{1-1 onto}{⟶}{B}$
imasf1oxmet.r ${⊢}{\phi }\to {R}\in {Z}$
imasf1oxmet.e ${⊢}{E}={\mathrm{dist}\left({R}\right)↾}_{\left({V}×{V}\right)}$
imasf1oxmet.d ${⊢}{D}=\mathrm{dist}\left({U}\right)$
imasf1oxmet.m ${⊢}{\phi }\to {E}\in \mathrm{\infty Met}\left({V}\right)$
Assertion imasf1oxmet ${⊢}{\phi }\to {D}\in \mathrm{\infty Met}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 imasf1oxmet.u ${⊢}{\phi }\to {U}={F}{“}_{𝑠}{R}$
2 imasf1oxmet.v ${⊢}{\phi }\to {V}={\mathrm{Base}}_{{R}}$
3 imasf1oxmet.f ${⊢}{\phi }\to {F}:{V}\underset{1-1 onto}{⟶}{B}$
4 imasf1oxmet.r ${⊢}{\phi }\to {R}\in {Z}$
5 imasf1oxmet.e ${⊢}{E}={\mathrm{dist}\left({R}\right)↾}_{\left({V}×{V}\right)}$
6 imasf1oxmet.d ${⊢}{D}=\mathrm{dist}\left({U}\right)$
7 imasf1oxmet.m ${⊢}{\phi }\to {E}\in \mathrm{\infty Met}\left({V}\right)$
8 f1ofo ${⊢}{F}:{V}\underset{1-1 onto}{⟶}{B}\to {F}:{V}\underset{onto}{⟶}{B}$
9 3 8 syl ${⊢}{\phi }\to {F}:{V}\underset{onto}{⟶}{B}$
10 eqid ${⊢}\mathrm{dist}\left({R}\right)=\mathrm{dist}\left({R}\right)$
11 1 2 9 4 10 6 imasdsfn ${⊢}{\phi }\to {D}Fn\left({B}×{B}\right)$
12 1 adantr ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to {U}={F}{“}_{𝑠}{R}$
13 2 adantr ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to {V}={\mathrm{Base}}_{{R}}$
14 3 adantr ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to {F}:{V}\underset{1-1 onto}{⟶}{B}$
15 4 adantr ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to {R}\in {Z}$
16 7 adantr ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to {E}\in \mathrm{\infty Met}\left({V}\right)$
17 simprl ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to {a}\in {V}$
18 simprr ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to {b}\in {V}$
19 12 13 14 15 5 6 16 17 18 imasdsf1o ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to {F}\left({a}\right){D}{F}\left({b}\right)={a}{E}{b}$
20 xmetcl ${⊢}\left({E}\in \mathrm{\infty Met}\left({V}\right)\wedge {a}\in {V}\wedge {b}\in {V}\right)\to {a}{E}{b}\in {ℝ}^{*}$
21 20 3expb ${⊢}\left({E}\in \mathrm{\infty Met}\left({V}\right)\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to {a}{E}{b}\in {ℝ}^{*}$
22 7 21 sylan ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to {a}{E}{b}\in {ℝ}^{*}$
23 19 22 eqeltrd ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to {F}\left({a}\right){D}{F}\left({b}\right)\in {ℝ}^{*}$
24 23 ralrimivva ${⊢}{\phi }\to \forall {a}\in {V}\phantom{\rule{.4em}{0ex}}\forall {b}\in {V}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\in {ℝ}^{*}$
25 f1ofn ${⊢}{F}:{V}\underset{1-1 onto}{⟶}{B}\to {F}Fn{V}$
26 3 25 syl ${⊢}{\phi }\to {F}Fn{V}$
27 oveq2 ${⊢}{y}={F}\left({b}\right)\to {F}\left({a}\right){D}{y}={F}\left({a}\right){D}{F}\left({b}\right)$
28 27 eleq1d ${⊢}{y}={F}\left({b}\right)\to \left({F}\left({a}\right){D}{y}\in {ℝ}^{*}↔{F}\left({a}\right){D}{F}\left({b}\right)\in {ℝ}^{*}\right)$
29 28 ralrn ${⊢}{F}Fn{V}\to \left(\forall {y}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\in {ℝ}^{*}↔\forall {b}\in {V}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\in {ℝ}^{*}\right)$
30 26 29 syl ${⊢}{\phi }\to \left(\forall {y}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\in {ℝ}^{*}↔\forall {b}\in {V}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\in {ℝ}^{*}\right)$
31 forn ${⊢}{F}:{V}\underset{onto}{⟶}{B}\to \mathrm{ran}{F}={B}$
32 9 31 syl ${⊢}{\phi }\to \mathrm{ran}{F}={B}$
33 32 raleqdv ${⊢}{\phi }\to \left(\forall {y}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\in {ℝ}^{*}↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\in {ℝ}^{*}\right)$
34 30 33 bitr3d ${⊢}{\phi }\to \left(\forall {b}\in {V}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\in {ℝ}^{*}↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\in {ℝ}^{*}\right)$
35 34 ralbidv ${⊢}{\phi }\to \left(\forall {a}\in {V}\phantom{\rule{.4em}{0ex}}\forall {b}\in {V}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\in {ℝ}^{*}↔\forall {a}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\in {ℝ}^{*}\right)$
36 24 35 mpbid ${⊢}{\phi }\to \forall {a}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\in {ℝ}^{*}$
37 oveq1 ${⊢}{x}={F}\left({a}\right)\to {x}{D}{y}={F}\left({a}\right){D}{y}$
38 37 eleq1d ${⊢}{x}={F}\left({a}\right)\to \left({x}{D}{y}\in {ℝ}^{*}↔{F}\left({a}\right){D}{y}\in {ℝ}^{*}\right)$
39 38 ralbidv ${⊢}{x}={F}\left({a}\right)\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\in {ℝ}^{*}↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\in {ℝ}^{*}\right)$
40 39 ralrn ${⊢}{F}Fn{V}\to \left(\forall {x}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\in {ℝ}^{*}↔\forall {a}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\in {ℝ}^{*}\right)$
41 26 40 syl ${⊢}{\phi }\to \left(\forall {x}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\in {ℝ}^{*}↔\forall {a}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\in {ℝ}^{*}\right)$
42 32 raleqdv ${⊢}{\phi }\to \left(\forall {x}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\in {ℝ}^{*}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\in {ℝ}^{*}\right)$
43 41 42 bitr3d ${⊢}{\phi }\to \left(\forall {a}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\in {ℝ}^{*}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\in {ℝ}^{*}\right)$
44 36 43 mpbid ${⊢}{\phi }\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\in {ℝ}^{*}$
45 ffnov ${⊢}{D}:{B}×{B}⟶{ℝ}^{*}↔\left({D}Fn\left({B}×{B}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\in {ℝ}^{*}\right)$
46 11 44 45 sylanbrc ${⊢}{\phi }\to {D}:{B}×{B}⟶{ℝ}^{*}$
47 xmeteq0 ${⊢}\left({E}\in \mathrm{\infty Met}\left({V}\right)\wedge {a}\in {V}\wedge {b}\in {V}\right)\to \left({a}{E}{b}=0↔{a}={b}\right)$
48 16 17 18 47 syl3anc ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to \left({a}{E}{b}=0↔{a}={b}\right)$
49 19 eqeq1d ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to \left({F}\left({a}\right){D}{F}\left({b}\right)=0↔{a}{E}{b}=0\right)$
50 f1of1 ${⊢}{F}:{V}\underset{1-1 onto}{⟶}{B}\to {F}:{V}\underset{1-1}{⟶}{B}$
51 3 50 syl ${⊢}{\phi }\to {F}:{V}\underset{1-1}{⟶}{B}$
52 f1fveq ${⊢}\left({F}:{V}\underset{1-1}{⟶}{B}\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to \left({F}\left({a}\right)={F}\left({b}\right)↔{a}={b}\right)$
53 51 52 sylan ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to \left({F}\left({a}\right)={F}\left({b}\right)↔{a}={b}\right)$
54 48 49 53 3bitr4d ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to \left({F}\left({a}\right){D}{F}\left({b}\right)=0↔{F}\left({a}\right)={F}\left({b}\right)\right)$
55 16 adantr ${⊢}\left(\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\wedge {c}\in {V}\right)\to {E}\in \mathrm{\infty Met}\left({V}\right)$
56 simpr ${⊢}\left(\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\wedge {c}\in {V}\right)\to {c}\in {V}$
57 17 adantr ${⊢}\left(\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\wedge {c}\in {V}\right)\to {a}\in {V}$
58 18 adantr ${⊢}\left(\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\wedge {c}\in {V}\right)\to {b}\in {V}$
59 xmettri2 ${⊢}\left({E}\in \mathrm{\infty Met}\left({V}\right)\wedge \left({c}\in {V}\wedge {a}\in {V}\wedge {b}\in {V}\right)\right)\to {a}{E}{b}\le \left({c}{E}{a}\right){+}_{𝑒}\left({c}{E}{b}\right)$
60 55 56 57 58 59 syl13anc ${⊢}\left(\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\wedge {c}\in {V}\right)\to {a}{E}{b}\le \left({c}{E}{a}\right){+}_{𝑒}\left({c}{E}{b}\right)$
61 19 adantr ${⊢}\left(\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\wedge {c}\in {V}\right)\to {F}\left({a}\right){D}{F}\left({b}\right)={a}{E}{b}$
62 12 adantr ${⊢}\left(\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\wedge {c}\in {V}\right)\to {U}={F}{“}_{𝑠}{R}$
63 13 adantr ${⊢}\left(\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\wedge {c}\in {V}\right)\to {V}={\mathrm{Base}}_{{R}}$
64 14 adantr ${⊢}\left(\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\wedge {c}\in {V}\right)\to {F}:{V}\underset{1-1 onto}{⟶}{B}$
65 15 adantr ${⊢}\left(\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\wedge {c}\in {V}\right)\to {R}\in {Z}$
66 62 63 64 65 5 6 55 56 57 imasdsf1o ${⊢}\left(\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\wedge {c}\in {V}\right)\to {F}\left({c}\right){D}{F}\left({a}\right)={c}{E}{a}$
67 62 63 64 65 5 6 55 56 58 imasdsf1o ${⊢}\left(\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\wedge {c}\in {V}\right)\to {F}\left({c}\right){D}{F}\left({b}\right)={c}{E}{b}$
68 66 67 oveq12d ${⊢}\left(\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\wedge {c}\in {V}\right)\to \left({F}\left({c}\right){D}{F}\left({a}\right)\right){+}_{𝑒}\left({F}\left({c}\right){D}{F}\left({b}\right)\right)=\left({c}{E}{a}\right){+}_{𝑒}\left({c}{E}{b}\right)$
69 60 61 68 3brtr4d ${⊢}\left(\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\wedge {c}\in {V}\right)\to {F}\left({a}\right){D}{F}\left({b}\right)\le \left({F}\left({c}\right){D}{F}\left({a}\right)\right){+}_{𝑒}\left({F}\left({c}\right){D}{F}\left({b}\right)\right)$
70 69 ralrimiva ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to \forall {c}\in {V}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({F}\left({c}\right){D}{F}\left({a}\right)\right){+}_{𝑒}\left({F}\left({c}\right){D}{F}\left({b}\right)\right)$
71 oveq1 ${⊢}{z}={F}\left({c}\right)\to {z}{D}{F}\left({a}\right)={F}\left({c}\right){D}{F}\left({a}\right)$
72 oveq1 ${⊢}{z}={F}\left({c}\right)\to {z}{D}{F}\left({b}\right)={F}\left({c}\right){D}{F}\left({b}\right)$
73 71 72 oveq12d ${⊢}{z}={F}\left({c}\right)\to \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)=\left({F}\left({c}\right){D}{F}\left({a}\right)\right){+}_{𝑒}\left({F}\left({c}\right){D}{F}\left({b}\right)\right)$
74 73 breq2d ${⊢}{z}={F}\left({c}\right)\to \left({F}\left({a}\right){D}{F}\left({b}\right)\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)↔{F}\left({a}\right){D}{F}\left({b}\right)\le \left({F}\left({c}\right){D}{F}\left({a}\right)\right){+}_{𝑒}\left({F}\left({c}\right){D}{F}\left({b}\right)\right)\right)$
75 74 ralrn ${⊢}{F}Fn{V}\to \left(\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)↔\forall {c}\in {V}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({F}\left({c}\right){D}{F}\left({a}\right)\right){+}_{𝑒}\left({F}\left({c}\right){D}{F}\left({b}\right)\right)\right)$
76 26 75 syl ${⊢}{\phi }\to \left(\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)↔\forall {c}\in {V}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({F}\left({c}\right){D}{F}\left({a}\right)\right){+}_{𝑒}\left({F}\left({c}\right){D}{F}\left({b}\right)\right)\right)$
77 32 raleqdv ${⊢}{\phi }\to \left(\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)↔\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)\right)$
78 76 77 bitr3d ${⊢}{\phi }\to \left(\forall {c}\in {V}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({F}\left({c}\right){D}{F}\left({a}\right)\right){+}_{𝑒}\left({F}\left({c}\right){D}{F}\left({b}\right)\right)↔\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)\right)$
79 78 adantr ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to \left(\forall {c}\in {V}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({F}\left({c}\right){D}{F}\left({a}\right)\right){+}_{𝑒}\left({F}\left({c}\right){D}{F}\left({b}\right)\right)↔\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)\right)$
80 70 79 mpbid ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)$
81 54 80 jca ${⊢}\left({\phi }\wedge \left({a}\in {V}\wedge {b}\in {V}\right)\right)\to \left(\left({F}\left({a}\right){D}{F}\left({b}\right)=0↔{F}\left({a}\right)={F}\left({b}\right)\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)\right)$
82 81 ralrimivva ${⊢}{\phi }\to \forall {a}\in {V}\phantom{\rule{.4em}{0ex}}\forall {b}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({a}\right){D}{F}\left({b}\right)=0↔{F}\left({a}\right)={F}\left({b}\right)\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)\right)$
83 27 eqeq1d ${⊢}{y}={F}\left({b}\right)\to \left({F}\left({a}\right){D}{y}=0↔{F}\left({a}\right){D}{F}\left({b}\right)=0\right)$
84 eqeq2 ${⊢}{y}={F}\left({b}\right)\to \left({F}\left({a}\right)={y}↔{F}\left({a}\right)={F}\left({b}\right)\right)$
85 83 84 bibi12d ${⊢}{y}={F}\left({b}\right)\to \left(\left({F}\left({a}\right){D}{y}=0↔{F}\left({a}\right)={y}\right)↔\left({F}\left({a}\right){D}{F}\left({b}\right)=0↔{F}\left({a}\right)={F}\left({b}\right)\right)\right)$
86 oveq2 ${⊢}{y}={F}\left({b}\right)\to {z}{D}{y}={z}{D}{F}\left({b}\right)$
87 86 oveq2d ${⊢}{y}={F}\left({b}\right)\to \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)=\left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)$
88 27 87 breq12d ${⊢}{y}={F}\left({b}\right)\to \left({F}\left({a}\right){D}{y}\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)↔{F}\left({a}\right){D}{F}\left({b}\right)\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)\right)$
89 88 ralbidv ${⊢}{y}={F}\left({b}\right)\to \left(\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)↔\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)\right)$
90 85 89 anbi12d ${⊢}{y}={F}\left({b}\right)\to \left(\left(\left({F}\left({a}\right){D}{y}=0↔{F}\left({a}\right)={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)\right)↔\left(\left({F}\left({a}\right){D}{F}\left({b}\right)=0↔{F}\left({a}\right)={F}\left({b}\right)\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)\right)\right)$
91 90 ralrn ${⊢}{F}Fn{V}\to \left(\forall {y}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({a}\right){D}{y}=0↔{F}\left({a}\right)={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)\right)↔\forall {b}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({a}\right){D}{F}\left({b}\right)=0↔{F}\left({a}\right)={F}\left({b}\right)\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)\right)\right)$
92 26 91 syl ${⊢}{\phi }\to \left(\forall {y}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({a}\right){D}{y}=0↔{F}\left({a}\right)={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)\right)↔\forall {b}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({a}\right){D}{F}\left({b}\right)=0↔{F}\left({a}\right)={F}\left({b}\right)\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)\right)\right)$
93 32 raleqdv ${⊢}{\phi }\to \left(\forall {y}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({a}\right){D}{y}=0↔{F}\left({a}\right)={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)\right)↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({a}\right){D}{y}=0↔{F}\left({a}\right)={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)\right)\right)$
94 92 93 bitr3d ${⊢}{\phi }\to \left(\forall {b}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({a}\right){D}{F}\left({b}\right)=0↔{F}\left({a}\right)={F}\left({b}\right)\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)\right)↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({a}\right){D}{y}=0↔{F}\left({a}\right)={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)\right)\right)$
95 94 ralbidv ${⊢}{\phi }\to \left(\forall {a}\in {V}\phantom{\rule{.4em}{0ex}}\forall {b}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({a}\right){D}{F}\left({b}\right)=0↔{F}\left({a}\right)={F}\left({b}\right)\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{F}\left({b}\right)\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{F}\left({b}\right)\right)\right)↔\forall {a}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({a}\right){D}{y}=0↔{F}\left({a}\right)={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)\right)\right)$
96 82 95 mpbid ${⊢}{\phi }\to \forall {a}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({a}\right){D}{y}=0↔{F}\left({a}\right)={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)\right)$
97 37 eqeq1d ${⊢}{x}={F}\left({a}\right)\to \left({x}{D}{y}=0↔{F}\left({a}\right){D}{y}=0\right)$
98 eqeq1 ${⊢}{x}={F}\left({a}\right)\to \left({x}={y}↔{F}\left({a}\right)={y}\right)$
99 97 98 bibi12d ${⊢}{x}={F}\left({a}\right)\to \left(\left({x}{D}{y}=0↔{x}={y}\right)↔\left({F}\left({a}\right){D}{y}=0↔{F}\left({a}\right)={y}\right)\right)$
100 oveq2 ${⊢}{x}={F}\left({a}\right)\to {z}{D}{x}={z}{D}{F}\left({a}\right)$
101 100 oveq1d ${⊢}{x}={F}\left({a}\right)\to \left({z}{D}{x}\right){+}_{𝑒}\left({z}{D}{y}\right)=\left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)$
102 37 101 breq12d ${⊢}{x}={F}\left({a}\right)\to \left({x}{D}{y}\le \left({z}{D}{x}\right){+}_{𝑒}\left({z}{D}{y}\right)↔{F}\left({a}\right){D}{y}\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)\right)$
103 102 ralbidv ${⊢}{x}={F}\left({a}\right)\to \left(\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right){+}_{𝑒}\left({z}{D}{y}\right)↔\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)\right)$
104 99 103 anbi12d ${⊢}{x}={F}\left({a}\right)\to \left(\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right){+}_{𝑒}\left({z}{D}{y}\right)\right)↔\left(\left({F}\left({a}\right){D}{y}=0↔{F}\left({a}\right)={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)\right)\right)$
105 104 ralbidv ${⊢}{x}={F}\left({a}\right)\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right){+}_{𝑒}\left({z}{D}{y}\right)\right)↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({a}\right){D}{y}=0↔{F}\left({a}\right)={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)\right)\right)$
106 105 ralrn ${⊢}{F}Fn{V}\to \left(\forall {x}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right){+}_{𝑒}\left({z}{D}{y}\right)\right)↔\forall {a}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({a}\right){D}{y}=0↔{F}\left({a}\right)={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)\right)\right)$
107 26 106 syl ${⊢}{\phi }\to \left(\forall {x}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right){+}_{𝑒}\left({z}{D}{y}\right)\right)↔\forall {a}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({a}\right){D}{y}=0↔{F}\left({a}\right)={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)\right)\right)$
108 32 raleqdv ${⊢}{\phi }\to \left(\forall {x}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right){+}_{𝑒}\left({z}{D}{y}\right)\right)↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right){+}_{𝑒}\left({z}{D}{y}\right)\right)\right)$
109 107 108 bitr3d ${⊢}{\phi }\to \left(\forall {a}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({a}\right){D}{y}=0↔{F}\left({a}\right)={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}\right){D}{y}\le \left({z}{D}{F}\left({a}\right)\right){+}_{𝑒}\left({z}{D}{y}\right)\right)↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right){+}_{𝑒}\left({z}{D}{y}\right)\right)\right)$
110 96 109 mpbid ${⊢}{\phi }\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right){+}_{𝑒}\left({z}{D}{y}\right)\right)$
111 7 elfvexd ${⊢}{\phi }\to {V}\in \mathrm{V}$
112 fornex ${⊢}{V}\in \mathrm{V}\to \left({F}:{V}\underset{onto}{⟶}{B}\to {B}\in \mathrm{V}\right)$
113 111 9 112 sylc ${⊢}{\phi }\to {B}\in \mathrm{V}$
114 isxmet ${⊢}{B}\in \mathrm{V}\to \left({D}\in \mathrm{\infty Met}\left({B}\right)↔\left({D}:{B}×{B}⟶{ℝ}^{*}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right){+}_{𝑒}\left({z}{D}{y}\right)\right)\right)\right)$
115 113 114 syl ${⊢}{\phi }\to \left({D}\in \mathrm{\infty Met}\left({B}\right)↔\left({D}:{B}×{B}⟶{ℝ}^{*}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right){+}_{𝑒}\left({z}{D}{y}\right)\right)\right)\right)$
116 46 110 115 mpbir2and ${⊢}{\phi }\to {D}\in \mathrm{\infty Met}\left({B}\right)$