Theorem ustrel

Description: The elements of uniform structures, called entourages, are relations. (Contributed by Thierry Arnoux, 15-Nov-2017)

	Ref	Expression
Assertion	ustrel	$$⊢\left(U\in \mathrm{UnifOn}\left(X\right)\wedge V\in U\right)\to \mathrm{Rel}V$$

Proof

Step	Hyp	Ref	Expression
1		ustssxp	$$⊢\left(U\in \mathrm{UnifOn}\left(X\right)\wedge V\in U\right)\to V\subseteq X\times X$$
2		xpss	$$⊢X\times X\subseteq \mathrm{V}\times \mathrm{V}$$
3	1 2	sstrdi	$$⊢\left(U\in \mathrm{UnifOn}\left(X\right)\wedge V\in U\right)\to V\subseteq \mathrm{V}\times \mathrm{V}$$
4		df-rel	$$⊢\mathrm{Rel}V\leftrightarrow V\subseteq \mathrm{V}\times \mathrm{V}$$
5	3 4	sylibr	$$⊢\left(U\in \mathrm{UnifOn}\left(X\right)\wedge V\in U\right)\to \mathrm{Rel}V$$