Theorem metustss

Description: Range of the elements of the filter base generated by the metric D . (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	metustss	$$⊢\left(D\in \mathrm{PsMet}\left(X\right)\wedge A\in F\right)\to A\subseteq X\times X$$

Proof

Step	Hyp	Ref	Expression
1		metust.1	$$⊢F=\mathrm{ran}\left(a\in {ℝ}^{+}⟼D^{-1}\left[\left[0,a\right)\right]\right)$$
2		cnvimass	$$⊢D^{-1}\left[\left[0,a\right)\right]\subseteq \mathrm{dom}D$$
3		psmetf	$$⊢D\in \mathrm{PsMet}\left(X\right)\to D:X\times X⟶{ℝ}^{*}$$
4	2 3	fssdm	$$⊢D\in \mathrm{PsMet}\left(X\right)\to D^{-1}\left[\left[0,a\right)\right]\subseteq X\times X$$
5	4	ad2antrr	$$⊢\left(\left(D\in \mathrm{PsMet}\left(X\right)\wedge A\in F\right)\wedge a\in {ℝ}^{+}\right)\to D^{-1}\left[\left[0,a\right)\right]\subseteq X\times X$$
6		cnvexg	$$⊢D\in \mathrm{PsMet}\left(X\right)\to D^{-1}\in \mathrm{V}$$
7		imaexg	$$⊢D^{-1}\in \mathrm{V}\to D^{-1}\left[\left[0,a\right)\right]\in \mathrm{V}$$
8		elpwg	$$⊢D^{-1}\left[\left[0,a\right)\right]\in \mathrm{V}\to \left(D^{-1}\left[\left[0,a\right)\right]\in 𝒫\left(X\times X\right)\leftrightarrow D^{-1}\left[\left[0,a\right)\right]\subseteq X\times X\right)$$
9	6 7 8	3syl	$$⊢D\in \mathrm{PsMet}\left(X\right)\to \left(D^{-1}\left[\left[0,a\right)\right]\in 𝒫\left(X\times X\right)\leftrightarrow D^{-1}\left[\left[0,a\right)\right]\subseteq X\times X\right)$$
10	9	ad2antrr	$$⊢\left(\left(D\in \mathrm{PsMet}\left(X\right)\wedge A\in F\right)\wedge a\in {ℝ}^{+}\right)\to \left(D^{-1}\left[\left[0,a\right)\right]\in 𝒫\left(X\times X\right)\leftrightarrow D^{-1}\left[\left[0,a\right)\right]\subseteq X\times X\right)$$
11	5 10	mpbird	$$⊢\left(\left(D\in \mathrm{PsMet}\left(X\right)\wedge A\in F\right)\wedge a\in {ℝ}^{+}\right)\to D^{-1}\left[\left[0,a\right)\right]\in 𝒫\left(X\times X\right)$$
12	11	ralrimiva	$$⊢\left(D\in \mathrm{PsMet}\left(X\right)\wedge A\in F\right)\to \forall a\in {ℝ}^{+}{D}^{-1}\left[\left[0,a\right)\right]\in 𝒫\left(X\times X\right)$$
13		eqid	$$⊢\left(a\in {ℝ}^{+}⟼D^{-1}\left[\left[0,a\right)\right]\right)=\left(a\in {ℝ}^{+}⟼D^{-1}\left[\left[0,a\right)\right]\right)$$
14	13	rnmptss	$$⊢\forall a\in {ℝ}^{+}{D}^{-1}\left[\left[0,a\right)\right]\in 𝒫\left(X\times X\right)\to \mathrm{ran}\left(a\in {ℝ}^{+}⟼D^{-1}\left[\left[0,a\right)\right]\right)\subseteq 𝒫\left(X\times X\right)$$
15	12 14	syl	$$⊢\left(D\in \mathrm{PsMet}\left(X\right)\wedge A\in F\right)\to \mathrm{ran}\left(a\in {ℝ}^{+}⟼D^{-1}\left[\left[0,a\right)\right]\right)\subseteq 𝒫\left(X\times X\right)$$
16	1 15	eqsstrid	$$⊢\left(D\in \mathrm{PsMet}\left(X\right)\wedge A\in F\right)\to F\subseteq 𝒫\left(X\times X\right)$$
17		simpr	$$⊢\left(D\in \mathrm{PsMet}\left(X\right)\wedge A\in F\right)\to A\in F$$
18	16 17	sseldd	$$⊢\left(D\in \mathrm{PsMet}\left(X\right)\wedge A\in F\right)\to A\in 𝒫\left(X\times X\right)$$
19	18	elpwid	$$⊢\left(D\in \mathrm{PsMet}\left(X\right)\wedge A\in F\right)\to A\subseteq X\times X$$