Theorem metustrel

Description: Elements of the filter base generated by the metric D are relations. (Contributed by Thierry Arnoux, 28-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

	Ref	Expression
Hypothesis	metust.1	$$⊢F=\mathrm{ran}\left(a\in {ℝ}^{+}⟼D^{-1}\left[\left[0,a\right)\right]\right)$$
Assertion	metustrel	$$⊢\left(D\in \mathrm{PsMet}\left(X\right)\wedge A\in F\right)\to \mathrm{Rel}A$$

Proof

Step	Hyp	Ref	Expression
1		metust.1	$$⊢F=\mathrm{ran}\left(a\in {ℝ}^{+}⟼D^{-1}\left[\left[0,a\right)\right]\right)$$
2	1	metustss	$$⊢\left(D\in \mathrm{PsMet}\left(X\right)\wedge A\in F\right)\to A\subseteq X\times X$$
3		xpss	$$⊢X\times X\subseteq \mathrm{V}\times \mathrm{V}$$
4	2 3	sstrdi	$$⊢\left(D\in \mathrm{PsMet}\left(X\right)\wedge A\in F\right)\to A\subseteq \mathrm{V}\times \mathrm{V}$$
5		df-rel	$$⊢\mathrm{Rel}A\leftrightarrow A\subseteq \mathrm{V}\times \mathrm{V}$$
6	4 5	sylibr	$$⊢\left(D\in \mathrm{PsMet}\left(X\right)\wedge A\in F\right)\to \mathrm{Rel}A$$