# Metamath Proof Explorer

## Theorem metuel2

Description: Elementhood in the uniform structure generated by a metric D (Contributed by Thierry Arnoux, 24-Jan-2018) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypothesis metuel2.u ${⊢}{U}=\mathrm{metUnif}\left({D}\right)$
Assertion metuel2 ${⊢}\left({X}\ne \varnothing \wedge {D}\in \mathrm{PsMet}\left({X}\right)\right)\to \left({V}\in {U}↔\left({V}\subseteq {X}×{X}\wedge \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{D}{y}<{d}\to {x}{V}{y}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 metuel2.u ${⊢}{U}=\mathrm{metUnif}\left({D}\right)$
2 1 eleq2i ${⊢}{V}\in {U}↔{V}\in \mathrm{metUnif}\left({D}\right)$
3 2 a1i ${⊢}\left({X}\ne \varnothing \wedge {D}\in \mathrm{PsMet}\left({X}\right)\right)\to \left({V}\in {U}↔{V}\in \mathrm{metUnif}\left({D}\right)\right)$
4 metuel ${⊢}\left({X}\ne \varnothing \wedge {D}\in \mathrm{PsMet}\left({X}\right)\right)\to \left({V}\in \mathrm{metUnif}\left({D}\right)↔\left({V}\subseteq {X}×{X}\wedge \exists {w}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}{w}\subseteq {V}\right)\right)$
5 oveq2 ${⊢}{a}={d}\to \left[0,{a}\right)=\left[0,{d}\right)$
6 5 imaeq2d ${⊢}{a}={d}\to {{D}}^{-1}\left[\left[0,{a}\right)\right]={{D}}^{-1}\left[\left[0,{d}\right)\right]$
7 6 cbvmptv ${⊢}\left({a}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{a}\right)\right]\right)=\left({d}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{d}\right)\right]\right)$
8 7 elrnmpt ${⊢}{w}\in \mathrm{V}\to \left({w}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{a}\right)\right]\right)↔\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{w}={{D}}^{-1}\left[\left[0,{d}\right)\right]\right)$
9 8 elv ${⊢}{w}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{a}\right)\right]\right)↔\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{w}={{D}}^{-1}\left[\left[0,{d}\right)\right]$
10 9 anbi1i ${⊢}\left({w}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{a}\right)\right]\right)\wedge {w}\subseteq {V}\right)↔\left(\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{w}={{D}}^{-1}\left[\left[0,{d}\right)\right]\wedge {w}\subseteq {V}\right)$
11 r19.41v ${⊢}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({w}={{D}}^{-1}\left[\left[0,{d}\right)\right]\wedge {w}\subseteq {V}\right)↔\left(\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{w}={{D}}^{-1}\left[\left[0,{d}\right)\right]\wedge {w}\subseteq {V}\right)$
12 10 11 bitr4i ${⊢}\left({w}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{a}\right)\right]\right)\wedge {w}\subseteq {V}\right)↔\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({w}={{D}}^{-1}\left[\left[0,{d}\right)\right]\wedge {w}\subseteq {V}\right)$
13 12 exbii ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{a}\right)\right]\right)\wedge {w}\subseteq {V}\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({w}={{D}}^{-1}\left[\left[0,{d}\right)\right]\wedge {w}\subseteq {V}\right)$
14 df-rex ${⊢}\exists {w}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}{w}\subseteq {V}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{a}\right)\right]\right)\wedge {w}\subseteq {V}\right)$
15 rexcom4 ${⊢}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}={{D}}^{-1}\left[\left[0,{d}\right)\right]\wedge {w}\subseteq {V}\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({w}={{D}}^{-1}\left[\left[0,{d}\right)\right]\wedge {w}\subseteq {V}\right)$
16 13 14 15 3bitr4i ${⊢}\exists {w}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}{w}\subseteq {V}↔\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}={{D}}^{-1}\left[\left[0,{d}\right)\right]\wedge {w}\subseteq {V}\right)$
17 cnvexg ${⊢}{D}\in \mathrm{PsMet}\left({X}\right)\to {{D}}^{-1}\in \mathrm{V}$
18 imaexg ${⊢}{{D}}^{-1}\in \mathrm{V}\to {{D}}^{-1}\left[\left[0,{d}\right)\right]\in \mathrm{V}$
19 sseq1 ${⊢}{w}={{D}}^{-1}\left[\left[0,{d}\right)\right]\to \left({w}\subseteq {V}↔{{D}}^{-1}\left[\left[0,{d}\right)\right]\subseteq {V}\right)$
20 19 ceqsexgv ${⊢}{{D}}^{-1}\left[\left[0,{d}\right)\right]\in \mathrm{V}\to \left(\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}={{D}}^{-1}\left[\left[0,{d}\right)\right]\wedge {w}\subseteq {V}\right)↔{{D}}^{-1}\left[\left[0,{d}\right)\right]\subseteq {V}\right)$
21 17 18 20 3syl ${⊢}{D}\in \mathrm{PsMet}\left({X}\right)\to \left(\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}={{D}}^{-1}\left[\left[0,{d}\right)\right]\wedge {w}\subseteq {V}\right)↔{{D}}^{-1}\left[\left[0,{d}\right)\right]\subseteq {V}\right)$
22 21 rexbidv ${⊢}{D}\in \mathrm{PsMet}\left({X}\right)\to \left(\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}={{D}}^{-1}\left[\left[0,{d}\right)\right]\wedge {w}\subseteq {V}\right)↔\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{{D}}^{-1}\left[\left[0,{d}\right)\right]\subseteq {V}\right)$
23 22 adantr ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\to \left(\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}={{D}}^{-1}\left[\left[0,{d}\right)\right]\wedge {w}\subseteq {V}\right)↔\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{{D}}^{-1}\left[\left[0,{d}\right)\right]\subseteq {V}\right)$
24 16 23 syl5bb ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\to \left(\exists {w}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}{w}\subseteq {V}↔\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{{D}}^{-1}\left[\left[0,{d}\right)\right]\subseteq {V}\right)$
25 cnvimass ${⊢}{{D}}^{-1}\left[\left[0,{d}\right)\right]\subseteq \mathrm{dom}{D}$
26 simpll ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\to {D}\in \mathrm{PsMet}\left({X}\right)$
27 psmetf ${⊢}{D}\in \mathrm{PsMet}\left({X}\right)\to {D}:{X}×{X}⟶{ℝ}^{*}$
28 fdm ${⊢}{D}:{X}×{X}⟶{ℝ}^{*}\to \mathrm{dom}{D}={X}×{X}$
29 26 27 28 3syl ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\to \mathrm{dom}{D}={X}×{X}$
30 25 29 sseqtrid ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\to {{D}}^{-1}\left[\left[0,{d}\right)\right]\subseteq {X}×{X}$
31 ssrel2 ${⊢}{{D}}^{-1}\left[\left[0,{d}\right)\right]\subseteq {X}×{X}\to \left({{D}}^{-1}\left[\left[0,{d}\right)\right]\subseteq {V}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {{D}}^{-1}\left[\left[0,{d}\right)\right]\to ⟨{x},{y}⟩\in {V}\right)\right)$
32 30 31 syl ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\to \left({{D}}^{-1}\left[\left[0,{d}\right)\right]\subseteq {V}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {{D}}^{-1}\left[\left[0,{d}\right)\right]\to ⟨{x},{y}⟩\in {V}\right)\right)$
33 simplr ${⊢}\left(\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to {x}\in {X}$
34 simpr ${⊢}\left(\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to {y}\in {X}$
35 33 34 opelxpd ${⊢}\left(\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to ⟨{x},{y}⟩\in \left({X}×{X}\right)$
36 35 biantrurd ${⊢}\left(\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to \left({D}\left(⟨{x},{y}⟩\right)\in \left[0,{d}\right)↔\left(⟨{x},{y}⟩\in \left({X}×{X}\right)\wedge {D}\left(⟨{x},{y}⟩\right)\in \left[0,{d}\right)\right)\right)$
37 psmetcl ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {x}\in {X}\wedge {y}\in {X}\right)\to {x}{D}{y}\in {ℝ}^{*}$
38 37 ad5ant145 ${⊢}\left(\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to {x}{D}{y}\in {ℝ}^{*}$
39 38 3biant1d ${⊢}\left(\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to \left(\left(0\le {x}{D}{y}\wedge {x}{D}{y}<{d}\right)↔\left({x}{D}{y}\in {ℝ}^{*}\wedge 0\le {x}{D}{y}\wedge {x}{D}{y}<{d}\right)\right)$
40 psmetge0 ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {x}\in {X}\wedge {y}\in {X}\right)\to 0\le {x}{D}{y}$
41 40 biantrurd ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {x}\in {X}\wedge {y}\in {X}\right)\to \left({x}{D}{y}<{d}↔\left(0\le {x}{D}{y}\wedge {x}{D}{y}<{d}\right)\right)$
42 41 ad5ant145 ${⊢}\left(\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to \left({x}{D}{y}<{d}↔\left(0\le {x}{D}{y}\wedge {x}{D}{y}<{d}\right)\right)$
43 0xr ${⊢}0\in {ℝ}^{*}$
44 simpllr ${⊢}\left(\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to {d}\in {ℝ}^{+}$
45 44 rpxrd ${⊢}\left(\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to {d}\in {ℝ}^{*}$
46 elico1 ${⊢}\left(0\in {ℝ}^{*}\wedge {d}\in {ℝ}^{*}\right)\to \left({x}{D}{y}\in \left[0,{d}\right)↔\left({x}{D}{y}\in {ℝ}^{*}\wedge 0\le {x}{D}{y}\wedge {x}{D}{y}<{d}\right)\right)$
47 43 45 46 sylancr ${⊢}\left(\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to \left({x}{D}{y}\in \left[0,{d}\right)↔\left({x}{D}{y}\in {ℝ}^{*}\wedge 0\le {x}{D}{y}\wedge {x}{D}{y}<{d}\right)\right)$
48 39 42 47 3bitr4d ${⊢}\left(\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to \left({x}{D}{y}<{d}↔{x}{D}{y}\in \left[0,{d}\right)\right)$
49 df-ov ${⊢}{x}{D}{y}={D}\left(⟨{x},{y}⟩\right)$
50 49 eleq1i ${⊢}{x}{D}{y}\in \left[0,{d}\right)↔{D}\left(⟨{x},{y}⟩\right)\in \left[0,{d}\right)$
51 48 50 syl6bb ${⊢}\left(\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to \left({x}{D}{y}<{d}↔{D}\left(⟨{x},{y}⟩\right)\in \left[0,{d}\right)\right)$
52 simp-4l ${⊢}\left(\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to {D}\in \mathrm{PsMet}\left({X}\right)$
53 ffn ${⊢}{D}:{X}×{X}⟶{ℝ}^{*}\to {D}Fn\left({X}×{X}\right)$
54 elpreima ${⊢}{D}Fn\left({X}×{X}\right)\to \left(⟨{x},{y}⟩\in {{D}}^{-1}\left[\left[0,{d}\right)\right]↔\left(⟨{x},{y}⟩\in \left({X}×{X}\right)\wedge {D}\left(⟨{x},{y}⟩\right)\in \left[0,{d}\right)\right)\right)$
55 52 27 53 54 4syl ${⊢}\left(\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to \left(⟨{x},{y}⟩\in {{D}}^{-1}\left[\left[0,{d}\right)\right]↔\left(⟨{x},{y}⟩\in \left({X}×{X}\right)\wedge {D}\left(⟨{x},{y}⟩\right)\in \left[0,{d}\right)\right)\right)$
56 36 51 55 3bitr4d ${⊢}\left(\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to \left({x}{D}{y}<{d}↔⟨{x},{y}⟩\in {{D}}^{-1}\left[\left[0,{d}\right)\right]\right)$
57 56 anasss ${⊢}\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({x}{D}{y}<{d}↔⟨{x},{y}⟩\in {{D}}^{-1}\left[\left[0,{d}\right)\right]\right)$
58 df-br ${⊢}{x}{V}{y}↔⟨{x},{y}⟩\in {V}$
59 58 a1i ${⊢}\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({x}{V}{y}↔⟨{x},{y}⟩\in {V}\right)$
60 57 59 imbi12d ${⊢}\left(\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left(\left({x}{D}{y}<{d}\to {x}{V}{y}\right)↔\left(⟨{x},{y}⟩\in {{D}}^{-1}\left[\left[0,{d}\right)\right]\to ⟨{x},{y}⟩\in {V}\right)\right)$
61 60 2ralbidva ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{D}{y}<{d}\to {x}{V}{y}\right)↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {{D}}^{-1}\left[\left[0,{d}\right)\right]\to ⟨{x},{y}⟩\in {V}\right)\right)$
62 32 61 bitr4d ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\wedge {d}\in {ℝ}^{+}\right)\to \left({{D}}^{-1}\left[\left[0,{d}\right)\right]\subseteq {V}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{D}{y}<{d}\to {x}{V}{y}\right)\right)$
63 62 rexbidva ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\to \left(\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{{D}}^{-1}\left[\left[0,{d}\right)\right]\subseteq {V}↔\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{D}{y}<{d}\to {x}{V}{y}\right)\right)$
64 24 63 bitrd ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {V}\subseteq {X}×{X}\right)\to \left(\exists {w}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}{w}\subseteq {V}↔\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{D}{y}<{d}\to {x}{V}{y}\right)\right)$
65 64 pm5.32da ${⊢}{D}\in \mathrm{PsMet}\left({X}\right)\to \left(\left({V}\subseteq {X}×{X}\wedge \exists {w}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}{w}\subseteq {V}\right)↔\left({V}\subseteq {X}×{X}\wedge \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{D}{y}<{d}\to {x}{V}{y}\right)\right)\right)$
66 65 adantl ${⊢}\left({X}\ne \varnothing \wedge {D}\in \mathrm{PsMet}\left({X}\right)\right)\to \left(\left({V}\subseteq {X}×{X}\wedge \exists {w}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}{w}\subseteq {V}\right)↔\left({V}\subseteq {X}×{X}\wedge \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{D}{y}<{d}\to {x}{V}{y}\right)\right)\right)$
67 3 4 66 3bitrd ${⊢}\left({X}\ne \varnothing \wedge {D}\in \mathrm{PsMet}\left({X}\right)\right)\to \left({V}\in {U}↔\left({V}\subseteq {X}×{X}\wedge \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{D}{y}<{d}\to {x}{V}{y}\right)\right)\right)$