# Metamath Proof Explorer

## Theorem metf1o

Description: Use a bijection with a metric space to construct a metric on a set. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypothesis metf1o.2 ${⊢}{N}=\left({x}\in {Y},{y}\in {Y}⟼{F}\left({x}\right){M}{F}\left({y}\right)\right)$
Assertion metf1o ${⊢}\left({Y}\in {A}\wedge {M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\to {N}\in \mathrm{Met}\left({Y}\right)$

### Proof

Step Hyp Ref Expression
1 metf1o.2 ${⊢}{N}=\left({x}\in {Y},{y}\in {Y}⟼{F}\left({x}\right){M}{F}\left({y}\right)\right)$
2 f1of ${⊢}{F}:{Y}\underset{1-1 onto}{⟶}{X}\to {F}:{Y}⟶{X}$
3 ffvelrn ${⊢}\left({F}:{Y}⟶{X}\wedge {x}\in {Y}\right)\to {F}\left({x}\right)\in {X}$
4 3 ex ${⊢}{F}:{Y}⟶{X}\to \left({x}\in {Y}\to {F}\left({x}\right)\in {X}\right)$
5 ffvelrn ${⊢}\left({F}:{Y}⟶{X}\wedge {y}\in {Y}\right)\to {F}\left({y}\right)\in {X}$
6 5 ex ${⊢}{F}:{Y}⟶{X}\to \left({y}\in {Y}\to {F}\left({y}\right)\in {X}\right)$
7 4 6 anim12d ${⊢}{F}:{Y}⟶{X}\to \left(\left({x}\in {Y}\wedge {y}\in {Y}\right)\to \left({F}\left({x}\right)\in {X}\wedge {F}\left({y}\right)\in {X}\right)\right)$
8 2 7 syl ${⊢}{F}:{Y}\underset{1-1 onto}{⟶}{X}\to \left(\left({x}\in {Y}\wedge {y}\in {Y}\right)\to \left({F}\left({x}\right)\in {X}\wedge {F}\left({y}\right)\in {X}\right)\right)$
9 metcl ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {F}\left({x}\right)\in {X}\wedge {F}\left({y}\right)\in {X}\right)\to {F}\left({x}\right){M}{F}\left({y}\right)\in ℝ$
10 9 3expib ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to \left(\left({F}\left({x}\right)\in {X}\wedge {F}\left({y}\right)\in {X}\right)\to {F}\left({x}\right){M}{F}\left({y}\right)\in ℝ\right)$
11 8 10 sylan9r ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\to \left(\left({x}\in {Y}\wedge {y}\in {Y}\right)\to {F}\left({x}\right){M}{F}\left({y}\right)\in ℝ\right)$
12 11 3adant1 ${⊢}\left({Y}\in {A}\wedge {M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\to \left(\left({x}\in {Y}\wedge {y}\in {Y}\right)\to {F}\left({x}\right){M}{F}\left({y}\right)\in ℝ\right)$
13 12 ralrimivv ${⊢}\left({Y}\in {A}\wedge {M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\to \forall {x}\in {Y}\phantom{\rule{.4em}{0ex}}\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){M}{F}\left({y}\right)\in ℝ$
14 1 fmpo ${⊢}\forall {x}\in {Y}\phantom{\rule{.4em}{0ex}}\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){M}{F}\left({y}\right)\in ℝ↔{N}:{Y}×{Y}⟶ℝ$
15 13 14 sylib ${⊢}\left({Y}\in {A}\wedge {M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\to {N}:{Y}×{Y}⟶ℝ$
16 fveq2 ${⊢}{x}={u}\to {F}\left({x}\right)={F}\left({u}\right)$
17 16 oveq1d ${⊢}{x}={u}\to {F}\left({x}\right){M}{F}\left({y}\right)={F}\left({u}\right){M}{F}\left({y}\right)$
18 fveq2 ${⊢}{y}={v}\to {F}\left({y}\right)={F}\left({v}\right)$
19 18 oveq2d ${⊢}{y}={v}\to {F}\left({u}\right){M}{F}\left({y}\right)={F}\left({u}\right){M}{F}\left({v}\right)$
20 ovex ${⊢}{F}\left({u}\right){M}{F}\left({v}\right)\in \mathrm{V}$
21 17 19 1 20 ovmpo ${⊢}\left({u}\in {Y}\wedge {v}\in {Y}\right)\to {u}{N}{v}={F}\left({u}\right){M}{F}\left({v}\right)$
22 21 eqeq1d ${⊢}\left({u}\in {Y}\wedge {v}\in {Y}\right)\to \left({u}{N}{v}=0↔{F}\left({u}\right){M}{F}\left({v}\right)=0\right)$
23 22 adantl ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\wedge \left({u}\in {Y}\wedge {v}\in {Y}\right)\right)\to \left({u}{N}{v}=0↔{F}\left({u}\right){M}{F}\left({v}\right)=0\right)$
24 ffvelrn ${⊢}\left({F}:{Y}⟶{X}\wedge {u}\in {Y}\right)\to {F}\left({u}\right)\in {X}$
25 24 ex ${⊢}{F}:{Y}⟶{X}\to \left({u}\in {Y}\to {F}\left({u}\right)\in {X}\right)$
26 ffvelrn ${⊢}\left({F}:{Y}⟶{X}\wedge {v}\in {Y}\right)\to {F}\left({v}\right)\in {X}$
27 26 ex ${⊢}{F}:{Y}⟶{X}\to \left({v}\in {Y}\to {F}\left({v}\right)\in {X}\right)$
28 25 27 anim12d ${⊢}{F}:{Y}⟶{X}\to \left(\left({u}\in {Y}\wedge {v}\in {Y}\right)\to \left({F}\left({u}\right)\in {X}\wedge {F}\left({v}\right)\in {X}\right)\right)$
29 2 28 syl ${⊢}{F}:{Y}\underset{1-1 onto}{⟶}{X}\to \left(\left({u}\in {Y}\wedge {v}\in {Y}\right)\to \left({F}\left({u}\right)\in {X}\wedge {F}\left({v}\right)\in {X}\right)\right)$
30 29 imp ${⊢}\left({F}:{Y}\underset{1-1 onto}{⟶}{X}\wedge \left({u}\in {Y}\wedge {v}\in {Y}\right)\right)\to \left({F}\left({u}\right)\in {X}\wedge {F}\left({v}\right)\in {X}\right)$
31 30 adantll ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\wedge \left({u}\in {Y}\wedge {v}\in {Y}\right)\right)\to \left({F}\left({u}\right)\in {X}\wedge {F}\left({v}\right)\in {X}\right)$
32 meteq0 ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {F}\left({u}\right)\in {X}\wedge {F}\left({v}\right)\in {X}\right)\to \left({F}\left({u}\right){M}{F}\left({v}\right)=0↔{F}\left({u}\right)={F}\left({v}\right)\right)$
33 32 3expb ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left({F}\left({u}\right)\in {X}\wedge {F}\left({v}\right)\in {X}\right)\right)\to \left({F}\left({u}\right){M}{F}\left({v}\right)=0↔{F}\left({u}\right)={F}\left({v}\right)\right)$
34 33 adantlr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\wedge \left({F}\left({u}\right)\in {X}\wedge {F}\left({v}\right)\in {X}\right)\right)\to \left({F}\left({u}\right){M}{F}\left({v}\right)=0↔{F}\left({u}\right)={F}\left({v}\right)\right)$
35 31 34 syldan ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\wedge \left({u}\in {Y}\wedge {v}\in {Y}\right)\right)\to \left({F}\left({u}\right){M}{F}\left({v}\right)=0↔{F}\left({u}\right)={F}\left({v}\right)\right)$
36 f1of1 ${⊢}{F}:{Y}\underset{1-1 onto}{⟶}{X}\to {F}:{Y}\underset{1-1}{⟶}{X}$
37 f1fveq ${⊢}\left({F}:{Y}\underset{1-1}{⟶}{X}\wedge \left({u}\in {Y}\wedge {v}\in {Y}\right)\right)\to \left({F}\left({u}\right)={F}\left({v}\right)↔{u}={v}\right)$
38 36 37 sylan ${⊢}\left({F}:{Y}\underset{1-1 onto}{⟶}{X}\wedge \left({u}\in {Y}\wedge {v}\in {Y}\right)\right)\to \left({F}\left({u}\right)={F}\left({v}\right)↔{u}={v}\right)$
39 38 adantll ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\wedge \left({u}\in {Y}\wedge {v}\in {Y}\right)\right)\to \left({F}\left({u}\right)={F}\left({v}\right)↔{u}={v}\right)$
40 23 35 39 3bitrd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\wedge \left({u}\in {Y}\wedge {v}\in {Y}\right)\right)\to \left({u}{N}{v}=0↔{u}={v}\right)$
41 ffvelrn ${⊢}\left({F}:{Y}⟶{X}\wedge {w}\in {Y}\right)\to {F}\left({w}\right)\in {X}$
42 41 ex ${⊢}{F}:{Y}⟶{X}\to \left({w}\in {Y}\to {F}\left({w}\right)\in {X}\right)$
43 28 42 anim12d ${⊢}{F}:{Y}⟶{X}\to \left(\left(\left({u}\in {Y}\wedge {v}\in {Y}\right)\wedge {w}\in {Y}\right)\to \left(\left({F}\left({u}\right)\in {X}\wedge {F}\left({v}\right)\in {X}\right)\wedge {F}\left({w}\right)\in {X}\right)\right)$
44 2 43 syl ${⊢}{F}:{Y}\underset{1-1 onto}{⟶}{X}\to \left(\left(\left({u}\in {Y}\wedge {v}\in {Y}\right)\wedge {w}\in {Y}\right)\to \left(\left({F}\left({u}\right)\in {X}\wedge {F}\left({v}\right)\in {X}\right)\wedge {F}\left({w}\right)\in {X}\right)\right)$
45 44 imp ${⊢}\left({F}:{Y}\underset{1-1 onto}{⟶}{X}\wedge \left(\left({u}\in {Y}\wedge {v}\in {Y}\right)\wedge {w}\in {Y}\right)\right)\to \left(\left({F}\left({u}\right)\in {X}\wedge {F}\left({v}\right)\in {X}\right)\wedge {F}\left({w}\right)\in {X}\right)$
46 45 adantll ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\wedge \left(\left({u}\in {Y}\wedge {v}\in {Y}\right)\wedge {w}\in {Y}\right)\right)\to \left(\left({F}\left({u}\right)\in {X}\wedge {F}\left({v}\right)\in {X}\right)\wedge {F}\left({w}\right)\in {X}\right)$
47 mettri2 ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left({F}\left({w}\right)\in {X}\wedge {F}\left({u}\right)\in {X}\wedge {F}\left({v}\right)\in {X}\right)\right)\to {F}\left({u}\right){M}{F}\left({v}\right)\le \left({F}\left({w}\right){M}{F}\left({u}\right)\right)+\left({F}\left({w}\right){M}{F}\left({v}\right)\right)$
48 47 expcom ${⊢}\left({F}\left({w}\right)\in {X}\wedge {F}\left({u}\right)\in {X}\wedge {F}\left({v}\right)\in {X}\right)\to \left({M}\in \mathrm{Met}\left({X}\right)\to {F}\left({u}\right){M}{F}\left({v}\right)\le \left({F}\left({w}\right){M}{F}\left({u}\right)\right)+\left({F}\left({w}\right){M}{F}\left({v}\right)\right)\right)$
49 48 3expb ${⊢}\left({F}\left({w}\right)\in {X}\wedge \left({F}\left({u}\right)\in {X}\wedge {F}\left({v}\right)\in {X}\right)\right)\to \left({M}\in \mathrm{Met}\left({X}\right)\to {F}\left({u}\right){M}{F}\left({v}\right)\le \left({F}\left({w}\right){M}{F}\left({u}\right)\right)+\left({F}\left({w}\right){M}{F}\left({v}\right)\right)\right)$
50 49 ancoms ${⊢}\left(\left({F}\left({u}\right)\in {X}\wedge {F}\left({v}\right)\in {X}\right)\wedge {F}\left({w}\right)\in {X}\right)\to \left({M}\in \mathrm{Met}\left({X}\right)\to {F}\left({u}\right){M}{F}\left({v}\right)\le \left({F}\left({w}\right){M}{F}\left({u}\right)\right)+\left({F}\left({w}\right){M}{F}\left({v}\right)\right)\right)$
51 50 impcom ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({F}\left({u}\right)\in {X}\wedge {F}\left({v}\right)\in {X}\right)\wedge {F}\left({w}\right)\in {X}\right)\right)\to {F}\left({u}\right){M}{F}\left({v}\right)\le \left({F}\left({w}\right){M}{F}\left({u}\right)\right)+\left({F}\left({w}\right){M}{F}\left({v}\right)\right)$
52 51 adantlr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\wedge \left(\left({F}\left({u}\right)\in {X}\wedge {F}\left({v}\right)\in {X}\right)\wedge {F}\left({w}\right)\in {X}\right)\right)\to {F}\left({u}\right){M}{F}\left({v}\right)\le \left({F}\left({w}\right){M}{F}\left({u}\right)\right)+\left({F}\left({w}\right){M}{F}\left({v}\right)\right)$
53 46 52 syldan ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\wedge \left(\left({u}\in {Y}\wedge {v}\in {Y}\right)\wedge {w}\in {Y}\right)\right)\to {F}\left({u}\right){M}{F}\left({v}\right)\le \left({F}\left({w}\right){M}{F}\left({u}\right)\right)+\left({F}\left({w}\right){M}{F}\left({v}\right)\right)$
54 53 anassrs ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\wedge \left({u}\in {Y}\wedge {v}\in {Y}\right)\right)\wedge {w}\in {Y}\right)\to {F}\left({u}\right){M}{F}\left({v}\right)\le \left({F}\left({w}\right){M}{F}\left({u}\right)\right)+\left({F}\left({w}\right){M}{F}\left({v}\right)\right)$
55 21 adantr ${⊢}\left(\left({u}\in {Y}\wedge {v}\in {Y}\right)\wedge {w}\in {Y}\right)\to {u}{N}{v}={F}\left({u}\right){M}{F}\left({v}\right)$
56 fveq2 ${⊢}{x}={w}\to {F}\left({x}\right)={F}\left({w}\right)$
57 56 oveq1d ${⊢}{x}={w}\to {F}\left({x}\right){M}{F}\left({y}\right)={F}\left({w}\right){M}{F}\left({y}\right)$
58 fveq2 ${⊢}{y}={u}\to {F}\left({y}\right)={F}\left({u}\right)$
59 58 oveq2d ${⊢}{y}={u}\to {F}\left({w}\right){M}{F}\left({y}\right)={F}\left({w}\right){M}{F}\left({u}\right)$
60 ovex ${⊢}{F}\left({w}\right){M}{F}\left({u}\right)\in \mathrm{V}$
61 57 59 1 60 ovmpo ${⊢}\left({w}\in {Y}\wedge {u}\in {Y}\right)\to {w}{N}{u}={F}\left({w}\right){M}{F}\left({u}\right)$
62 61 ancoms ${⊢}\left({u}\in {Y}\wedge {w}\in {Y}\right)\to {w}{N}{u}={F}\left({w}\right){M}{F}\left({u}\right)$
63 62 adantlr ${⊢}\left(\left({u}\in {Y}\wedge {v}\in {Y}\right)\wedge {w}\in {Y}\right)\to {w}{N}{u}={F}\left({w}\right){M}{F}\left({u}\right)$
64 18 oveq2d ${⊢}{y}={v}\to {F}\left({w}\right){M}{F}\left({y}\right)={F}\left({w}\right){M}{F}\left({v}\right)$
65 ovex ${⊢}{F}\left({w}\right){M}{F}\left({v}\right)\in \mathrm{V}$
66 57 64 1 65 ovmpo ${⊢}\left({w}\in {Y}\wedge {v}\in {Y}\right)\to {w}{N}{v}={F}\left({w}\right){M}{F}\left({v}\right)$
67 66 ancoms ${⊢}\left({v}\in {Y}\wedge {w}\in {Y}\right)\to {w}{N}{v}={F}\left({w}\right){M}{F}\left({v}\right)$
68 67 adantll ${⊢}\left(\left({u}\in {Y}\wedge {v}\in {Y}\right)\wedge {w}\in {Y}\right)\to {w}{N}{v}={F}\left({w}\right){M}{F}\left({v}\right)$
69 63 68 oveq12d ${⊢}\left(\left({u}\in {Y}\wedge {v}\in {Y}\right)\wedge {w}\in {Y}\right)\to \left({w}{N}{u}\right)+\left({w}{N}{v}\right)=\left({F}\left({w}\right){M}{F}\left({u}\right)\right)+\left({F}\left({w}\right){M}{F}\left({v}\right)\right)$
70 55 69 breq12d ${⊢}\left(\left({u}\in {Y}\wedge {v}\in {Y}\right)\wedge {w}\in {Y}\right)\to \left({u}{N}{v}\le \left({w}{N}{u}\right)+\left({w}{N}{v}\right)↔{F}\left({u}\right){M}{F}\left({v}\right)\le \left({F}\left({w}\right){M}{F}\left({u}\right)\right)+\left({F}\left({w}\right){M}{F}\left({v}\right)\right)\right)$
71 70 adantll ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\wedge \left({u}\in {Y}\wedge {v}\in {Y}\right)\right)\wedge {w}\in {Y}\right)\to \left({u}{N}{v}\le \left({w}{N}{u}\right)+\left({w}{N}{v}\right)↔{F}\left({u}\right){M}{F}\left({v}\right)\le \left({F}\left({w}\right){M}{F}\left({u}\right)\right)+\left({F}\left({w}\right){M}{F}\left({v}\right)\right)\right)$
72 54 71 mpbird ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\wedge \left({u}\in {Y}\wedge {v}\in {Y}\right)\right)\wedge {w}\in {Y}\right)\to {u}{N}{v}\le \left({w}{N}{u}\right)+\left({w}{N}{v}\right)$
73 72 ralrimiva ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\wedge \left({u}\in {Y}\wedge {v}\in {Y}\right)\right)\to \forall {w}\in {Y}\phantom{\rule{.4em}{0ex}}{u}{N}{v}\le \left({w}{N}{u}\right)+\left({w}{N}{v}\right)$
74 40 73 jca ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\wedge \left({u}\in {Y}\wedge {v}\in {Y}\right)\right)\to \left(\left({u}{N}{v}=0↔{u}={v}\right)\wedge \forall {w}\in {Y}\phantom{\rule{.4em}{0ex}}{u}{N}{v}\le \left({w}{N}{u}\right)+\left({w}{N}{v}\right)\right)$
75 74 3adantl1 ${⊢}\left(\left({Y}\in {A}\wedge {M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\wedge \left({u}\in {Y}\wedge {v}\in {Y}\right)\right)\to \left(\left({u}{N}{v}=0↔{u}={v}\right)\wedge \forall {w}\in {Y}\phantom{\rule{.4em}{0ex}}{u}{N}{v}\le \left({w}{N}{u}\right)+\left({w}{N}{v}\right)\right)$
76 75 ex ${⊢}\left({Y}\in {A}\wedge {M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\to \left(\left({u}\in {Y}\wedge {v}\in {Y}\right)\to \left(\left({u}{N}{v}=0↔{u}={v}\right)\wedge \forall {w}\in {Y}\phantom{\rule{.4em}{0ex}}{u}{N}{v}\le \left({w}{N}{u}\right)+\left({w}{N}{v}\right)\right)\right)$
77 76 ralrimivv ${⊢}\left({Y}\in {A}\wedge {M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\to \forall {u}\in {Y}\phantom{\rule{.4em}{0ex}}\forall {v}\in {Y}\phantom{\rule{.4em}{0ex}}\left(\left({u}{N}{v}=0↔{u}={v}\right)\wedge \forall {w}\in {Y}\phantom{\rule{.4em}{0ex}}{u}{N}{v}\le \left({w}{N}{u}\right)+\left({w}{N}{v}\right)\right)$
78 ismet ${⊢}{Y}\in {A}\to \left({N}\in \mathrm{Met}\left({Y}\right)↔\left({N}:{Y}×{Y}⟶ℝ\wedge \forall {u}\in {Y}\phantom{\rule{.4em}{0ex}}\forall {v}\in {Y}\phantom{\rule{.4em}{0ex}}\left(\left({u}{N}{v}=0↔{u}={v}\right)\wedge \forall {w}\in {Y}\phantom{\rule{.4em}{0ex}}{u}{N}{v}\le \left({w}{N}{u}\right)+\left({w}{N}{v}\right)\right)\right)\right)$
79 78 3ad2ant1 ${⊢}\left({Y}\in {A}\wedge {M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\to \left({N}\in \mathrm{Met}\left({Y}\right)↔\left({N}:{Y}×{Y}⟶ℝ\wedge \forall {u}\in {Y}\phantom{\rule{.4em}{0ex}}\forall {v}\in {Y}\phantom{\rule{.4em}{0ex}}\left(\left({u}{N}{v}=0↔{u}={v}\right)\wedge \forall {w}\in {Y}\phantom{\rule{.4em}{0ex}}{u}{N}{v}\le \left({w}{N}{u}\right)+\left({w}{N}{v}\right)\right)\right)\right)$
80 15 77 79 mpbir2and ${⊢}\left({Y}\in {A}\wedge {M}\in \mathrm{Met}\left({X}\right)\wedge {F}:{Y}\underset{1-1 onto}{⟶}{X}\right)\to {N}\in \mathrm{Met}\left({Y}\right)$